Commit 8b054480 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.

Type families: T2219

parent f18c7113
{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators #-}
module Test where
data Zero
data Succ a
data FZ
data FS fn
data Fin n fn where
FZ :: Fin (Succ n) FZ
FS :: Fin n fn -> Fin (Succ n) (FS fn)
data Nil
data a ::: b
type family Lookup ts fn :: *
type instance Lookup (t ::: ts) FZ = t
type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn
data Tuple n ts where
Nil :: Tuple Zero Nil
(:::) :: t -> Tuple n ts -> Tuple (Succ n) (t ::: ts)
proj :: Fin n fn -> Tuple n ts -> Lookup ts fn
proj FZ (v ::: _) = v
proj (FS fn) (_ ::: vs) = proj fn vs
......@@ -116,3 +116,4 @@ test('T1981', normal, compile, [''])
test('T2238', normal, compile, [''])
test('OversatDecomp', normal, compile, [''])
test('T2219', normal, compile, [''])
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