Commit bab57202 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Test Trac #7967

parent 23331488
{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, GADTs #-}
module T7967 where
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, and got a bogus error above
sNatToIndex :: SNat n -> HList l -> Index n l
sNatToIndex SZero HNil = IZero
T7967.hs:31:26:
Couldn't match type ‛'[] *’ with ‛(':) * h0 t0’
Expected type: Index n l
Actual type: Index 'Zero ((':) * h0 t0)
In the expression: IZero
In an equation for ‛sNatToIndex’: sNatToIndex SZero HNil = IZero
......@@ -98,3 +98,4 @@ test('T7560', normal, compile_fail, [''])
test('T7729', normal, compile_fail, [''])
test('T7729a', normal, compile_fail, [''])
test('T7786', normal, compile_fail, [''])
test('T7967', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment