Ticket #5395: CMP.hs

File CMP.hs, 767 bytes (added by guest, 4 years ago)

Haskell Source code with the tests

Line 
1{-# LANGUAGE TypeFamilies #-}
2
3module CMP where
4
5data Z = Z
6data S a = S a
7
8data HTrue
9data HFalse
10
11
12-- NAT -> NAT -> BOOL
13type family NatEQ x y :: *
14
15type instance NatEQ Z (S a) = HFalse
16type instance NatEQ (S a) Z = HFalse
17type instance NatEQ (S a) (S b) = NatEQ a b
18
19natEq :: a -> b -> NatEQ a b
20natEq _ _ = undefined
21
22n20 = S . S . S . S . S . S . S . S . S . S . S . S . S . S . S . S . S . S . S . S $ Z
23
24n21 = S n20
25
26-- This is OK
27t1 = natEq n20 n20
28
29-- t2 = natEq n20 n21
30{-
31the following, when uncommented, gives the following error:
32
33    Context reduction stack overflow; size = 21
34    Use -fcontext-stack=N to increase stack size to N
35      co :: NatEQ Z (S Z) ~ t0
36      co :: NatEQ (S Z) (S (S Z)) ~ t0
37      co :: NatEQ (S (S Z)) (S (S (S Z))) ~ t0
38
39-}