#6036: Kind generalization fails in data family instance GADT
---------------------------------------+------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type
checker)
Version: 7.5 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------------+------------------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6036>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
