Different behaviour between a GADT and a data family with regards to kind unification
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?
Trac metadata
Trac field | Value |
---|---|
Version | 7.5 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |