newtype Age = Age Int deriving (Show)


--------------------------------------------------------
type Peq {[ * ]} t = t -> t -> Bool
type Peq {[ k -> l ]} t = forall a. Peq {[k]} a -> Peq {[ l ]} (t a)

peq {| t :: k |} :: Peq {[ k ]} t
peq {| Unit |} x y = True 
peq {| :+: |} peqA peqB (Inl x) (Inl y) =  peqA x y
peq {| :+: |} peqA peqB (Inr x) (Inr y) =  peqB x y
peq {| :+: |} peqA peqB  _       _      = False
peq {| :*: |} peqA peqB (x1 :*: y1)  (x2 :*: y2)   = peqA x1 x2 && peqB y1 y2 
peq {| Int |}     = (==)
peq {| Char |}    = (==)
peq {| Bool |}    = (==)
peq {| Con c|} peqA (Con a1) (Con a2) = peqA a1 a2
peq {| Label l|} peqA (Label a1) (Label a2) = peqA a1 a2
-- peq {| Age  |} (Age i) (Age j) = if i < 30 || j < 30 then i == j else True
 





--------------------------------------------------------
-- creating arbitrary datatypes

type Zero {[ * ]} t1 = t1
type Zero {[k -> l]} t1 = forall a. Zero {[k]} a -> Zero{[ l]} (t1 a)

zero {| t :: k |} :: Zero {[ k ]} t
zero {| Unit |} = Unit
zero {| Int  |} = 0
zero {| Char |} = '0'
zero {| :+:  |} zA zB = Inl zA
zero {| :*:  |} zA zB = (zA :*: zB)
zero {| (->) |} zA zB = \x -> zB
zero {| Con c|} zA = Con zA
zero {| Label l|} zA = Label zA


-----------------------------------------------------
-- printing types 

type Pt {[*]} = String
type Pt {[k -> l]} = Pt {[k]} -> Pt {[l]} 

pt {| t :: k |} :: Pt {[ k ]}
pt {| Unit |} = "Unit"
pt {| Int  |} = "Int"
pt {| Char |} = "Char"
pt {| :+:  |} zA zB = "(" ++ zA ++ ":+:" ++ zB ++ ")"
pt {| :*:  |} zA zB = "(" ++ zA ++ ":*:" ++ zB ++ ")"
pt {| (->) |} zA zB = "(" ++ zA ++ "->" ++ zB ++ ")"
pt {| Con c|}   zA = conName c ++ ":" ++ zA
pt {| Label c|} zB = labelType c

-----------------------------------------------------
-- printing terms

type Tostring {[*]} a = a -> String
type Tostring {[k -> l]} t = forall a. Tostring {[k]} a -> Tostring {[l]} (t a)
tostring {| t :: k |} :: Tostring {[ k ]} t

tostring {| Unit |} x = "Unit" 
tostring {| Int  |} i = show i
tostring {| Char |} c = show c
tostring {| :+:  |} zA zB (Inl x) = "Inl " ++ (zA x)
tostring {| :+:  |} zA zB (Inr x) = "Inr " ++ (zB x)
tostring {| :*:  |} zA zB (x :*: y) = "(" ++ (zA x) ++ ":*:" ++ (zB y) ++ ")"
tostring {| (->) |} zA zB f = "<function>"
tostring {| Con c|} zA (Con x) = conName c ++ " " ++ (zA x)
tostring {| Label c|} zA (Label x) = labelName c ++ "=" ++ (zA x)


data Fruit = Banana | Apple


main = 
  let ellie = Age 1
      steph = Age 32
      steve = Age 31
      
  in do print (pt {| Age |})
        print (pt {| Fruit |})
	print (tostring {| Fruit |} Banana)
        print (zero {|Age|})
	print (tostring {| Age |} ellie)
        print (peq {|Age|} ellie steve, 
	       peq {|Age|} steph ellie)