Different behaviour between a GADT and a data family with regards to kind unification

[dreixel]

We have discussed this before, but I don't remember if this was classified as a bug or as a "known feature" of GADTs. Given the following code:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}

data Sum a b = L a | R b

data Sum1 (a :: k1 -> *) (b :: k2 -> *) :: Sum k1 k2 -> * where
  LL :: a i -> Sum1 a b (L i)
  RR :: b i -> Sum1 a b (R i)

data Code i o = F (Code (Sum i o) o)

An interpretation for Code using a data family works:

data family In (f :: Code i o) :: (i -> *) -> (o -> *)

data instance In (F f) r o where
  In :: In f (Sum1 r (In (F f) r)) o -> In (F f) r o

However, if we try to use a GADT instead...

data In' (f :: Code i o) :: (i -> *) -> (o -> *) where
  In' :: In' f (Sum1 r (In' (F f) r)) o -> In' (F f) r o

... GHC complains:

    Kind mis-match
    The first argument of `F' should have kind `Code (Sum k0 k1) k1',
    but `f' has kind `Code i o'
    In the type `In' f (Sum1 r (In' (F f) r)) o'
    In the definition of data constructor In'
    In the data declaration for In'

Is there a good reason for the difference in behaviour? If so, is this something we should document?

[simonpj@…]

commit c91172004f2a5a6bf201b418c32c2d640ee34049

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Thu Jun 7 12:09:22 2012 +0100

    Support polymorphic kind recursion
    
    This is (I hope) the last major patch for kind polymorphism.
    The big new feature is polymorphic kind recursion when you
    supply a complete kind signature for a type constructor.
    (I've documented it in the user manual too.)
    
    This fixes Trac #6137, #6093, #6049.
    
    The patch also makes type/data families less polymorphic by default.
       data family T a
    now defaults to T :: * -> *
    If you want T :: forall k. k -> *, use
       data family T (a :: k)
    
    This defaulting to * is done whenever there is a
    "complete, user-specified kind signature", something that is
    carefully defined in the user manual.
    
    Hurrah!

 compiler/typecheck/TcBinds.lhs      |    3 +-
 compiler/typecheck/TcClassDcl.lhs   |   49 --------
 compiler/typecheck/TcHsType.lhs     |   50 ++++++--
 compiler/typecheck/TcInstDcls.lhs   |  106 +++++------------
 compiler/typecheck/TcRnDriver.lhs   |   66 ++++++++---
 compiler/typecheck/TcRnTypes.lhs    |   31 ++----
 compiler/typecheck/TcSplice.lhs     |    3 +-
 compiler/typecheck/TcTyClsDecls.lhs |  204 ++++++++++++++++++-------------
 docs/users_guide/flags.xml          |    5 +-
 docs/users_guide/glasgow_exts.xml   |  228 ++++++++++++++++++++++-------------
 10 files changed, 400 insertions(+), 345 deletions(-)