With dependent types, error reported in seemingly unrelated function
In doing some routine dependently typed hackery, I wrote the following:
{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, GADTs #-}
data Nat = Zero | Succ Nat
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
data HList :: [*] -> * where
HNil :: HList '[]
HCons :: h -> HList t -> HList (h ': t)
data Index :: Nat -> [*] -> * where
IZero :: Index Zero (h ': t)
ISucc :: Index n l -> Index (Succ n) (h ': l)
type family Lookup (n :: Nat) (l :: [*]) :: *
type instance Lookup Zero (h ': t) = h
type instance Lookup (Succ n) (h ': t) = Lookup n t
hLookup :: Index n l -> HList l -> Lookup n l
hLookup IZero (HCons h _) = h
hLookup (ISucc n) (HCons _ t) = hLookup n t
hLookup _ _ = undefined
So far, so good. But, I wanted a way to convert SNat
s to Index
es. When I add the (wrong) code below
sNatToIndex :: SNat n -> HList l -> Index n l
sNatToIndex SZero HNil = IZero
I get an error in the second clause of hLookup
, '''even though I haven't touched hLookup
'''. (I also get an error in sNatToIndex
, but that one's OK.)
The error is this:
/Users/rae/temp/Bug.hs:23:33:
Couldn't match type ‛t1’ with ‛Lookup n l’
‛t1’ is untouchable
inside the constraints (l ~ (':) * h1 t)
bound by a pattern with constructor
HCons :: forall h (t :: [*]). h -> HList t -> HList ((':) * h t),
in an equation for ‛hLookup’
at /Users/rae/temp/Bug.hs:23:20-28
Expected type: Lookup n l
Actual type: Lookup n1 l1
Relevant bindings include
hLookup :: Index n l -> HList l -> Lookup n l
(bound at /Users/rae/temp/Bug.hs:22:1)
In the expression: hLookup n t
In an equation for ‛hLookup’:
hLookup (ISucc n) (HCons _ t) = hLookup n t
This was tested with 7.7.20130528.
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |