Kind-indexed type family failure with polymorphic kinds
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.
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 |