#6035: Kind-indexed type family failure with polymorphic kinds
------------------------------+---------------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.5 | Keywords: PolyKinds TypeFamilies
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------+---------------------------------------------
The following code fails to compile:
{{{
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs,
TypeOperators
#-}
data Nat = Zero | Succ Nat
type family Sing (a :: k) :: k -> *
data SNat n where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
data SList (a :: [k]) where
SNil :: SList '[]
SCons :: Sing h h -> SList t -> SList (h ': t)
type instance Sing (a :: Nat) = SNat
type instance Sing (a :: [k]) = SList
term :: SList '[ '[Zero], '[]]
term = SCons (SCons SZero SNil) (SCons SNil SNil)
}}}
The error generated is
{{{
/Users/rae/temp/Scratch.hs:27:15:
Couldn't match type `Sing [Nat] ((':) Nat 'Zero ('[] Nat))'
with `SList Nat'
Expected type: Sing
[Nat] ((':) Nat 'Zero ('[] Nat)) ((':) Nat 'Zero ('[]
Nat))
Actual type: SList Nat ((':) Nat 'Zero ('[] Nat))
In the return type of a call of `SCons'
In the first argument of `SCons', namely `(SCons SZero SNil)'
In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)
/Users/rae/temp/Scratch.hs:27:40:
Couldn't match type `Sing [Nat] ('[] Nat)' with `SList Nat'
Expected type: Sing [Nat] ('[] Nat) ('[] Nat)
Actual type: SList Nat ('[] Nat)
In the first argument of `SCons', namely `SNil'
In the second argument of `SCons', namely `(SCons SNil SNil)'
In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)
}}}
It seems that the {{{Sing}}} kind-indexed type family isn't quite working.
My guess is that the problem is that we really want, say, {{{Sing
'[Zero]}}} to be {{{SList Nat}}}, where {{{Nat}}} is the implicit kind
parameter to {{{SList}}}. But, we can't say that. I would hope that the
explicit kind annotation on the result of {{{Sing}}} would fix the
implicit kind parameter to {{{SList}}}, but it doesn't seem to.
This was tested on 7.5.20120420.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6035>
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
