Kind generalization fails in data family instance GADT
The following code fails to compile:
{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs #-}
data family Sing (a :: k)
data instance Sing (a :: Maybe k) where
SNothing :: Sing 'Nothing
SJust :: Sing b -> Sing ('Just b)
The error is
Data constructor `SNothing' returns type `Sing
(Maybe k0) ('Nothing k0)'
instead of an instance of its parent type `Sing (Maybe k) a'
In the definition of data constructor `SNothing'
In the data instance declaration for `Sing'
It seems that the k
kind parameter is not being allowed to generalize over other kind parameters. The following (seemingly equivalent) formulation compiles:
{-# LANGUAGE ..., ExistentialQuantification #-}
data instance Sing (a :: Maybe k) =
a ~ 'Nothing => SNothing
| forall b. a ~ 'Just b => SJust (Sing b)
This was tested on 7.5.20120420.
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 |