id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
6137,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?",bug,closed,normal,,Compiler (Type checker),7.5,fixed,PolyKinds,,Unknown/Multiple,Unknown/Multiple,None/Unknown,Unknown,polykinds/T6137,,,