Complete work on new OVERLAPPABLE/OVERLAPPING pragmas (Trac #9242)
[ghc.git] / testsuite / tests / indexed-types / should_fail / T5439.hs
1 {-# LANGUAGE UnicodeSyntax #-}
2 {-# LANGUAGE DeriveDataTypeable #-}
3 {-# LANGUAGE EmptyDataDecls #-}
4 {-# LANGUAGE TypeOperators #-}
5 {-# LANGUAGE ScopedTypeVariables #-}
6 {-# LANGUAGE RankNTypes #-}
7 {-# LANGUAGE GADTs #-}
8 {-# LANGUAGE TypeFamilies #-}
9 {-# LANGUAGE MultiParamTypeClasses #-}
10 {-# LANGUAGE FlexibleContexts #-}
11 {-# LANGUAGE FlexibleInstances #-}
12 {-# LANGUAGE UndecidableInstances #-}
13
14 module Main where
15
16 import Data.Typeable
17 import Control.Exception
18
19 data Attempt α = Success α
20 | ∀ e . Exception e ⇒ Failure e
21
22 data Inject f α = ∀ β . Inject (f β) (α → β)
23
24 class Completable f where
25 complete ∷ f α → α → IO Bool
26
27 instance Completable f ⇒ Completable (Inject f) where
28 complete (Inject f inj) = complete f . inj
29
30 class WaitOp op where
31 type WaitOpResult op
32 registerWaitOp ∷ Completable f
33 ⇒ op → f (Attempt (WaitOpResult op))IO Bool
34
35 data WaitOps rs where
36 WaitOp ∷ WaitOp op ⇒ op → WaitOps (HSingle (WaitOpResult op))
37 (:?)(WaitOp op, HNonEmpty rs)
38 ⇒ op → WaitOps rs → WaitOps (WaitOpResult op :* rs)
39
40 waitOpsNonEmpty ∷ ∀ rs . WaitOps rs → HNonEmptyInst rs
41 waitOpsNonEmpty (WaitOp _) = HNonEmptyInst
42 waitOpsNonEmpty (_ :? _) = HNonEmptyInst
43
44 infixr 7 .?
45 infix 8 .?.
46
47 (.?) ∷ WaitOp op ⇒ op → WaitOps rs → WaitOps (WaitOpResult op :* rs)
48 op .? ops = case waitOpsNonEmpty ops of
49 HNonEmptyInst → op :? ops
50
51 (.?.)(WaitOp op1, WaitOp op2) ⇒ op1 → op2
52 → WaitOps (WaitOpResult op1 :*: WaitOpResult op2)
53 op1 .?. op2 = op1 .? WaitOp op2
54
55 data NthException n e = NthException (Peano n) e deriving (Typeable, Show)
56
57 instance (Typeable n, Exception e) ⇒ Exception (NthException n e)
58
59 instance WaitOp (WaitOps rs) where
60 type WaitOpResult (WaitOps rs) = HElemOf rs
61 registerWaitOp ops ev =
62 let register ∷ ∀ n . HDropClass n rs
63Bool → Peano n → WaitOps (HDrop n rs)IO Bool
64 register first n (WaitOp op) = do
65 let inj n (Success r) = Success (HNth n r)
66 inj n (Failure e) = Failure (NthException n e)
67 t ← try $ registerWaitOp op (Inject ev $ inj n)
68 r ← case t of
69 Right r → return r
70 Left e → complete ev $ inj n $ Failure (e ∷ SomeException)
71 return $ r || not first
72 register first n (op :? ops') = do
73 let inj n (Success r) = Success (HNth n r)
74 inj n (Failure e) = Failure (NthException n e)
75 t ← try $ registerWaitOp op (Inject ev $ inj n)
76 case t of
77 Right Truecase waitOpsNonEmpty ops' of
78 HNonEmptyInst → case hTailDropComm ∷ HTailDropComm n rs of
79 HTailDropComm → register False (PSucc n) ops'
80 Right Falsereturn $ not first
81 Left e → do
82 c ← complete ev $ inj $ Failure (e ∷ SomeException)
83 return $ c || not first
84 in case waitOpsNonEmpty ops of
85 HNonEmptyInst → register True PZero ops
86
87 main = return ()
88
89 data PZero deriving Typeable
90 data PSucc p deriving Typeable
91
92 data Peano n where
93 PZero ∷ Peano PZero
94 PSucc ∷ IsPeano p ⇒ Peano p → Peano (PSucc p)
95
96 instance Show (Peano n) where
97 show n = show (peanoNum n ∷ Int)
98
99 peanoNum ∷ Num n ⇒ Peano p → n
100 peanoNum PZero = 0
101 peanoNum (PSucc p) = 1 + peanoNum p
102
103 class Typeable n ⇒ IsPeano n where
104 peano ∷ Peano n
105
106 instance IsPeano PZero where
107 peano = PZero
108
109 instance IsPeano p ⇒ IsPeano (PSucc p) where
110 peano = PSucc peano
111
112 class (n ~ PSucc (PPred n)) ⇒ PHasPred n where
113 type PPred n
114
115 instance PHasPred (PSucc p) where
116 type PPred (PSucc p) = p
117
118 pPred ∷ Peano (PSucc p) → Peano p
119 pPred (PSucc p) = p
120
121 infixr 7 :*, .*
122 infix 8 :*:, .*.
123
124 data HNil
125 data h :* t
126 type HSingle α = α :* HNil
127 type α :*: β = α :* β :* HNil
128
129 data HList l where
130 HNil ∷ HList HNil
131 (:*) ∷ HListClass t ⇒ h → HList t → HList (h :* t)
132
133 instance Show (HList HNil) where
134 show _ = "HNil"
135
136 instance (Show h, Show (HList t))Show (HList (h :* t)) where
137 showsPrec d (h :* t) = showParen (d > 7) $
138 showsPrec 8 h . showString " .* " . showsPrec 7 t
139
140 (.*) ∷ HListClass t ⇒ h → HList t → HList (h :* t)
141 (.*) = (:*)
142
143 (.*.) ∷ α → β → HList (α :*: β)
144 a .*. b = a .* b .* HNil
145
146 data HListWitness l where
147 HNilList ∷ HListWitness HNil
148 HConsList ∷ HListClass t ⇒ HListWitness (h :* t)
149
150 class HListClass l where
151 hListWitness ∷ HListWitness l
152
153 instance HListClass HNil where
154 hListWitness = HNilList
155
156 instance HListClass t ⇒ HListClass (h :* t) where
157 hListWitness = HConsList
158
159 data HListInst l where
160 HListInst ∷ HListClass l ⇒ HListInst l
161
162 hListInst ∷ HList l → HListInst l
163 hListInst HNil = HListInst
164 hListInst (_ :* _) = HListInst
165
166 class (l ~ (HHead l :* HTail l), HListClass (HTail l)) ⇒ HNonEmpty l where
167 type HHead l
168 type HTail l
169
170 instance HListClass t ⇒ HNonEmpty (h :* t) where
171 type HHead (h :* t) = h
172 type HTail (h :* t) = t
173
174 hHead ∷ HList (h :* t) → h
175 hHead (h :* _) = h
176
177 hTail ∷ HList (h :* t) → HList t
178 hTail (_ :* t) = t
179
180 data HNonEmptyInst l where
181 HNonEmptyInst ∷ HListClass t ⇒ HNonEmptyInst (h :* t)
182
183 data HDropWitness n l where
184 HDropZero ∷ HListClass l ⇒ HDropWitness PZero l
185 HDropSucc ∷ HDropClass p t ⇒ HDropWitness (PSucc p) (h :* t)
186
187 class (IsPeano n, HListClass l, HListClass (HDrop n l)) ⇒ HDropClass n l where
188 type HDrop n l
189 hDropWitness ∷ HDropWitness n l
190
191 instance HListClass l ⇒ HDropClass PZero l where
192 type HDrop PZero l = l
193 hDropWitness = HDropZero
194
195 instance HDropClass p t ⇒ HDropClass (PSucc p) (h :* t) where
196 type HDrop (PSucc p) (h :* t) = HDrop p t
197 hDropWitness = case hDropWitness ∷ HDropWitness p t of
198 HDropZero → HDropSucc
199 HDropSucc → HDropSucc
200
201 data HDropInst n l where
202 HDropInst ∷ HDropClass n l ⇒ HDropInst n l
203
204 hDrop ∷ ∀ n l . HDropClass n l ⇒ Peano n → HList l → HList (HDrop n l)
205 hDrop n l = case hDropWitness ∷ HDropWitness n l of
206 HDropZero → l
207 HDropSucc → hDrop (pPred n) (hTail l)
208
209 data HNonEmptyDropInst n l where
210 HNonEmptyDropInst ∷ (HDropClass n l, HNonEmpty l,
211 HDropClass (PSucc n) l, HNonEmpty (HDrop n l))
212 ⇒ HNonEmptyDropInst n l
213
214 pPrevDropInst ∷ ∀ n l . HDropClass (PSucc n) l ⇒ HNonEmptyDropInst n l
215 pPrevDropInst = case hDropWitness ∷ HDropWitness (PSucc n) l of
216 HDropSucc → case hDropWitness ∷ HDropWitness n (HTail l) of
217 HDropZero → HNonEmptyDropInst
218 HDropSucc → case pPrevDropInst ∷ HNonEmptyDropInst (PPred n) (HTail l) of
219 HNonEmptyDropInst → HNonEmptyDropInst
220
221 hNextDropInst ∷ ∀ n l . (HDropClass n l, HNonEmpty (HDrop n l))
222 ⇒ HNonEmptyDropInst n l
223 hNextDropInst = case hDropWitness ∷ HDropWitness n l of
224 HDropZero → HNonEmptyDropInst
225 HDropSucc → case hNextDropInst ∷ HNonEmptyDropInst (PPred n) (HTail l) of
226 HNonEmptyDropInst → HNonEmptyDropInst
227
228 data HTailDropComm n l where
229 HTailDropComm ∷ (HNonEmpty l, HDropClass n l,
230 HNonEmpty (HDrop n l), HDropClass n (HTail l),
231 HDropClass (PSucc n) l,
232 HTail (HDrop n l) ~ HDrop n (HTail l),
233 HDrop (PSucc n) l ~ HTail (HDrop n l),
234 HDrop (PSucc n) l ~ HDrop n (HTail l))
235 ⇒ HTailDropComm n l
236
237 hTailDropComm' ∷ ∀ n l . (HDropClass (PSucc n) l)
238 ⇒ HTailDropComm n l
239 hTailDropComm' = case pPrevDropInst ∷ HNonEmptyDropInst n l of
240 HNonEmptyDropInst → hTailDropComm
241
242 hTailDropComm ∷ ∀ n l . (HDropClass n l, HNonEmpty (HDrop n l))
243 ⇒ HTailDropComm n l
244 hTailDropComm = case hDropWitness ∷ HDropWitness n l of
245 HDropZero → HTailDropComm
246 HDropSucc → case hTailDropComm ∷ HTailDropComm (PPred n) (HTail l) of
247 HTailDropComm → HTailDropComm
248
249 type HNth n l = HHead (HDrop n l)
250
251 data HElemOf l where
252 HNth ∷ (HDropClass n l, HNonEmpty (HDrop n l))
253 ⇒ Peano n → HNth n l → HElemOf l
254