#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: |
---------------------------------------+------------------------------------
Comment(by goldfire):
The following code is another demonstration of (I believe) the same
underlying problem:
{{{
{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs,
ExistentialQuantification #-}
data Nat = Zero | Succ Nat
data family Sing (a :: k)
data instance Sing (a :: Nat) where
SZero :: Sing Zero
SSucc :: Sing n -> Sing (Succ n)
data instance Sing (a :: Maybe k) =
a ~ 'Nothing => SNothing
| forall b. a ~ 'Just b => SJust (Sing b)
term = SJust SZero
}}}
The last line fails with the following:
{{{
Couldn't match kind `k' against `Nat'
Kind incompatibility when matching types:
b0 :: k
'Zero :: Nat
In the first argument of `SJust', namely `SZero'
In the expression: SJust SZero
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6036#comment:1>
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
