Merge branch 'master' into atomics
[ghc.git] / testsuite / tests / simplCore / should_compile / T5329.hs
1 {-# LANGUAGE UnicodeSyntax #-}
2 {-# LANGUAGE EmptyDataDecls #-}
3 {-# LANGUAGE TypeOperators #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE GADTs #-}
6 {-# LANGUAGE TypeFamilies #-}
7 {-# LANGUAGE MultiParamTypeClasses #-}
8 {-# LANGUAGE FlexibleContexts #-}
9 {-# LANGUAGE FlexibleInstances #-}
10
11 module T5329 where
12
13 data PZero
14 data PSucc p
15
16 data Peano n where
17 PZero ∷ Peano PZero
18 PSucc ∷ IsPeano p ⇒ Peano p → Peano (PSucc p)
19
20 class IsPeano n where
21 peano ∷ Peano n
22
23 instance IsPeano PZero where
24 peano = PZero
25
26 instance IsPeano p ⇒ IsPeano (PSucc p) where
27 peano = PSucc peano
28
29 class (n ~ PSucc (PPred n)) ⇒ PHasPred n where
30 type PPred n
31
32 instance PHasPred (PSucc p) where
33 type PPred (PSucc p) = p
34
35 pPred ∷ Peano (PSucc p) → Peano p
36 pPred (PSucc p) = p
37
38 infixl 6 :+:
39
40 class (IsPeano n, IsPeano m, IsPeano (n :+: m), (n :+: m) ~ (m :+: n))
41 ⇒ PAdd n m where
42 type n :+: m
43
44 instance PAdd PZero PZero where
45 type PZero :+: PZero = PZero
46
47 instance IsPeano p ⇒ PAdd PZero (PSucc p) where
48 type PZero :+: (PSucc p) = PSucc p
49
50 instance IsPeano p ⇒ PAdd (PSucc p) PZero where
51 type (PSucc p) :+: PZero = PSucc p
52
53 instance (IsPeano n, IsPeano m, PAdd n m) ⇒ PAdd (PSucc n) (PSucc m) where
54 type (PSucc n) :+: (PSucc m) = PSucc (PSucc (n :+: m))
55
56 data PAddResult n m r where
57 PAddResult ∷ (PAdd n m, PAdd m n, (n :+: m) ~ r)
58 ⇒ PAddResult n m r
59
60 pAddLeftZero ∷ ∀ n . IsPeano n ⇒ PAddResult PZero n n
61 pAddLeftZero = case peano ∷ Peano n of
62 PZero → PAddResult
63 PSucc _ → PAddResult
64
65 pAddRightZero ∷ ∀ n . IsPeano n ⇒ PAddResult n PZero n
66 pAddRightZero = case peano ∷ Peano n of
67 PZero → PAddResult
68 PSucc _ → PAddResult
69
70 data PAddSucc n m where
71 PAddSucc ∷ (PAdd n m, PAdd m n,
72 PAdd (PSucc n) m, PAdd m (PSucc n),
73 PAdd n (PSucc m), PAdd (PSucc m) n,
74 (PSucc n :+: m) ~ PSucc (n :+: m),
75 (n :+: PSucc m) ~ PSucc (n :+: m))
76 ⇒ PAddSucc n m
77
78 pAddSucc ∷ ∀ n m . (IsPeano n, IsPeano m) ⇒ PAddSucc n m
79 pAddSucc = case (peano ∷ Peano n, peano ∷ Peano m) of
80 (PZero, PZero) → PAddSucc
81 (PZero, PSucc _)case pAddLeftZero ∷ PAddResult n (PPred m) (PPred m) of
82 PAddResult → PAddSucc
83 (PSucc _, PZero)case pAddRightZero ∷ PAddResult (PPred n) m (PPred n) of
84 PAddResult → PAddSucc
85 (PSucc _, PSucc _)case pAddSucc ∷ PAddSucc (PPred n) (PPred m) of
86 PAddSucc → PAddSucc
87
88 data PAdd2 n m where
89 PAdd2 ∷ (PAdd n m, PAdd m n) ⇒ PAdd2 n m
90
91 pAdd2 ∷ ∀ n m . (IsPeano n, IsPeano m) ⇒ PAdd2 n m
92 pAdd2 = case (peano ∷ Peano n, peano ∷ Peano m) of
93 (PZero, PZero) → PAdd2
94 (PZero, PSucc _) → PAdd2
95 (PSucc _, PZero) → PAdd2
96 (PSucc _, PSucc _)case pAdd2 ∷ PAdd2 (PPred n) (PPred m) of
97 PAdd2 → PAdd2
98
99 data PAdd3 n m k where
100 PAdd3 ∷ (PAdd n m, PAdd m k, PAdd m n, PAdd k m, PAdd n k, PAdd k n,
101 PAdd (n :+: m) k, PAdd k (m :+: n),
102 PAdd n (m :+: k), PAdd (m :+: k) n,
103 PAdd (n :+: k) m, PAdd m (n :+: k),
104 ((n :+: m) :+: k) ~ (n :+: (m :+: k)),
105 (m :+: (n :+: k)) ~ ((m :+: n) :+: k))
106 ⇒ PAdd3 n m k
107
108 pAdd3 ∷ ∀ n m k . (IsPeano n, IsPeano m, IsPeano k) ⇒ PAdd3 n m k
109 pAdd3 = case (peano ∷ Peano n, peano ∷ Peano m, peano ∷ Peano k) of
110 (PZero, PZero, PZero) → PAdd3
111 (PZero, PZero, PSucc _) → PAdd3
112 (PZero, PSucc _, PZero) → PAdd3
113 (PSucc _, PZero, PZero) → PAdd3
114 (PZero, PSucc _, PSucc _)
115 case pAdd2 ∷ PAdd2 (PPred m) (PPred k) of
116 PAdd2 → PAdd3
117 (PSucc _, PZero, PSucc _)
118 case pAdd2 ∷ PAdd2 (PPred n) (PPred k) of
119 PAdd2 → PAdd3
120 (PSucc _, PSucc _, PZero)
121 case pAdd2 ∷ PAdd2 (PPred n) (PPred m) of
122 PAdd2 → PAdd3
123 (PSucc _, PSucc _, PSucc _)
124 case pAdd3 ∷ PAdd3 (PPred n) (PPred m) (PPred k) of
125 PAdd3 → case pAddSucc ∷ PAddSucc (PPred n :+: PPred m) (PPred k) of
126 PAddSucc → case pAddSucc ∷ PAddSucc (PPred n :+: PPred k) (PPred m) of
127 PAddSucc → case pAddSucc ∷ PAddSucc (PPred m :+: PPred k) (PPred n) of
128 PAddSucc → PAdd3
129