summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt/gadt-dim7.hs
blob: 0ea3633fa34f77ad3cbe8aafa0ee1bc8690e6ae7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
{-# LANGUAGE GADTs #-}

module ShouldSucceed4 where 

data Z 
data S a 


data Add n m r where 
  PZero :: Add Z m m 
  PSucc :: Add n m p -> Add (S n) m (S p) 


data XList n a where 
  XNil :: XList Z a  
  XCons :: a -> XList n a -> XList (S n) a 


-- simple safe append function 
append :: (Add n m r) -> XList n a -> XList m a -> XList r a 
append PZero XNil l = l 
append (PSucc prf) (XCons x xs) l = XCons x (append prf xs l)