update baked in CoqPass.hs
[coq-hetmet.git] / build / CoqPass.hs
1 {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
2 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
3 where
4 import qualified Unique
5 import qualified Kind
6 import qualified UniqSupply
7 import qualified MkCore
8 import qualified TysWiredIn
9 import qualified TysPrim
10 import qualified Outputable
11 import qualified PrelNames
12 import qualified OccName
13 import qualified Name
14 import qualified Literal
15 import qualified Type
16 import qualified TypeRep
17 import qualified DataCon
18 import qualified TyCon
19 import qualified Coercion
20 import qualified Var
21 import qualified Id
22 import qualified Pair
23 import qualified FastString
24 import qualified BasicTypes
25 import qualified DataCon
26 import qualified CoreSyn
27 import qualified CoreUtils
28 import qualified Class
29 import qualified Data.Char 
30 import qualified Data.List
31 import qualified Data.Ord
32 import qualified Data.Typeable
33 import Data.Bits ((.&.), shiftL, (.|.))
34 import Prelude ( (++), (+), (==), Show, show, (.), ($) )
35 import qualified Prelude
36 import qualified GHC.Base
37 import qualified System.IO.Unsafe
38
39 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
40 getTyConTyVars tc =
41   if TyCon.isFunTyCon tc
42   then []
43   else if TyCon.isPrimTyCon tc
44        then []
45        else TyCon.tyConTyVars tc
46
47 cmpAlts :: (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> (CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var) -> Data.Ord.Ordering
48 cmpAlts (CoreSyn.DEFAULT,_,_) _   = Data.Ord.LT
49 cmpAlts _ (CoreSyn.DEFAULT,_,_)   = Data.Ord.GT
50 cmpAlts (a1,_,_) (a2,_,_)         = Data.Ord.compare a2 a1
51
52 sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
53 sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
54
55 coreVarToWeakVar :: Var.Var -> CoreVarToWeakVarResult
56 coreVarToWeakVar v | Id.isId     v = CVTWVR_EVar  (Var.varType v)
57 coreVarToWeakVar v | Var.isTyVar v = CVTWVR_TyVar (coreKindToKind (Var.varType v))
58 coreVarToWeakVar v | Coercion.isCoVar v = CVTWVR_CoVar (Prelude.fst (Coercion.coVarKind v)) (Prelude.snd (Coercion.coVarKind v))
59 coreVarToWeakVar _                 = Prelude.error "Var.Var that is neither an expression, type variable, nor coercion variable!"
60
61 rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
62 rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
63                   ,
64                    coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
65                    where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
66
67 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
68 tyConOrTyFun n =
69    if n == TysPrim.statePrimTyCon     -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
70    then Prelude.Right n
71    else if TyCon.isFamInstTyCon n
72         then Prelude.Right n
73         else if TyCon.isSynTyCon n
74              then Prelude.Right n
75              else Prelude.Left n
76
77 nat2int :: Nat -> Prelude.Int
78 nat2int O     = 0
79 nat2int (S x) = 1 + (nat2int x)
80
81 natToString :: Nat -> Prelude.String
82 natToString n = show (nat2int n)
83
84 sanitizeForLatex :: Prelude.String -> Prelude.String
85 sanitizeForLatex []      = []
86 sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x)
87 sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x)
88 sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x)
89 sanitizeForLatex (c:x)   = c:(sanitizeForLatex x)
90
91 kindToCoreKind :: Kind -> TypeRep.Kind
92 kindToCoreKind KindStar          = Kind.liftedTypeKind
93 kindToCoreKind (KindArrow k1 k2) = Kind.mkArrowKind (kindToCoreKind k1) (kindToCoreKind k2)
94 kindToCoreKind k                 = Prelude.error ((Prelude.++)
95                                                     "kindToCoreKind does not know how to handle kind "
96                                                                                (kindToString k))
97 coreKindToKind :: TypeRep.Kind -> Kind
98 coreKindToKind k =
99   case Kind.splitKindFunTy_maybe k of
100       Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
101       Prelude.Nothing -> 
102                       if (Kind.isLiftedTypeKind k)   then KindStar
103                  else if (Kind.isUnliftedTypeKind k) then KindStar
104                  else if (Kind.isArgTypeKind k)      then KindStar
105                  else if (Kind.isUbxTupleKind k)     then KindStar
106                  else if (Kind.isOpenTypeKind k)     then KindStar
107 --
108 -- The "subkinding" in GHC is not dealt with in System FC, and dealing
109 -- with it is not actually as simple as you'd think.
110 --
111 --                 else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType
112 --                 else if (Coercion.isOpenTypeKind k)     then KindOpenType
113 --                 else if (Coercion.isArgTypeKind k)      then KindArgType
114 --                 else if (Coercion.isUbxTupleKind k)     then KindUnboxedTuple
115 --
116                  else if (Kind.isTySuperKind k)      then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types"
117                  else                                         Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: "
118                                                                                (Outputable.showSDoc (Outputable.ppr k)))
119 outputableToString :: Outputable.Outputable a => a -> Prelude.String
120 outputableToString = (\x -> Outputable.showSDocDebug (Outputable.ppr x))
121
122 coreViewDeep :: Type.Type -> Type.Type
123 coreViewDeep t =
124     case t of
125       TypeRep.TyVarTy tv       -> TypeRep.TyVarTy tv
126       TypeRep.FunTy arg res    -> TypeRep.FunTy (coreViewDeep arg) (coreViewDeep res)
127       TypeRep.AppTy fun arg    -> TypeRep.AppTy (coreViewDeep fun) (coreViewDeep arg)
128       TypeRep.ForAllTy fun arg -> TypeRep.ForAllTy fun (coreViewDeep arg)
129       TypeRep.TyConApp tc tys  -> let t' = TypeRep.TyConApp tc (Prelude.map coreViewDeep tys)
130                         in case Type.coreView t' of
131                                Prelude.Nothing     -> t'
132                                Prelude.Just    t'' -> t''
133       TypeRep.PredTy p         -> case Type.coreView t of
134                                Prelude.Nothing     -> TypeRep.PredTy p
135                                Prelude.Just    t'  -> t'
136
137 {-# NOINLINE trace #-}
138 trace :: Prelude.String -> a -> a
139 trace msg x = x
140
141 --trace = Debug.Trace.trace
142 --trace msg x = x
143 --trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return x
144 --trace s x = x
145 --trace msg x = System.IO.Unsafe.unsafePerformIO $
146 --                (Prelude.>>=) (System.IO.hPutStrLn System.IO.stdout msg) (\_ -> Prelude.return x)
147 --trace msg x = System.IO.Unsafe.unsafePerformIO $
148 --                (Prelude.>>=) (System.IO.hPutStr System.IO.stdout " ") (\_ -> Prelude.return x)
149
150 -- I'm leaving this here (commented out) in case I ever need it again)
151 --checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool
152 --checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2)
153 {-# OPTIONS_GHC -cpp -fglasgow-exts #-}
154 {- For Hugs, use the option -F"cpp -P -traditional" -}
155
156
157
158 #ifdef __GLASGOW_HASKELL__
159 unsafeCoerce = GHC.Base.unsafeCoerce#
160 #else
161 -- HUGS
162 unsafeCoerce = IOExts.unsafeCoerce
163 #endif
164
165 __ = Prelude.error "Logical or arity value used"
166
167 false_rect :: a1
168 false_rect =
169   (trace "X" (Prelude.error "absurd case"))
170
171 eq_rect :: a1 -> a2 -> a1 -> a2
172 eq_rect x f y =
173   (trace "X" (f))
174
175 eq_rec :: a1 -> a2 -> a1 -> a2
176 eq_rec x f y =
177   (trace "X" ((trace "X" (eq_rect (trace "X" (x)) (trace "X" (f)) (trace "X" (y))))))
178
179 eq_rec_r :: a1 -> a2 -> a1 -> a2
180 eq_rec_r x h y =
181   (trace "X" ((trace "X" (eq_rec (trace "X" (x)) (trace "X" (h)) (trace "X" (y))))))
182
183 eq_rect_r :: a1 -> a2 -> a1 -> a2
184 eq_rect_r x h y =
185   (trace "X" ((trace "X" (eq_rect (trace "X" (x)) (trace "X" (h)) (trace "X" (y))))))
186
187 data Nat =
188    O
189  | S Nat
190
191 nat_rect :: a1 -> (Nat -> a1 -> a1) -> Nat -> a1
192 nat_rect f f0 n =
193   (trace "X" (case (trace "X" (n)) of {
194                O -> (trace "X" (f));
195                S n0 -> (trace "X" ((trace "X" (f0 (trace "X" (n0)) (trace "X" ((trace "X" ((nat_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (n0)))))))))))}))
196
197 nat_rec :: a1 -> (Nat -> a1 -> a1) -> Nat -> a1
198 nat_rec =
199   (trace "X" (nat_rect))
200
201 fst :: ((,) a1 a2) -> a1
202 fst p =
203   (trace "X" (case (trace "X" (p)) of {
204                (,) x y -> (trace "X" (x))}))
205
206 snd :: ((,) a1 a2) -> a2
207 snd p =
208   (trace "X" (case (trace "X" (p)) of {
209                (,) x y -> (trace "X" (y))}))
210
211 list_rect :: a2 -> (a1 -> (([]) a1) -> a2 -> a2) -> (([]) a1) -> a2
212 list_rect f f0 l =
213   (trace "X" (case (trace "X" (l)) of {
214                ([]) -> (trace "X" (f));
215                (:) y l0 -> (trace "X" ((trace "X" (f0 (trace "X" (y)) (trace "X" (l0)) (trace "X" ((trace "X" ((list_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (l0)))))))))))}))
216
217 list_rec :: a2 -> (a1 -> (([]) a1) -> a2 -> a2) -> (([]) a1) -> a2
218 list_rec =
219   (trace "X" (list_rect))
220
221 length :: (([]) a1) -> Nat
222 length l =
223   (trace "X" (case (trace "X" (l)) of {
224                ([]) -> (trace "X" (O));
225                (:) y l' -> (trace "X" (S (trace "X" ((trace "X" ((length (trace "X" (l')))))))))}))
226
227 app :: (([]) a1) -> (([]) a1) -> ([]) a1
228 app l m =
229   (trace "X" (case (trace "X" (l)) of {
230                ([]) -> (trace "X" (m));
231                (:) a l1 -> (trace "X" ((:) (trace "X" (a)) (trace "X" ((trace "X" ((app (trace "X" (l1)) (trace "X" (m)))))))))}))
232
233 type Sig a =
234   a
235   -- singleton inductive, whose constructor was exist
236   
237 data SigT a p =
238    ExistT a p
239
240 projT1 :: (SigT a1 a2) -> a1
241 projT1 x =
242   (trace "X" (case (trace "X" (x)) of {
243                ExistT a p -> (trace "X" (a))}))
244
245 projT2 :: (SigT a1 a2) -> a2
246 projT2 x =
247   (trace "X" (case (trace "X" (x)) of {
248                ExistT x0 h -> (trace "X" (h))}))
249
250 sumbool_rect :: (() -> a1) -> (() -> a1) -> Prelude.Bool -> a1
251 sumbool_rect f f0 s =
252   (trace "X" (case (trace "X" (s)) of {
253                Prelude.True -> (trace "X" ((trace "X" (f (trace "X" (__))))));
254                Prelude.False -> (trace "X" ((trace "X" (f0 (trace "X" (__))))))}))
255
256 sumbool_rec :: (() -> a1) -> (() -> a1) -> Prelude.Bool -> a1
257 sumbool_rec =
258   (trace "X" (sumbool_rect))
259
260 plus :: Nat -> Nat -> Nat
261 plus n m =
262   (trace "X" (case (trace "X" (n)) of {
263                O -> (trace "X" (m));
264                S p -> (trace "X" (S (trace "X" ((trace "X" ((plus (trace "X" (p)) (trace "X" (m)))))))))}))
265
266 eq_nat_dec :: Nat -> Nat -> Prelude.Bool
267 eq_nat_dec n =
268   (trace "X" ((trace "X" (nat_rec (trace "X" ((\m ->
269                             (trace "X" (case (trace "X" (m)) of {
270                                          O -> (trace "X" (Prelude.True));
271                                          S m0 -> (trace "X" (Prelude.False))}))))) (trace "X" ((\n0 iHn m ->
272                             (trace "X" (case (trace "X" (m)) of {
273                                          O -> (trace "X" (Prelude.False));
274                                          S m0 -> (trace "X" ((trace "X" (sumbool_rec (trace "X" ((\_ -> (trace "X" (Prelude.True))))) (trace "X" ((\_ -> (trace "X" (Prelude.False))))) (trace "X" ((trace "X" ((iHn (trace "X" (m0)))))))))))}))))) (trace "X" (n))))))
275
276 map :: (a1 -> a2) -> (([]) a1) -> ([]) a2
277 map f l =
278   (trace "X" (case (trace "X" (l)) of {
279                ([]) -> (trace "X" (([])));
280                (:) a t -> (trace "X" ((:) (trace "X" ((trace "X" ((f (trace "X" (a))))))) (trace "X" ((trace "X" ((map (trace "X" (f)) (trace "X" (t)))))))))}))
281
282 fold_left :: (a1 -> a2 -> a1) -> (([]) a2) -> a1 -> a1
283 fold_left f l a0 =
284   (trace "X" (case (trace "X" (l)) of {
285                ([]) -> (trace "X" (a0));
286                (:) b t -> (trace "X" ((trace "X" (fold_left (trace "X" (f)) (trace "X" (t)) (trace "X" ((trace "X" ((f (trace "X" (a0)) (trace "X" (b)))))))))))}))
287
288 fold_right :: (a2 -> a1 -> a1) -> a1 -> (([]) a2) -> a1
289 fold_right f a0 l =
290   (trace "X" (case (trace "X" (l)) of {
291                ([]) -> (trace "X" (a0));
292                (:) b t -> (trace "X" ((trace "X" (f (trace "X" (b)) (trace "X" ((trace "X" ((fold_right (trace "X" (f)) (trace "X" (a0)) (trace "X" (t)))))))))))}))
293
294 append :: Prelude.String -> Prelude.String -> Prelude.String
295 append s1 s2 =
296   (trace "X" (case (trace "X" (s1)) of {
297                [] -> (trace "X" (s2));
298                (:) c s1' -> (trace "X" ((:) (trace "X" (c)) (trace "X" ((trace "X" ((append (trace "X" (s1')) (trace "X" (s2)))))))))}))
299
300 type EqDecider t = t -> t -> Prelude.Bool
301
302 type EqDecidable t =
303   t -> t -> Prelude.Bool
304   -- singleton inductive, whose constructor was Build_EqDecidable
305   
306 eqd_dec :: (EqDecidable a1) -> a1 -> a1 -> Prelude.Bool
307 eqd_dec eqDecidable =
308   (trace "X" (eqDecidable))
309
310 eqDecidableOption :: (EqDecidable a1) -> EqDecidable (Prelude.Maybe a1)
311 eqDecidableOption eQDT v1 v2 =
312   (trace "X" (case (trace "X" (v1)) of {
313                Prelude.Just t ->
314                 (trace "X" (case (trace "X" (v2)) of {
315                              Prelude.Just t0 ->
316                               (trace "X" (let {s = (trace "X" ((trace "X" (eqd_dec (trace "X" (eQDT)) (trace "X" (t)) (trace "X" (t0))))))} in
317                                           (trace "X" (case (trace "X" (s)) of {
318                                                        Prelude.True -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (t0)) (trace "X" (Prelude.True)) (trace "X" (t))))));
319                                                        Prelude.False -> (trace "X" (Prelude.False))}))));
320                              Prelude.Nothing -> (trace "X" (Prelude.False))}));
321                Prelude.Nothing ->
322                 (trace "X" (case (trace "X" (v2)) of {
323                              Prelude.Just t -> (trace "X" (Prelude.False));
324                              Prelude.Nothing -> (trace "X" (Prelude.True))}))}))
325
326 type ToString t =
327   t -> Prelude.String
328   -- singleton inductive, whose constructor was Build_ToString
329   
330 toString :: (ToString a1) -> a1 -> Prelude.String
331 toString toString0 =
332   (trace "X" (toString0))
333
334 type Concatenable t =
335   t -> t -> t
336   -- singleton inductive, whose constructor was Build_Concatenable
337   
338 concatenate :: (Concatenable a1) -> a1 -> a1 -> a1
339 concatenate concatenable =
340   (trace "X" (concatenable))
341
342 concatenableString :: Concatenable Prelude.String
343 concatenableString =
344   (trace "X" (append))
345
346 data Tree a =
347    T_Leaf a
348  | T_Branch (Tree a) (Tree a)
349
350 tree_rect :: (a1 -> a2) -> ((Tree a1) -> a2 -> (Tree a1) -> a2 -> a2) -> (Tree a1) -> a2
351 tree_rect f f0 t =
352   (trace "X" (case (trace "X" (t)) of {
353                T_Leaf y -> (trace "X" ((trace "X" (f (trace "X" (y))))));
354                T_Branch t0 t1 -> (trace "X" ((trace "X" (f0 (trace "X" (t0)) (trace "X" ((trace "X" ((tree_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (t0))))))) (trace "X" (t1)) (trace "X" ((trace "X" ((tree_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (t1)))))))))))}))
355
356 mapTree :: (a1 -> a2) -> (Tree a1) -> Tree a2
357 mapTree f t =
358   (trace "X" (case (trace "X" (t)) of {
359                T_Leaf x -> (trace "X" (T_Leaf (trace "X" ((trace "X" ((f (trace "X" (x)))))))));
360                T_Branch l r -> (trace "X" (T_Branch (trace "X" ((trace "X" ((mapTree (trace "X" (f)) (trace "X" (l))))))) (trace "X" ((trace "X" ((mapTree (trace "X" (f)) (trace "X" (r)))))))))}))
361
362 mapOptionTree :: (a1 -> a2) -> (Tree (Prelude.Maybe a1)) -> Tree (Prelude.Maybe a2)
363 mapOptionTree f t =
364   (trace "X" (case (trace "X" (t)) of {
365                T_Leaf o ->
366                 (trace "X" (case (trace "X" (o)) of {
367                              Prelude.Just x -> (trace "X" (T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (x))))))))))));
368                              Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
369                T_Branch l r -> (trace "X" (T_Branch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (l))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (r)))))))))}))
370
371 mapOptionTreeAndFlatten :: (a1 -> Tree (Prelude.Maybe a2)) -> (Tree (Prelude.Maybe a1)) -> Tree (Prelude.Maybe a2)
372 mapOptionTreeAndFlatten f t =
373   (trace "X" (case (trace "X" (t)) of {
374                T_Leaf o ->
375                 (trace "X" (case (trace "X" (o)) of {
376                              Prelude.Just x -> (trace "X" ((trace "X" (f (trace "X" (x))))));
377                              Prelude.Nothing -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))))}));
378                T_Branch l r -> (trace "X" (T_Branch (trace "X" ((trace "X" ((mapOptionTreeAndFlatten (trace "X" (f)) (trace "X" (l))))))) (trace "X" ((trace "X" ((mapOptionTreeAndFlatten (trace "X" (f)) (trace "X" (r)))))))))}))
379
380 reduceTree :: a1 -> (a1 -> a1 -> a1) -> (Tree (Prelude.Maybe a1)) -> a1
381 reduceTree unit0 merge tt =
382   (trace "X" (case (trace "X" (tt)) of {
383                T_Leaf o ->
384                 (trace "X" (case (trace "X" (o)) of {
385                              Prelude.Just x -> (trace "X" (x));
386                              Prelude.Nothing -> (trace "X" (unit0))}));
387                T_Branch b1 b2 -> (trace "X" ((trace "X" (merge (trace "X" ((trace "X" ((reduceTree (trace "X" (unit0)) (trace "X" (merge)) (trace "X" (b1))))))) (trace "X" ((trace "X" ((reduceTree (trace "X" (unit0)) (trace "X" (merge)) (trace "X" (b2)))))))))))}))
388
389 leaves :: (Tree (Prelude.Maybe a1)) -> ([]) a1
390 leaves t =
391   (trace "X" (case (trace "X" (t)) of {
392                T_Leaf l ->
393                 (trace "X" (case (trace "X" (l)) of {
394                              Prelude.Just x -> (trace "X" ((:) (trace "X" (x)) (trace "X" (([])))));
395                              Prelude.Nothing -> (trace "X" (([])))}));
396                T_Branch l r -> (trace "X" ((trace "X" (app (trace "X" ((trace "X" ((leaves (trace "X" (l))))))) (trace "X" ((trace "X" ((leaves (trace "X" (r)))))))))))}))
397
398 unleaves :: (([]) a1) -> Tree (Prelude.Maybe a1)
399 unleaves l =
400   (trace "X" (case (trace "X" (l)) of {
401                ([]) -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))));
402                (:) a b -> (trace "X" (T_Branch (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (a)))))))) (trace "X" ((trace "X" ((unleaves (trace "X" (b)))))))))}))
403
404 unleaves' :: (([]) a1) -> Tree (Prelude.Maybe a1)
405 unleaves' l =
406   (trace "X" (case (trace "X" (l)) of {
407                ([]) -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))));
408                (:) a b -> (trace "X" (T_Branch (trace "X" ((trace "X" ((unleaves' (trace "X" (b))))))) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (a))))))))))}))
409
410 filter :: (([]) (Prelude.Maybe a1)) -> ([]) a1
411 filter l =
412   (trace "X" (case (trace "X" (l)) of {
413                ([]) -> (trace "X" (([])));
414                (:) o b ->
415                 (trace "X" (case (trace "X" (o)) of {
416                              Prelude.Just x -> (trace "X" ((:) (trace "X" (x)) (trace "X" ((trace "X" ((filter (trace "X" (b)))))))));
417                              Prelude.Nothing -> (trace "X" ((trace "X" (filter (trace "X" (b))))))}))}))
418
419 in_decidable :: (EqDecidable a1) -> a1 -> (([]) a1) -> Prelude.Bool
420 in_decidable eqdVV v lv =
421   (trace "X" ((trace "X" (list_rec (trace "X" (Prelude.False)) (trace "X" ((\a lv0 iHlv ->
422                             (trace "X" (case (trace "X" (iHlv)) of {
423                                          Prelude.True -> (trace "X" (Prelude.True));
424                                          Prelude.False ->
425                                           (trace "X" (let {dec = (trace "X" ((trace "X" (eqd_dec (trace "X" (eqdVV)) (trace "X" (v)) (trace "X" (a))))))} in
426                                                       (trace "X" (case (trace "X" (dec)) of {
427                                                                    Prelude.True -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (a)) (trace "X" ((\_ -> (trace "X" (Prelude.True))))) (trace "X" (v)) (trace "X" (__))))));
428                                                                    Prelude.False -> (trace "X" (Prelude.False))}))))}))))) (trace "X" (lv))))))
429
430 distinct_decidable :: (EqDecidable a1) -> (([]) a1) -> Prelude.Bool
431 distinct_decidable eqdVV lv =
432   (trace "X" ((trace "X" (list_rec (trace "X" (Prelude.True)) (trace "X" ((\a lv0 iHlv ->
433                             (trace "X" (case (trace "X" (iHlv)) of {
434                                          Prelude.True ->
435                                           (trace "X" (let {dec = (trace "X" ((trace "X" (in_decidable (trace "X" (eqdVV)) (trace "X" (a)) (trace "X" (lv0))))))} in
436                                                       (trace "X" (case (trace "X" (dec)) of {
437                                                                    Prelude.True -> (trace "X" (Prelude.False));
438                                                                    Prelude.False -> (trace "X" (Prelude.True))}))));
439                                          Prelude.False -> (trace "X" (Prelude.False))}))))) (trace "X" (lv))))))
440
441 list_eq_dec :: (([]) a1) -> (([]) a1) -> (a1 -> a1 -> Prelude.Bool) -> Prelude.Bool
442 list_eq_dec l1 =
443   (trace "X" ((trace "X" (list_rect (trace "X" ((\l2 dec ->
444                             (trace "X" (case (trace "X" (l2)) of {
445                                          ([]) -> (trace "X" (Prelude.True));
446                                          (:) t l3 -> (trace "X" (Prelude.False))}))))) (trace "X" ((\a l2 iHl1 l3 dec ->
447                             (trace "X" (case (trace "X" (l3)) of {
448                                          ([]) -> (trace "X" (Prelude.False));
449                                          (:) b l4 ->
450                                           (trace "X" (let {eqx = (trace "X" ((trace "X" (iHl1 (trace "X" (l4)) (trace "X" (dec))))))} in
451                                                       (trace "X" (case (trace "X" (eqx)) of {
452                                                                    Prelude.True ->
453                                                                     (trace "X" ((trace "X" (eq_rect_r (trace "X" (l4)) (trace "X" ((\iHl2 ->
454                                                                                               (trace "X" (let {eqy = (trace "X" ((trace "X" (dec (trace "X" (a)) (trace "X" (b))))))} in
455                                                                                                           (trace "X" (case (trace "X" (eqy)) of {
456                                                                                                                        Prelude.True -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (b)) (trace "X" (Prelude.True)) (trace "X" (a))))));
457                                                                                                                        Prelude.False -> (trace "X" (Prelude.False))}))))))) (trace "X" (l2)) (trace "X" (iHl1))))));
458                                                                    Prelude.False -> (trace "X" (Prelude.False))}))))}))))) (trace "X" (l1))))))
459
460 eqDecidableList :: (EqDecidable a1) -> EqDecidable (([]) a1)
461 eqDecidableList eqd v1 v2 =
462   (trace "X" ((trace "X" (list_eq_dec (trace "X" (v1)) (trace "X" (v2)) (trace "X" ((trace "X" ((eqd_dec (trace "X" (eqd)))))))))))
463
464 data TreeFlags t =
465    Tf_leaf_true t
466  | Tf_leaf_false t
467  | Tf_branch (Tree t) (Tree t) (TreeFlags t) (TreeFlags t)
468
469 mkFlags :: (a1 -> Prelude.Bool) -> (Tree a1) -> TreeFlags a1
470 mkFlags f t =
471   (trace "X" (case (trace "X" (t)) of {
472                T_Leaf x ->
473                 (trace "X" (case (trace "X" ((trace "X" (f (trace "X" (x)))))) of {
474                              Prelude.True -> (trace "X" (Tf_leaf_true (trace "X" (x))));
475                              Prelude.False -> (trace "X" (Tf_leaf_false (trace "X" (x))))}));
476                T_Branch b1 b2 -> (trace "X" (Tf_branch (trace "X" (b1)) (trace "X" (b2)) (trace "X" ((trace "X" ((mkFlags (trace "X" (f)) (trace "X" (b1))))))) (trace "X" ((trace "X" ((mkFlags (trace "X" (f)) (trace "X" (b2)))))))))}))
477
478 dropT :: (Tree (Prelude.Maybe a1)) -> (TreeFlags (Prelude.Maybe a1)) -> Tree (Prelude.Maybe a1)
479 dropT __U03a3_ tf =
480   (trace "X" (case (trace "X" (tf)) of {
481                Tf_leaf_true x -> (trace "X" (T_Leaf (trace "X" (Prelude.Nothing))));
482                Tf_leaf_false x -> (trace "X" (__U03a3_));
483                Tf_branch b1 b2 tb1 tb2 -> (trace "X" (T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (b1)) (trace "X" (tb1))))))) (trace "X" ((trace "X" ((dropT (trace "X" (b2)) (trace "X" (tb2)))))))))}))
484
485 liftBoolFunc :: Prelude.Bool -> (a1 -> Prelude.Bool) -> (Prelude.Maybe a1) -> Prelude.Bool
486 liftBoolFunc b f t =
487   (trace "X" (case (trace "X" (t)) of {
488                Prelude.Just x -> (trace "X" ((trace "X" (f (trace "X" (x))))));
489                Prelude.Nothing -> (trace "X" (b))}))
490
491 tree_eq_dec :: (Tree a1) -> (Tree a1) -> (a1 -> a1 -> Prelude.Bool) -> Prelude.Bool
492 tree_eq_dec l1 =
493   (trace "X" ((trace "X" (tree_rect (trace "X" ((\a l2 dec ->
494                             (trace "X" (case (trace "X" (l2)) of {
495                                          T_Leaf t ->
496                                           (trace "X" (let {s = (trace "X" ((trace "X" (dec (trace "X" (a)) (trace "X" (t))))))} in
497                                                       (trace "X" (case (trace "X" (s)) of {
498                                                                    Prelude.True -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (t)) (trace "X" (Prelude.True)) (trace "X" (a))))));
499                                                                    Prelude.False -> (trace "X" (Prelude.False))}))));
500                                          T_Branch l2_1 l2_2 -> (trace "X" (Prelude.False))}))))) (trace "X" ((\l1_1 iHl1_1 l1_2 iHl1_2 l2 dec ->
501                             (trace "X" (case (trace "X" (l2)) of {
502                                          T_Leaf t -> (trace "X" (Prelude.False));
503                                          T_Branch l2_1 l2_2 ->
504                                           (trace "X" (let {s = (trace "X" ((trace "X" (iHl1_1 (trace "X" (l2_1)) (trace "X" (dec))))))} in
505                                                       (trace "X" (case (trace "X" (s)) of {
506                                                                    Prelude.True ->
507                                                                     (trace "X" (let {s0 = (trace "X" ((trace "X" (iHl1_2 (trace "X" (l2_2)) (trace "X" (dec))))))} in
508                                                                                 (trace "X" (case (trace "X" (s0)) of {
509                                                                                              Prelude.True -> (trace "X" ((trace "X" (eq_rect_r (trace "X" (l2_2)) (trace "X" ((\iHl1_3 -> (trace "X" ((trace "X" (eq_rect_r (trace "X" (l2_1)) (trace "X" ((\iHl1_4 -> (trace "X" (Prelude.True))))) (trace "X" (l1_1)) (trace "X" (iHl1_1))))))))) (trace "X" (l1_2)) (trace "X" (iHl1_2))))));
510                                                                                              Prelude.False -> (trace "X" ((trace "X" (eq_rect_r (trace "X" (l2_1)) (trace "X" ((\iHl1_3 -> (trace "X" (Prelude.False))))) (trace "X" (l1_1)) (trace "X" (iHl1_1))))))}))));
511                                                                    Prelude.False ->
512                                                                     (trace "X" (let {s0 = (trace "X" ((trace "X" (iHl1_2 (trace "X" (l2_2)) (trace "X" (dec))))))} in
513                                                                                 (trace "X" (case (trace "X" (s0)) of {
514                                                                                              Prelude.True -> (trace "X" ((trace "X" (eq_rect_r (trace "X" (l2_2)) (trace "X" ((\iHl1_3 -> (trace "X" (Prelude.False))))) (trace "X" (l1_2)) (trace "X" (iHl1_2))))));
515                                                                                              Prelude.False -> (trace "X" (Prelude.False))}))))}))))}))))) (trace "X" (l1))))))
516
517 eqDecidableTree :: (EqDecidable a1) -> EqDecidable (Tree a1)
518 eqDecidableTree eqd v1 v2 =
519   (trace "X" ((trace "X" (tree_eq_dec (trace "X" (v1)) (trace "X" (v2)) (trace "X" ((trace "X" ((eqd_dec (trace "X" (eqd)))))))))))
520
521 data Vec a =
522    Vec_nil
523  | Vec_cons Nat a (Vec a)
524
525 vec2list :: Nat -> (Vec a1) -> ([]) a1
526 vec2list n v =
527   (trace "X" (case (trace "X" (v)) of {
528                Vec_nil -> (trace "X" (([])));
529                Vec_cons n0 a va -> (trace "X" ((:) (trace "X" (a)) (trace "X" ((trace "X" ((vec2list (trace "X" (n0)) (trace "X" (va)))))))))}))
530
531 vec_zip :: Nat -> (Vec a1) -> (Vec a2) -> Vec ((,) a1 a2)
532 vec_zip n va vb =
533   (trace "X" ((trace "X" (nat_rect (trace "X" ((\va0 vb0 -> (trace "X" (Vec_nil))))) (trace "X" ((\n0 iHn va0 vb0 ->
534                             (trace "X" (case (trace "X" (va0)) of {
535                                          Vec_nil -> (trace "X" (false_rect));
536                                          Vec_cons n1 x x0 ->
537                                           (trace "X" ((trace "X" (eq_rect (trace "X" (n0)) (trace "X" ((\x1 x2 ->
538                                                                     (trace "X" (case (trace "X" (vb0)) of {
539                                                                                  Vec_nil -> (trace "X" (false_rect));
540                                                                                  Vec_cons n2 x3 x4 -> (trace "X" ((trace "X" (eq_rect (trace "X" (n0)) (trace "X" ((\x5 x6 -> (trace "X" (Vec_cons (trace "X" (n0)) (trace "X" (((,) (trace "X" (x1)) (trace "X" (x5))))) (trace "X" ((trace "X" ((iHn (trace "X" (x2)) (trace "X" (x6)))))))))))) (trace "X" (n2)) (trace "X" (x3)) (trace "X" (x4))))))}))))) (trace "X" (n1)) (trace "X" (x)) (trace "X" (x0))))))}))))) (trace "X" (n)) (trace "X" (va)) (trace "X" (vb))))))
541
542 vec_map :: Nat -> (a1 -> a2) -> (Vec a1) -> Vec a2
543 vec_map n f v =
544   (trace "X" ((trace "X" (nat_rect (trace "X" ((\v0 -> (trace "X" (Vec_nil))))) (trace "X" ((\n0 iHn v0 ->
545                             (trace "X" (case (trace "X" (v0)) of {
546                                          Vec_nil -> (trace "X" (false_rect));
547                                          Vec_cons n1 x x0 -> (trace "X" ((trace "X" (eq_rect (trace "X" (n0)) (trace "X" ((\x1 x2 -> (trace "X" (Vec_cons (trace "X" (n0)) (trace "X" ((trace "X" ((f (trace "X" (x1))))))) (trace "X" ((trace "X" ((iHn (trace "X" (x2)))))))))))) (trace "X" (n1)) (trace "X" (x)) (trace "X" (x0))))))}))))) (trace "X" (n)) (trace "X" (v))))))
548
549 list2vec :: (([]) a1) -> Vec a1
550 list2vec l =
551   (trace "X" ((trace "X" (list_rect (trace "X" (Vec_nil)) (trace "X" ((\a l0 iHl -> (trace "X" (Vec_cons
552                             (trace "X" ((trace "X" ((let {
553                                                       length0 l1 =
554                                                         (trace "X" (case (trace "X" (l1)) of {
555                                                                      ([]) -> (trace "X" (O));
556                                                                      (:) y l' -> (trace "X" (S (trace "X" ((trace "X" ((length0 (trace "X" (l')))))))))}))}
557                                                      in length0 (trace "X" (l0))))))) (trace "X" (a)) (trace "X" (iHl))))))) (trace "X" (l))))))
558
559 vec_chop' :: (([]) a1) -> (([]) a1) -> (Vec a2) -> Vec a2
560 vec_chop' l1 l2 v =
561   (trace "X" ((trace "X" (list_rect (trace "X" ((\v0 -> (trace "X" (v0))))) (trace "X" ((\a l3 iHl1 v0 ->
562                             (trace "X" ((trace "X" (iHl1
563                                                       (trace "X" ((case (trace "X" (v0)) of {
564                                                                     Vec_nil -> (trace "X" (false_rect));
565                                                                     Vec_cons n x x0 -> (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((length (trace "X" ((trace "X" ((app (trace "X" (l3)) (trace "X" (l2)))))))))))) (trace "X" ((\x1 x2 -> (trace "X" (x2))))) (trace "X" (n)) (trace "X" (x)) (trace "X" (x0))))))})))))))))) (trace "X" (l1)) (trace "X" (v))))))
566
567 data IList i f =
568    INil
569  | ICons i (([]) i) f (IList i f)
570
571 ilist_head :: a1 -> (([]) a1) -> (IList a1 a2) -> a2
572 ilist_head x y il =
573   (trace "X" (case (trace "X" (il)) of {
574                INil -> (trace "X" (false_rect));
575                ICons i is x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (x)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (y)) (trace "X" ((\x2 x3 -> (trace "X" (x2))))) (trace "X" (is))))))))) (trace "X" (i)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))}))
576
577 ilist_tail :: a1 -> (([]) a1) -> (IList a1 a2) -> IList a1 a2
578 ilist_tail x y il =
579   (trace "X" (case (trace "X" (il)) of {
580                INil -> (trace "X" (false_rect));
581                ICons i is x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (x)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (y)) (trace "X" ((\x2 x3 -> (trace "X" (x3))))) (trace "X" (is))))))))) (trace "X" (i)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))}))
582
583 ilmap :: (([]) a1) -> (a1 -> a2 -> a3) -> (IList a1 a2) -> IList a1 a3
584 ilmap il f =
585   (trace "X" ((trace "X" (list_rect (trace "X" ((\x -> (trace "X" (INil))))) (trace "X" ((\a il0 iHil x ->
586                             (trace "X" (case (trace "X" (x)) of {
587                                          INil -> (trace "X" (false_rect));
588                                          ICons i is x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (il0)) (trace "X" ((\x2 x3 -> (trace "X" (ICons (trace "X" (a)) (trace "X" (il0)) (trace "X" ((trace "X" ((f (trace "X" (a)) (trace "X" (x2))))))) (trace "X" ((trace "X" ((iHil (trace "X" (x3)))))))))))) (trace "X" (is))))))))) (trace "X" (i)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))}))))) (trace "X" (il))))))
589
590 ilist_chop :: (([]) a1) -> (([]) a1) -> (IList a1 a2) -> IList a1 a2
591 ilist_chop l1 l2 v =
592   (trace "X" ((trace "X" (list_rect (trace "X" ((\v0 -> (trace "X" (INil))))) (trace "X" ((\a l3 iHl1 v0 -> (trace "X" (ICons (trace "X" (a)) (trace "X" (l3))
593                             (trace "X" ((case (trace "X" (v0)) of {
594                                           INil -> (trace "X" (false_rect));
595                                           ICons i is x x0 -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((app (trace "X" (l3)) (trace "X" (l2))))))) (trace "X" ((\x1 x2 -> (trace "X" (x1))))) (trace "X" (is))))))))) (trace "X" (i)) (trace "X" (__)) (trace "X" (x)) (trace "X" (x0))))))})))
596                             (trace "X" ((trace "X" ((iHl1
597                                                       (trace "X" ((case (trace "X" (v0)) of {
598                                                                     INil -> (trace "X" (false_rect));
599                                                                     ICons i is x x0 -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((app (trace "X" (l3)) (trace "X" (l2))))))) (trace "X" ((\x1 x2 -> (trace "X" (x2))))) (trace "X" (is))))))))) (trace "X" (i)) (trace "X" (__)) (trace "X" (x)) (trace "X" (x0))))))}))))))))))))) (trace "X" (l1)) (trace "X" (v))))))
600
601 ilist_chop' :: (([]) a1) -> (([]) a1) -> (IList a1 a2) -> IList a1 a2
602 ilist_chop' l1 l2 v =
603   (trace "X" ((trace "X" (list_rect (trace "X" ((\v0 -> (trace "X" (v0))))) (trace "X" ((\a l3 iHl1 v0 ->
604                             (trace "X" ((trace "X" (iHl1
605                                                       (trace "X" ((case (trace "X" (v0)) of {
606                                                                     INil -> (trace "X" (false_rect));
607                                                                     ICons i is x x0 -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((app (trace "X" (l3)) (trace "X" (l2))))))) (trace "X" ((\x1 x2 -> (trace "X" (x2))))) (trace "X" (is))))))))) (trace "X" (i)) (trace "X" (__)) (trace "X" (x)) (trace "X" (x0))))))})))))))))) (trace "X" (l1)) (trace "X" (v))))))
608
609 ilist_to_list :: (([]) a1) -> (IList a1 a2) -> ([]) a2
610 ilist_to_list l il =
611   (trace "X" (case (trace "X" (il)) of {
612                INil -> (trace "X" (([])));
613                ICons i is a b -> (trace "X" ((:) (trace "X" (a)) (trace "X" ((trace "X" ((ilist_to_list (trace "X" (is)) (trace "X" (b)))))))))}))
614
615 data ITree i f =
616    INone
617  | ILeaf i f
618  | IBranch (Tree (Prelude.Maybe i)) (Tree (Prelude.Maybe i)) (ITree i f) (ITree i f)
619
620 iTree_rect :: a3 -> (a1 -> a2 -> a3) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (ITree a1 a2) -> a3 -> (ITree a1 a2) -> a3 -> a3) -> (Tree (Prelude.Maybe a1)) -> (ITree a1 a2) -> a3
621 iTree_rect f f0 f1 t i =
622   (trace "X" (case (trace "X" (i)) of {
623                INone -> (trace "X" (f));
624                ILeaf i0 y -> (trace "X" ((trace "X" (f0 (trace "X" (i0)) (trace "X" (y))))));
625                IBranch it1 it2 i0 i1 -> (trace "X" ((trace "X" (f1 (trace "X" (it1)) (trace "X" (it2)) (trace "X" (i0)) (trace "X" ((trace "X" ((iTree_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (it1)) (trace "X" (i0))))))) (trace "X" (i1)) (trace "X" ((trace "X" ((iTree_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (it2)) (trace "X" (i1)))))))))))}))
626
627 itmap :: (Tree (Prelude.Maybe a1)) -> (a1 -> a2 -> a3) -> (ITree a1 a2) -> ITree a1 a3
628 itmap il f =
629   (trace "X" ((trace "X" (tree_rect (trace "X" ((\a x ->
630                             (trace "X" (case (trace "X" (a)) of {
631                                          Prelude.Just i -> (trace "X" (ILeaf (trace "X" (i))
632                                           (trace "X" ((trace "X" ((f (trace "X" (i))
633                                                                     (trace "X" ((case (trace "X" (x)) of {
634                                                                                   INone -> (trace "X" (false_rect));
635                                                                                   ILeaf i0 x0 -> (trace "X" ((trace "X" (eq_rect (trace "X" (i)) (trace "X" ((\x1 -> (trace "X" (x1))))) (trace "X" (i0)) (trace "X" (x0))))));
636                                                                                   IBranch it1 it2 x0 x1 -> (trace "X" ((trace "X" (false_rect (trace "X" (x0)) (trace "X" (x1))))))}))))))))));
637                                          Prelude.Nothing -> (trace "X" (INone))}))))) (trace "X" ((\il1 iHil1 il2 iHil2 x -> (trace "X" (IBranch (trace "X" (il1)) (trace "X" (il2))
638                             (trace "X" ((case (trace "X" (x)) of {
639                                           INone -> (trace "X" (false_rect));
640                                           ILeaf i x0 -> (trace "X" ((trace "X" (false_rect (trace "X" (x0))))));
641                                           IBranch it1 it2 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (il1)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (il2)) (trace "X" ((\x2 x3 -> (trace "X" ((trace "X" (iHil1 (trace "X" (x2))))))))) (trace "X" (it2))))))))) (trace "X" (it1)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))})))
642                             (trace "X" ((case (trace "X" (x)) of {
643                                           INone -> (trace "X" (false_rect));
644                                           ILeaf i x0 -> (trace "X" ((trace "X" (false_rect (trace "X" (x0))))));
645                                           IBranch it1 it2 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (il1)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (il2)) (trace "X" ((\x2 x3 -> (trace "X" ((trace "X" (iHil2 (trace "X" (x3))))))))) (trace "X" (it2))))))))) (trace "X" (it1)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))})))))))) (trace "X" (il))))))
646
647 bnot :: Prelude.Bool -> Prelude.Bool
648 bnot b =
649   (trace "X" (case (trace "X" (b)) of {
650                Prelude.True -> (trace "X" (Prelude.False));
651                Prelude.False -> (trace "X" (Prelude.True))}))
652
653 eol :: Prelude.String
654 eol = '\n':[]
655
656 data Monad t =
657    Build_Monad (() -> () -> t) (() -> () -> t -> (() -> t) -> t)
658
659 returnM :: (Monad a1) -> a2 -> a1
660 returnM monad x =
661   (trace "X" (case (trace "X" (monad)) of {
662                Build_Monad returnM0 bindM0 -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (returnM0)) (trace "X" (__)) (trace "X" (x))))))}))
663
664 bindM :: (Monad a1) -> a1 -> (a2 -> a1) -> a1
665 bindM monad x x0 =
666   (trace "X" (case (trace "X" (monad)) of {
667                Build_Monad returnM0 bindM0 -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (bindM0)) (trace "X" (__)) (trace "X" (__)) (trace "X" (x)) (trace "X" (x0))))))}))
668
669 data OrError t =
670    Error Prelude.String
671  | OK t
672
673 orErrorBind :: (OrError a1) -> (a1 -> OrError a2) -> OrError a2
674 orErrorBind oe f =
675   (trace "X" (case (trace "X" (oe)) of {
676                Error s -> (trace "X" (Error (trace "X" (s))));
677                OK t -> (trace "X" ((trace "X" (f (trace "X" (t))))))}))
678
679 orErrorBindWithMessage :: (OrError a1) -> (a1 -> OrError a2) -> Prelude.String -> OrError a2
680 orErrorBindWithMessage oe f err_msg =
681   (trace "X" (case (trace "X" (oe)) of {
682                Error s -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (err_msg)) (trace "X" (eol))))))) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))) (trace "X" (s)))))))));
683                OK t -> (trace "X" ((trace "X" (f (trace "X" (t))))))}))
684
685 addErrorMessage :: Prelude.String -> (OrError a1) -> OrError a1
686 addErrorMessage s x =
687   (trace "X" ((trace "X" (orErrorBindWithMessage (trace "X" (x)) (trace "X" ((\y -> (trace "X" (OK (trace "X" (y))))))) (trace "X" (s))))))
688
689 eqDecidableNat :: EqDecidable Nat
690 eqDecidableNat v1 v2 =
691   (trace "X" ((trace "X" (eq_nat_dec (trace "X" (v1)) (trace "X" (v2))))))
692
693 list2vecOrFail :: (([]) a1) -> Nat -> (Nat -> Nat -> Prelude.String) -> OrError (Vec a1)
694 list2vecOrFail l n error_message =
695   (trace "X" (let {v = (trace "X" ((trace "X" (list2vec (trace "X" (l))))))} in
696               (trace "X" (let {s = (trace "X" ((trace "X" (eqd_dec (trace "X" (eqDecidableNat)) (trace "X" ((trace "X" ((length (trace "X" (l))))))) (trace "X" (n))))))} in
697                           (trace "X" (case (trace "X" (s)) of {
698                                        Prelude.True -> (trace "X" (let {v0 = (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((length (trace "X" (l))))))) (trace "X" (v)) (trace "X" (n))))))} in (trace "X" (OK (trace "X" (v0))))));
699                                        Prelude.False -> (trace "X" (Error (trace "X" ((trace "X" ((error_message (trace "X" ((trace "X" ((length (trace "X" (l))))))) (trace "X" (n)))))))))}))))))
700
701 split_list :: (([]) a1) -> Nat -> OrError ((,) (([]) a1) (([]) a1))
702 split_list l n =
703   (trace "X" (case (trace "X" (n)) of {
704                O -> (trace "X" (OK (trace "X" (((,) (trace "X" (([]))) (trace "X" (l)))))));
705                S n' ->
706                 (trace "X" (case (trace "X" (l)) of {
707                              ([]) -> (trace "X" (Error (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('k')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('_')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))));
708                              (:) h t -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((split_list (trace "X" (t)) (trace "X" (n'))))))) (trace "X" ((\t' -> (trace "X" (case (trace "X" (t')) of {
709                                                                                                                                                                                        (,) t1 t2 -> (trace "X" (OK (trace "X" (((,) (trace "X" (((:) (trace "X" (h)) (trace "X" (t1))))) (trace "X" (t2)))))))})))))))))}))}))
710
711 type UniqM t =
712   UniqSupply.UniqSupply -> OrError ((,) UniqSupply.UniqSupply t)
713   -- singleton inductive, whose constructor was uniqM
714   
715 uniqMonad :: Monad (UniqM ())
716 uniqMonad =
717   (trace "X" (Build_Monad (trace "X" ((\_ x u -> (trace "X" (OK (trace "X" (((,) (trace "X" (u)) (trace "X" (x)))))))))) (trace "X" ((\_ _ x f u ->
718     (trace "X" (case (trace "X" ((trace "X" (x (trace "X" (u)))))) of {
719                  Error s -> (trace "X" (Error (trace "X" (s))));
720                  OK p -> (trace "X" (case (trace "X" (p)) of {
721                                       (,) u' va -> (trace "X" ((trace "X" (f (trace "X" (va)) (trace "X" (u'))))))}))})))))))
722
723 getU :: UniqM Unique.Unique
724 getU us =
725   (trace "X" (case (trace "X" ((trace "X" (UniqSupply.splitUniqSupply (trace "X" (us)))))) of {
726                (,) us1 us2 -> (trace "X" (OK (trace "X" (((,) (trace "X" (us1)) (trace "X" ((trace "X" ((UniqSupply.uniqFromSupply (trace "X" (us2))))))))))))}))
727
728 data FreshMonad t =
729    Build_FreshMonad (Monad ()) ((([]) t) -> ())
730
731 type FMT t x = ()
732
733 fMT_Monad :: (FreshMonad a1) -> Monad (FMT a1 ())
734 fMT_Monad f =
735   (trace "X" (case (trace "X" (f)) of {
736                Build_FreshMonad fMT_Monad0 fMT_fresh0 -> (trace "X" (fMT_Monad0))}))
737
738 fMT_fresh :: (FreshMonad a1) -> (([]) a1) -> FMT a1 (SigT a1 ())
739 fMT_fresh f =
740   (trace "X" (case (trace "X" (f)) of {
741                Build_FreshMonad fMT_Monad0 fMT_fresh0 -> (trace "X" (fMT_fresh0))}))
742
743 mapM :: (Monad a1) -> (([]) a1) -> a1
744 mapM mon ml =
745   (trace "X" (case (trace "X" (ml)) of {
746                ([]) -> (trace "X" ((trace "X" (returnM (trace "X" (mon)) (trace "X" (([])))))));
747                (:) a b -> (trace "X" ((trace "X" (bindM (trace "X" (mon)) (trace "X" (a)) (trace "X" ((\a' -> (trace "X" ((trace "X" (bindM (trace "X" (mon)) (trace "X" ((trace "X" ((mapM (trace "X" (mon)) (trace "X" (b))))))) (trace "X" ((\b' -> (trace "X" ((trace "X" (returnM (trace "X" (mon)) (trace "X" (((:) (trace "X" (a')) (trace "X" (b')))))))))))))))))))))))}))
748
749 treeM :: (Monad a2) -> (Tree (Prelude.Maybe a2)) -> a2
750 treeM mT t =
751   (trace "X" (case (trace "X" (t)) of {
752                T_Leaf o ->
753                 (trace "X" (case (trace "X" (o)) of {
754                              Prelude.Just x -> (trace "X" ((trace "X" (bindM (trace "X" (mT)) (trace "X" (x)) (trace "X" ((\x' -> (trace "X" ((trace "X" (returnM (trace "X" (mT)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (x')))))))))))))))))));
755                              Prelude.Nothing -> (trace "X" ((trace "X" (returnM (trace "X" (mT)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))))}));
756                T_Branch b1 b2 -> (trace "X" ((trace "X" (bindM (trace "X" (mT)) (trace "X" ((trace "X" ((treeM (trace "X" (mT)) (trace "X" (b1))))))) (trace "X" ((\b1' -> (trace "X" ((trace "X" (bindM (trace "X" (mT)) (trace "X" ((trace "X" ((treeM (trace "X" (mT)) (trace "X" (b2))))))) (trace "X" ((\b2' -> (trace "X" ((trace "X" (returnM (trace "X" (mT)) (trace "X" ((T_Branch (trace "X" (b1')) (trace "X" (b2')))))))))))))))))))))))}))
757
758 type Latex =
759   Prelude.String
760   -- singleton inductive, whose constructor was rawLatex
761   
762 type LatexMath =
763   Prelude.String
764   -- singleton inductive, whose constructor was rawLatexMath
765   
766 type ToLatex t =
767   t -> Latex
768   -- singleton inductive, whose constructor was Build_ToLatex
769   
770 toLatex :: (ToLatex a1) -> a1 -> Latex
771 toLatex toLatex0 =
772   (trace "X" (toLatex0))
773
774 latexToString :: ToString Latex
775 latexToString x =
776   (trace "X" (x))
777
778 type ToLatexMath t =
779   t -> LatexMath
780   -- singleton inductive, whose constructor was Build_ToLatexMath
781   
782 toLatexMath :: (ToLatexMath a1) -> a1 -> LatexMath
783 toLatexMath toLatexMath0 =
784   (trace "X" (toLatexMath0))
785
786 concatenableLatexMath :: Concatenable LatexMath
787 concatenableLatexMath l1 l2 =
788   (trace "X" ((trace "X" (concatenate (trace "X" (concatenableString)) (trace "X" (l1)) (trace "X" (l2))))))
789
790 latexMathToString :: ToString LatexMath
791 latexMathToString x =
792   (trace "X" (x))
793
794 toLatexMathLatex :: ToLatexMath Latex
795 toLatexMathLatex l =
796   (trace "X" ((trace "X" (concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" ([])))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (latexToString)) (trace "X" (l)))))))))))) (trace "X" (((:) (trace "X" ('}')) (trace "X" ([])))))))))
797
798 stringToLatex :: ToLatex Prelude.String
799 stringToLatex x =
800   (trace "X" ((trace "X" (sanitizeForLatex (trace "X" (x))))))
801
802 stringToLatexMath :: ToLatexMath Prelude.String
803 stringToLatexMath x =
804   (trace "X" ((trace "X" (toLatexMath (trace "X" (toLatexMathLatex)) (trace "X" ((trace "X" ((toLatex (trace "X" (stringToLatex)) (trace "X" (x)))))))))))
805
806 latexMathToLatexMath :: ToLatexMath LatexMath
807 latexMathToLatexMath x =
808   (trace "X" (x))
809
810 treeToLatexMath :: (ToLatexMath a1) -> (Tree (Prelude.Maybe a1)) -> LatexMath
811 treeToLatexMath toLatexV t =
812   (trace "X" (case (trace "X" (t)) of {
813                T_Leaf o ->
814                 (trace "X" (case (trace "X" (o)) of {
815                              Prelude.Just x -> (trace "X" ((trace "X" (concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([]))))))))))))))))))))))) (trace "X" ((trace "X" ((toLatexMath (trace "X" (toLatexV)) (trace "X" (x)))))))))))) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))));
816                              Prelude.Nothing -> (trace "X" ((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))}));
817                T_Branch b1 b2 -> (trace "X" ((trace "X" (concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([]))))))))))))))))))))))) (trace "X" ((trace "X" ((treeToLatexMath (trace "X" (toLatexV)) (trace "X" (b1)))))))))))) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" (',')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([])))))))))))))))) (trace "X" ((trace "X" ((treeToLatexMath (trace "X" (toLatexV)) (trace "X" (b2)))))))))))) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))}))
818
819 data ND judgment rule =
820    Nd_id0
821  | Nd_id1 judgment
822  | Nd_weak1 judgment
823  | Nd_copy (Tree (Prelude.Maybe judgment))
824  | Nd_exch (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment))
825  | Nd_prod (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (ND judgment rule) (ND judgment rule)
826  | Nd_comp (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (ND judgment rule) (ND judgment rule)
827  | Nd_cancell (Tree (Prelude.Maybe judgment))
828  | Nd_cancelr (Tree (Prelude.Maybe judgment))
829  | Nd_llecnac (Tree (Prelude.Maybe judgment))
830  | Nd_rlecnac (Tree (Prelude.Maybe judgment))
831  | Nd_assoc (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment))
832  | Nd_cossa (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment))
833  | Nd_rule (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) rule
834
835 nD_rect :: a3 -> (a1 -> a3) -> (a1 -> a3) -> ((Tree (Prelude.Maybe a1)) -> a3) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a3) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (ND a1 a2) -> a3 -> (ND a1 a2) -> a3 -> a3) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (ND a1 a2) -> a3 -> (ND a1 a2) -> a3 -> a3) -> ((Tree (Prelude.Maybe a1)) -> a3) -> ((Tree (Prelude.Maybe a1)) -> a3) -> ((Tree (Prelude.Maybe a1)) -> a3) -> ((Tree (Prelude.Maybe a1)) -> a3) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a3) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a3) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a2 -> a3) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (ND a1 a2) -> a3
836 nD_rect f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 hypotheses conclusions n =
837   (trace "X" (case (trace "X" (n)) of {
838                Nd_id0 -> (trace "X" (f));
839                Nd_id1 h -> (trace "X" ((trace "X" (f0 (trace "X" (h))))));
840                Nd_weak1 h -> (trace "X" ((trace "X" (f1 (trace "X" (h))))));
841                Nd_copy h -> (trace "X" ((trace "X" (f2 (trace "X" (h))))));
842                Nd_exch x y -> (trace "X" ((trace "X" (f3 (trace "X" (x)) (trace "X" (y))))));
843                Nd_prod h1 h2 c1 c2 pf1 pf2 -> (trace "X" ((trace "X" (f4 (trace "X" (h1)) (trace "X" (h2)) (trace "X" (c1)) (trace "X" (c2)) (trace "X" (pf1)) (trace "X" ((trace "X" ((nD_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (f5)) (trace "X" (f6)) (trace "X" (f7)) (trace "X" (f8)) (trace "X" (f9)) (trace "X" (f10)) (trace "X" (f11)) (trace "X" (f12)) (trace "X" (h1)) (trace "X" (c1)) (trace "X" (pf1))))))) (trace "X" (pf2)) (trace "X" ((trace "X" ((nD_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (f5)) (trace "X" (f6)) (trace "X" (f7)) (trace "X" (f8)) (trace "X" (f9)) (trace "X" (f10)) (trace "X" (f11)) (trace "X" (f12)) (trace "X" (h2)) (trace "X" (c2)) (trace "X" (pf2)))))))))));
844                Nd_comp h x c pf1 pf2 -> (trace "X" ((trace "X" (f5 (trace "X" (h)) (trace "X" (x)) (trace "X" (c)) (trace "X" (pf1)) (trace "X" ((trace "X" ((nD_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (f5)) (trace "X" (f6)) (trace "X" (f7)) (trace "X" (f8)) (trace "X" (f9)) (trace "X" (f10)) (trace "X" (f11)) (trace "X" (f12)) (trace "X" (h)) (trace "X" (x)) (trace "X" (pf1))))))) (trace "X" (pf2)) (trace "X" ((trace "X" ((nD_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (f5)) (trace "X" (f6)) (trace "X" (f7)) (trace "X" (f8)) (trace "X" (f9)) (trace "X" (f10)) (trace "X" (f11)) (trace "X" (f12)) (trace "X" (x)) (trace "X" (c)) (trace "X" (pf2)))))))))));
845                Nd_cancell a -> (trace "X" ((trace "X" (f6 (trace "X" (a))))));
846                Nd_cancelr a -> (trace "X" ((trace "X" (f7 (trace "X" (a))))));
847                Nd_llecnac a -> (trace "X" ((trace "X" (f8 (trace "X" (a))))));
848                Nd_rlecnac a -> (trace "X" ((trace "X" (f9 (trace "X" (a))))));
849                Nd_assoc a b c -> (trace "X" ((trace "X" (f10 (trace "X" (a)) (trace "X" (b)) (trace "X" (c))))));
850                Nd_cossa a b c -> (trace "X" ((trace "X" (f11 (trace "X" (a)) (trace "X" (b)) (trace "X" (c))))));
851                Nd_rule h c r -> (trace "X" ((trace "X" (f12 (trace "X" (h)) (trace "X" (c)) (trace "X" (r))))))}))
852
853 nd_id :: (Tree (Prelude.Maybe a1)) -> ND a1 a2
854 nd_id sl =
855   (trace "X" (case (trace "X" (sl)) of {
856                T_Leaf o ->
857                 (trace "X" (case (trace "X" (o)) of {
858                              Prelude.Just x -> (trace "X" (Nd_id1 (trace "X" (x))));
859                              Prelude.Nothing -> (trace "X" (Nd_id0))}));
860                T_Branch a b -> (trace "X" (Nd_prod (trace "X" (a)) (trace "X" (b)) (trace "X" (a)) (trace "X" (b)) (trace "X" ((trace "X" ((nd_id (trace "X" (a))))))) (trace "X" ((trace "X" ((nd_id (trace "X" (b)))))))))}))
861
862 nd_weak :: (Tree (Prelude.Maybe a1)) -> ND a1 a2
863 nd_weak sl =
864   (trace "X" (case (trace "X" (sl)) of {
865                T_Leaf o ->
866                 (trace "X" (case (trace "X" (o)) of {
867                              Prelude.Just x -> (trace "X" (Nd_weak1 (trace "X" (x))));
868                              Prelude.Nothing -> (trace "X" (Nd_id0))}));
869                T_Branch a b -> (trace "X" (Nd_comp (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((Nd_prod (trace "X" (a)) (trace "X" (b)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((nd_weak (trace "X" (a))))))) (trace "X" ((trace "X" ((nd_weak (trace "X" (b)))))))))) (trace "X" ((Nd_cancelr (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))))))))}))
870
871 data SIND judgment rule =
872    Scnd_weak (Tree (Prelude.Maybe judgment))
873  | Scnd_comp (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) judgment (SIND judgment rule) rule
874  | Scnd_branch (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (Tree (Prelude.Maybe judgment)) (SIND judgment rule) (SIND judgment rule)
875
876 mkSIND :: (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (ND a1 a2) -> (SIND a1 a2) -> SIND a1 a2
877 mkSIND h x c nd =
878   (trace "X" ((trace "X" (nD_rect (trace "X" ((\k -> (trace "X" (k))))) (trace "X" ((\h0 k -> (trace "X" (k))))) (trace "X" ((\h0 k -> (trace "X" (Scnd_weak (trace "X" (h))))))) (trace "X" ((\h0 k -> (trace "X" (Scnd_branch (trace "X" (h)) (trace "X" (h0)) (trace "X" (h0)) (trace "X" (k)) (trace "X" (k))))))) (trace "X" ((\x0 y k ->
879                             (trace "X" (case (trace "X" (k)) of {
880                                          Scnd_weak c0 -> (trace "X" (false_rect));
881                                          Scnd_comp ht ct c0 x1 x2 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" (false_rect))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x1)) (trace "X" (x2))))));
882                                          Scnd_branch ht c1 c2 x1 x2 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (x0)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (y)) (trace "X" ((\x3 x4 -> (trace "X" (Scnd_branch (trace "X" (h)) (trace "X" (y)) (trace "X" (x0)) (trace "X" (x4)) (trace "X" (x3))))))) (trace "X" (c2))))))))) (trace "X" (c1)) (trace "X" (__))))))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x1)) (trace "X" (x2))))))}))))) (trace "X" ((\h1 h2 c1 c2 nd1 iHnd1 nd2 iHnd2 k ->
883                             (trace "X" (case (trace "X" (k)) of {
884                                          Scnd_weak c0 -> (trace "X" (false_rect));
885                                          Scnd_comp ht ct c0 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" (false_rect))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))));
886                                          Scnd_branch ht c0 c3 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (h1)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (h2)) (trace "X" ((\x2 x3 -> (trace "X" (Scnd_branch (trace "X" (h)) (trace "X" (c1)) (trace "X" (c2)) (trace "X" ((trace "X" ((iHnd1 (trace "X" (x2))))))) (trace "X" ((trace "X" ((iHnd2 (trace "X" (x3)))))))))))) (trace "X" (c3))))))))) (trace "X" (c0)) (trace "X" (__))))))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))}))))) (trace "X" ((\h0 x0 c0 nd1 iHnd1 nd2 iHnd2 k -> (trace "X" ((trace "X" (iHnd2 (trace "X" ((trace "X" ((iHnd1 (trace "X" (k)))))))))))))) (trace "X" ((\a k ->
887                             (trace "X" (case (trace "X" (k)) of {
888                                          Scnd_weak c0 -> (trace "X" (false_rect));
889                                          Scnd_comp ht ct c0 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" (false_rect))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))));
890                                          Scnd_branch ht c1 c2 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\x2 x3 -> (trace "X" (x3))))) (trace "X" (c2))))))))) (trace "X" (c1)) (trace "X" (__))))))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))}))))) (trace "X" ((\a k ->
891                             (trace "X" (case (trace "X" (k)) of {
892                                          Scnd_weak c0 -> (trace "X" (false_rect));
893                                          Scnd_comp ht ct c0 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" (false_rect))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))));
894                                          Scnd_branch ht c1 c2 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((\x2 x3 -> (trace "X" (x2))))) (trace "X" (c2))))))))) (trace "X" (c1)) (trace "X" (__))))))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))}))))) (trace "X" ((\a k -> (trace "X" (Scnd_branch (trace "X" (h)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" (a)) (trace "X" ((Scnd_weak (trace "X" (h))))) (trace "X" (k))))))) (trace "X" ((\a k -> (trace "X" (Scnd_branch (trace "X" (h)) (trace "X" (a)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" (k)) (trace "X" ((Scnd_weak (trace "X" (h)))))))))) (trace "X" ((\a b c0 k ->
895                             (trace "X" (case (trace "X" (k)) of {
896                                          Scnd_weak c1 -> (trace "X" (false_rect));
897                                          Scnd_comp ht ct c1 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" (false_rect))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))));
898                                          Scnd_branch ht c1 c2 x0 x1 ->
899                                           (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ ->
900                                                                     (trace "X" ((trace "X" (eq_rect (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" ((\_ ->
901                                                                                               (trace "X" ((trace "X" (eq_rect (trace "X" (c0)) (trace "X" ((\x2 x3 ->
902                                                                                                                         (trace "X" (case (trace "X" (x2)) of {
903                                                                                                                                      Scnd_weak c3 -> (trace "X" (false_rect));
904                                                                                                                                      Scnd_comp ht0 ct c3 x4 x5 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" (false_rect))))) (trace "X" (ht0)) (trace "X" (__)) (trace "X" (x4)) (trace "X" (x5))))));
905                                                                                                                                      Scnd_branch ht0 c3 c4 x4 x5 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (b)) (trace "X" ((\x6 x7 -> (trace "X" (Scnd_branch (trace "X" (h)) (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c0))))) (trace "X" (x6)) (trace "X" ((Scnd_branch (trace "X" (h)) (trace "X" (b)) (trace "X" (c0)) (trace "X" (x7)) (trace "X" (x3)))))))))) (trace "X" (c4))))))))) (trace "X" (c3)) (trace "X" (__))))))))) (trace "X" (ht0)) (trace "X" (__)) (trace "X" (x4)) (trace "X" (x5))))))}))))) (trace "X" (c2))))))))) (trace "X" (c1)) (trace "X" (__))))))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))}))))) (trace "X" ((\a b c0 k ->
906                             (trace "X" (case (trace "X" (k)) of {
907                                          Scnd_weak c1 -> (trace "X" (false_rect));
908                                          Scnd_comp ht ct c1 x0 x1 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" (false_rect))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))));
909                                          Scnd_branch ht c1 c2 x0 x1 ->
910                                           (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ ->
911                                                                     (trace "X" ((trace "X" (eq_rect (trace "X" (a)) (trace "X" ((\_ ->
912                                                                                               (trace "X" ((trace "X" (eq_rect (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c0))))) (trace "X" ((\x2 x3 ->
913                                                                                                                         (trace "X" (case (trace "X" (x3)) of {
914                                                                                                                                      Scnd_weak c3 -> (trace "X" (false_rect));
915                                                                                                                                      Scnd_comp ht0 ct c3 x4 x5 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" (false_rect))))) (trace "X" (ht0)) (trace "X" (__)) (trace "X" (x4)) (trace "X" (x5))))));
916                                                                                                                                      Scnd_branch ht0 c3 c4 x4 x5 -> (trace "X" ((trace "X" (eq_rect (trace "X" (h)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (b)) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" (c0)) (trace "X" ((\x6 x7 -> (trace "X" (Scnd_branch (trace "X" (h)) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c0)) (trace "X" ((Scnd_branch (trace "X" (h)) (trace "X" (a)) (trace "X" (b)) (trace "X" (x2)) (trace "X" (x6))))) (trace "X" (x7))))))) (trace "X" (c4))))))))) (trace "X" (c3)) (trace "X" (__))))))))) (trace "X" (ht0)) (trace "X" (__)) (trace "X" (x4)) (trace "X" (x5))))))}))))) (trace "X" (c2))))))))) (trace "X" (c1)) (trace "X" (__))))))))) (trace "X" (ht)) (trace "X" (__)) (trace "X" (x0)) (trace "X" (x1))))))}))))) (trace "X" ((\h0 c0 r k ->
917                             (trace "X" (case (trace "X" (c0)) of {
918                                          T_Leaf o ->
919                                           (trace "X" (case (trace "X" (o)) of {
920                                                        Prelude.Just j -> (trace "X" (Scnd_comp (trace "X" (h)) (trace "X" (h0)) (trace "X" (j)) (trace "X" (k)) (trace "X" (r))));
921                                                        Prelude.Nothing -> (trace "X" (Scnd_weak (trace "X" (h))))}));
922                                          T_Branch c1 c2 -> (trace "X" (Prelude.error "absurd case"))}))))) (trace "X" (x)) (trace "X" (c)) (trace "X" (nd))))))
923
924 nd_map' :: (a1 -> a3) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a2 -> ND a3 a4) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (ND a1 a2) -> ND a3 a4
925 nd_map' f r h c pf =
926   (trace "X" (case (trace "X" (pf)) of {
927                Nd_id0 -> (trace "X" (Nd_id0));
928                Nd_id1 h0 -> (trace "X" (Nd_id1 (trace "X" ((trace "X" ((f (trace "X" (h0)))))))));
929                Nd_weak1 h0 -> (trace "X" ((trace "X" (nd_weak (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" ((trace "X" ((f (trace "X" (h0)))))))))))))))));
930                Nd_copy h0 -> (trace "X" (Nd_copy (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (h0)))))))));
931                Nd_exch x y -> (trace "X" (Nd_exch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (x))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (y)))))))));
932                Nd_prod h1 h2 c1 c2 lpf rpf -> (trace "X" (Nd_prod (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (h1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (h2))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c1))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c2))))))) (trace "X" ((trace "X" ((nd_map' (trace "X" (f)) (trace "X" (r)) (trace "X" (h1)) (trace "X" (c1)) (trace "X" (lpf))))))) (trace "X" ((trace "X" ((nd_map' (trace "X" (f)) (trace "X" (r)) (trace "X" (h2)) (trace "X" (c2)) (trace "X" (rpf)))))))));
933                Nd_comp h0 x c0 top bot -> (trace "X" (Nd_comp (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (h0))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (x))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c0))))))) (trace "X" ((trace "X" ((nd_map' (trace "X" (f)) (trace "X" (r)) (trace "X" (h0)) (trace "X" (x)) (trace "X" (top))))))) (trace "X" ((trace "X" ((nd_map' (trace "X" (f)) (trace "X" (r)) (trace "X" (x)) (trace "X" (c0)) (trace "X" (bot)))))))));
934                Nd_cancell a -> (trace "X" (Nd_cancell (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))));
935                Nd_cancelr a -> (trace "X" (Nd_cancelr (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))));
936                Nd_llecnac a -> (trace "X" (Nd_llecnac (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))));
937                Nd_rlecnac a -> (trace "X" (Nd_rlecnac (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))));
938                Nd_assoc a b c0 -> (trace "X" (Nd_assoc (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (b))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c0)))))))));
939                Nd_cossa a b c0 -> (trace "X" (Nd_cossa (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (b))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c0)))))))));
940                Nd_rule h0 c0 rule -> (trace "X" ((trace "X" (r (trace "X" (h0)) (trace "X" (c0)) (trace "X" (rule))))))}))
941
942 eolL :: LatexMath
943 eolL =
944   (trace "X" (eol))
945
946 sIND_toLatexMath :: (ToLatexMath a1) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> ToLatexMath a2) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a2 -> Prelude.Bool) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (SIND a1 a2) -> LatexMath
947 sIND_toLatexMath judgmentToLatexMath ruleToLatexMath hideRule h c pns =
948   (trace "X" (case (trace "X" (pns)) of {
949                Scnd_weak c0 -> (trace "X" ([]));
950                Scnd_comp ht ct c0 pns0 rule ->
951                 (trace "X" (case (trace "X" ((trace "X" (hideRule (trace "X" (ct)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (c0)))))))) (trace "X" (rule)))))) of {
952                              Prelude.True -> (trace "X" ((trace "X" (sIND_toLatexMath (trace "X" (judgmentToLatexMath)) (trace "X" (ruleToLatexMath)) (trace "X" (hideRule)) (trace "X" (ht)) (trace "X" (ct)) (trace "X" (pns0))))));
953                              Prelude.False -> (trace "X" ((trace "X" (concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('[')) (trace "X" ([])))))))))))))))))))))))))) (trace "X" ((trace "X" ((toLatexMath (trace "X" ((trace "X" ((ruleToLatexMath (trace "X" (ct)) (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (c0))))))))))))) (trace "X" (rule)))))))))))) (trace "X" (((:) (trace "X" (']')) (trace "X" (((:) (trace "X" ('{')) (trace "X" ([]))))))))))))) (trace "X" (eolL))))))) (trace "X" ((trace "X" ((sIND_toLatexMath (trace "X" (judgmentToLatexMath)) (trace "X" (ruleToLatexMath)) (trace "X" (hideRule)) (trace "X" (ht)) (trace "X" (ct)) (trace "X" (pns0)))))))))))) (trace "X" (((:) (trace "X" ('}')) (trace "X" (((:) (trace "X" ('{')) (trace "X" ([]))))))))))))) (trace "X" (eolL))))))) (trace "X" ((trace "X" ((toLatexMath (trace "X" (judgmentToLatexMath)) (trace "X" (c0)))))))))))) (trace "X" (((:) (trace "X" ('}')) (trace "X" ([])))))))))) (trace "X" (eolL))))))}));
954                Scnd_branch ht c1 c2 pns1 pns2 -> (trace "X" ((trace "X" (concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((sIND_toLatexMath (trace "X" (judgmentToLatexMath)) (trace "X" (ruleToLatexMath)) (trace "X" (hideRule)) (trace "X" (ht)) (trace "X" (c1)) (trace "X" (pns1))))))) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('1')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('}')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((sIND_toLatexMath (trace "X" (judgmentToLatexMath)) (trace "X" (ruleToLatexMath)) (trace "X" (hideRule)) (trace "X" (ht)) (trace "X" (c2)) (trace "X" (pns2)))))))))))}))
955
956 data Arrange t =
957    AId (Tree (Prelude.Maybe t))
958  | ACanL (Tree (Prelude.Maybe t))
959  | ACanR (Tree (Prelude.Maybe t))
960  | AuCanL (Tree (Prelude.Maybe t))
961  | AuCanR (Tree (Prelude.Maybe t))
962  | AAssoc (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t))
963  | AuAssoc (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t))
964  | AExch (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t))
965  | AWeak (Tree (Prelude.Maybe t))
966  | ACont (Tree (Prelude.Maybe t))
967  | ALeft (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t)) (Arrange t)
968  | ARight (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t)) (Arrange t)
969  | AComp (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t)) (Tree (Prelude.Maybe t)) (Arrange t) (Arrange t)
970
971 arrange_rect :: ((Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> a2) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Arrange a1) -> a2 -> a2) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Arrange a1) -> a2 -> a2) -> ((Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Arrange a1) -> a2 -> (Arrange a1) -> a2 -> a2) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Arrange a1) -> a2
972 arrange_rect f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 t t0 a =
973   (trace "X" (case (trace "X" (a)) of {
974                AId a0 -> (trace "X" ((trace "X" (f (trace "X" (a0))))));
975                ACanL a0 -> (trace "X" ((trace "X" (f0 (trace "X" (a0))))));
976                ACanR a0 -> (trace "X" ((trace "X" (f1 (trace "X" (a0))))));
977                AuCanL a0 -> (trace "X" ((trace "X" (f2 (trace "X" (a0))))));
978                AuCanR a0 -> (trace "X" ((trace "X" (f3 (trace "X" (a0))))));
979                AAssoc a0 b c -> (trace "X" ((trace "X" (f4 (trace "X" (a0)) (trace "X" (b)) (trace "X" (c))))));
980                AuAssoc a0 b c -> (trace "X" ((trace "X" (f5 (trace "X" (a0)) (trace "X" (b)) (trace "X" (c))))));
981                AExch a0 b -> (trace "X" ((trace "X" (f6 (trace "X" (a0)) (trace "X" (b))))));
982                AWeak a0 -> (trace "X" ((trace "X" (f7 (trace "X" (a0))))));
983                ACont a0 -> (trace "X" ((trace "X" (f8 (trace "X" (a0))))));
984                ALeft h c x a0 -> (trace "X" ((trace "X" (f9 (trace "X" (h)) (trace "X" (c)) (trace "X" (x)) (trace "X" (a0)) (trace "X" ((trace "X" ((arrange_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (f5)) (trace "X" (f6)) (trace "X" (f7)) (trace "X" (f8)) (trace "X" (f9)) (trace "X" (f10)) (trace "X" (f11)) (trace "X" (h)) (trace "X" (c)) (trace "X" (a0)))))))))));
985                ARight h c x a0 -> (trace "X" ((trace "X" (f10 (trace "X" (h)) (trace "X" (c)) (trace "X" (x)) (trace "X" (a0)) (trace "X" ((trace "X" ((arrange_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (f5)) (trace "X" (f6)) (trace "X" (f7)) (trace "X" (f8)) (trace "X" (f9)) (trace "X" (f10)) (trace "X" (f11)) (trace "X" (h)) (trace "X" (c)) (trace "X" (a0)))))))))));
986                AComp a0 b c a1 a2 -> (trace "X" ((trace "X" (f11 (trace "X" (a0)) (trace "X" (b)) (trace "X" (c)) (trace "X" (a1)) (trace "X" ((trace "X" ((arrange_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (f5)) (trace "X" (f6)) (trace "X" (f7)) (trace "X" (f8)) (trace "X" (f9)) (trace "X" (f10)) (trace "X" (f11)) (trace "X" (a0)) (trace "X" (b)) (trace "X" (a1))))))) (trace "X" (a2)) (trace "X" ((trace "X" ((arrange_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (f5)) (trace "X" (f6)) (trace "X" (f7)) (trace "X" (f8)) (trace "X" (f9)) (trace "X" (f10)) (trace "X" (f11)) (trace "X" (b)) (trace "X" (c)) (trace "X" (a2)))))))))))}))
987
988 arrangeMap :: (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (a1 -> a2) -> (Arrange a1) -> Arrange a2
989 arrangeMap __U03a3___U2081_ __U03a3___U2082_ f x =
990   (trace "X" ((trace "X" (arrange_rect (trace "X" ((\a -> (trace "X" (AId (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))))))) (trace "X" ((\a -> (trace "X" (ACanL (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))))))) (trace "X" ((\a -> (trace "X" (ACanR (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))))))) (trace "X" ((\a -> (trace "X" (AuCanL (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))))))) (trace "X" ((\a -> (trace "X" (AuCanR (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))))))) (trace "X" ((\a b c -> (trace "X" (AAssoc (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (b))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c)))))))))))) (trace "X" ((\a b c -> (trace "X" (AuAssoc (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (b))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c)))))))))))) (trace "X" ((\a b -> (trace "X" (AExch (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (b)))))))))))) (trace "X" ((\a -> (trace "X" (AWeak (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))))))) (trace "X" ((\a -> (trace "X" (ACont (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a)))))))))))) (trace "X" ((\h c x0 x1 iHX -> (trace "X" (ALeft (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (h))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (x0))))))) (trace "X" (iHX))))))) (trace "X" ((\h c x0 x1 iHX -> (trace "X" (ARight (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (h))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (x0))))))) (trace "X" (iHX))))))) (trace "X" ((\a b c x1 iHX1 x2 iHX2 -> (trace "X" (AComp (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (a))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (b))))))) (trace "X" ((trace "X" ((mapOptionTree (trace "X" (f)) (trace "X" (c))))))) (trace "X" (iHX1)) (trace "X" (iHX2))))))) (trace "X" (__U03a3___U2081_)) (trace "X" (__U03a3___U2082_)) (trace "X" (x))))))
991
992 arrangeSwapMiddle :: (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> Arrange a1
993 arrangeSwapMiddle a b c d =
994   (trace "X" (AComp (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (d)))))))) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (d))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (d)))))))) (trace "X" ((AuAssoc (trace "X" (a)) (trace "X" (b)) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (d)))))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (d))))))))))) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b))))) (trace "X" (d)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (d)))))))) (trace "X" ((ALeft (trace "X" ((T_Branch (trace "X" (b)) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (d)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b))))) (trace "X" (d))))) (trace "X" (a)) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" (b)) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (d)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c))))) (trace "X" (d))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b))))) (trace "X" (d))))) (trace "X" ((AAssoc (trace "X" (b)) (trace "X" (c)) (trace "X" (d))))) (trace "X" ((ARight (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b))))) (trace "X" (d)) (trace "X" ((AExch (trace "X" (c)) (trace "X" (b)))))))))))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b))))) (trace "X" (d)))))))) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (d))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (d)))))))) (trace "X" ((ALeft (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b))))) (trace "X" (d))))) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (d)))))))) (trace "X" (a)) (trace "X" ((AuAssoc (trace "X" (c)) (trace "X" (b)) (trace "X" (d)))))))) (trace "X" ((AAssoc (trace "X" (a)) (trace "X" (c)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (d))))))))))))))))
995
996 pivotContext :: (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> Arrange a1
997 pivotContext a b c =
998   (trace "X" (AComp (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" (b))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c)))))))) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b)))))))) (trace "X" ((AuAssoc (trace "X" (a)) (trace "X" (b)) (trace "X" (c))))) (trace "X" ((ALeft (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b))))) (trace "X" (a)) (trace "X" ((AExch (trace "X" (c)) (trace "X" (b))))))))))) (trace "X" ((AAssoc (trace "X" (a)) (trace "X" (c)) (trace "X" (b)))))))
999
1000 pivotContext' :: (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> Arrange a1
1001 pivotContext' a b c =
1002   (trace "X" (AComp (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (a))))) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c)))))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" (a)) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (c)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (a))))) (trace "X" (c))))) (trace "X" ((AAssoc (trace "X" (a)) (trace "X" (b)) (trace "X" (c))))) (trace "X" ((ARight (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (a))))) (trace "X" (c)) (trace "X" ((AExch (trace "X" (b)) (trace "X" (a))))))))))) (trace "X" ((AuAssoc (trace "X" (b)) (trace "X" (a)) (trace "X" (c)))))))
1003
1004 copyAndPivotContext :: (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> Arrange a1
1005 copyAndPivotContext a b c =
1006   (trace "X" (AComp (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (b)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" (b))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" (b))))) (trace "X" (b))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (b)))))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" ((T_Branch (trace "X" (c)) (trace "X" (b)))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c))))) (trace "X" (b))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" (b))))) (trace "X" (b))))) (trace "X" ((AAssoc (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c)) (trace "X" (b))))) (trace "X" ((ARight (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (b))))) (trace "X" (c))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" (b))))) (trace "X" (b)) (trace "X" ((trace "X" ((pivotContext (trace "X" (a)) (trace "X" (b)) (trace "X" (c))))))))))))) (trace "X" ((AuAssoc (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" (b)) (trace "X" (b)))))))) (trace "X" ((ALeft (trace "X" ((T_Branch (trace "X" (b)) (trace "X" (b))))) (trace "X" (b)) (trace "X" ((T_Branch (trace "X" (a)) (trace "X" (c))))) (trace "X" ((ACont (trace "X" (b))))))))))
1007
1008 arrangePartition :: (Tree (Prelude.Maybe a1)) -> (a1 -> Prelude.Bool) -> Arrange a1
1009 arrangePartition __U03a3_ f =
1010   (trace "X" ((trace "X" (tree_rect (trace "X" ((\a ->
1011                             (trace "X" (case (trace "X" (a)) of {
1012                                          Prelude.Just t ->
1013                                           (trace "X" (let {b = (trace "X" ((trace "X" (f (trace "X" (t))))))} in
1014                                                       (trace "X" (case (trace "X" (b)) of {
1015                                                                    Prelude.True -> (trace "X" (AuCanL (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (t))))))))));
1016                                                                    Prelude.False -> (trace "X" (AuCanR (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (t))))))))))}))));
1017                                          Prelude.Nothing -> (trace "X" (AuCanL (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))}))))) (trace "X" ((\__U03a3_1 iH__U03a3_1 __U03a3_2 iH__U03a3_2 -> (trace "X" (AComp (trace "X" ((T_Branch (trace "X" (__U03a3_1)) (trace "X" (__U03a3_2))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1))))))))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2)))))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2))))))))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2)))))))))))))))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" (__U03a3_1)) (trace "X" (__U03a3_2))))) (trace "X" ((T_Branch (trace "X" (__U03a3_1)) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2)))))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1))))))))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2)))))))))))))))))) (trace "X" ((ALeft (trace "X" (__U03a3_2)) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2))))))))))))))) (trace "X" (__U03a3_1)) (trace "X" (iH__U03a3_2))))) (trace "X" ((ARight (trace "X" (__U03a3_1)) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1))))))))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2))))))))))))))) (trace "X" (iH__U03a3_1)))))))) (trace "X" ((trace "X" ((arrangeSwapMiddle (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2)))))))))))))))))))))) (trace "X" (__U03a3_))))))
1018
1019 arrangeUnPartition :: (Tree (Prelude.Maybe a1)) -> (a1 -> Prelude.Bool) -> Arrange a1
1020 arrangeUnPartition __U03a3_ f =
1021   (trace "X" ((trace "X" (tree_rect (trace "X" ((\a ->
1022                             (trace "X" (case (trace "X" (a)) of {
1023                                          Prelude.Just t ->
1024                                           (trace "X" (let {b = (trace "X" ((trace "X" (f (trace "X" (t))))))} in
1025                                                       (trace "X" (case (trace "X" (b)) of {
1026                                                                    Prelude.True -> (trace "X" (ACanL (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (t))))))))));
1027                                                                    Prelude.False -> (trace "X" (ACanR (trace "X" ((T_Leaf (trace "X" ((Prelude.Just (trace "X" (t))))))))))}))));
1028                                          Prelude.Nothing -> (trace "X" (ACanL (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))}))))) (trace "X" ((\__U03a3_1 iH__U03a3_1 __U03a3_2 iH__U03a3_2 -> (trace "X" (AComp (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2))))))))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2)))))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1))))))))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2)))))))))))))))))) (trace "X" ((T_Branch (trace "X" (__U03a3_1)) (trace "X" (__U03a3_2))))) (trace "X" ((trace "X" ((arrangeSwapMiddle (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2))))))))))))))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1))))))))))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2)))))))))))))))))) (trace "X" ((T_Branch (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1))))))))))))))) (trace "X" (__U03a3_2))))) (trace "X" ((T_Branch (trace "X" (__U03a3_1)) (trace "X" (__U03a3_2))))) (trace "X" ((ALeft (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_2)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_2)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_2))))))))))))))) (trace "X" (__U03a3_2)) (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1))))))))))))))) (trace "X" (iH__U03a3_2))))) (trace "X" ((ARight (trace "X" ((T_Branch (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" (f))))))) (trace "X" (__U03a3_1)))))))))))) (trace "X" ((trace "X" ((dropT (trace "X" (__U03a3_1)) (trace "X" ((trace "X" ((mkFlags (trace "X" ((trace "X" ((liftBoolFunc (trace "X" (Prelude.False)) (trace "X" ((\x -> (trace "X" ((trace "X" (bnot (trace "X" ((trace "X" ((f (trace "X" (x))))))))))))))))))) (trace "X" (__U03a3_1))))))))))))))) (trace "X" (__U03a3_1)) (trace "X" (__U03a3_2)) (trace "X" (iH__U03a3_1))))))))))))) (trace "X" (__U03a3_))))))
1029
1030 decide_tree_empty :: (Tree (Prelude.Maybe a1)) -> Prelude.Either (SigT (Tree ()) ()) ()
1031 decide_tree_empty t =
1032   (trace "X" (case (trace "X" (t)) of {
1033                T_Leaf x ->
1034                 (trace "X" (case (trace "X" (x)) of {
1035                              Prelude.Just t0 -> (trace "X" (Prelude.Right (trace "X" (()))));
1036                              Prelude.Nothing -> (trace "X" (Prelude.Left (trace "X" ((ExistT (trace "X" ((T_Leaf (trace "X" (()))))) (trace "X" (__)))))))}));
1037                T_Branch b1 b2 ->
1038                 (trace "X" (let {b1' = (trace "X" ((trace "X" (decide_tree_empty (trace "X" (b1))))))} in
1039                             (trace "X" (let {b2' = (trace "X" ((trace "X" (decide_tree_empty (trace "X" (b2))))))} in
1040                                         (trace "X" (case (trace "X" (b1')) of {
1041                                                      Prelude.Left s ->
1042                                                       (trace "X" (case (trace "X" (b2')) of {
1043                                                                    Prelude.Left s0 ->
1044                                                                     (trace "X" (case (trace "X" (s)) of {
1045                                                                                  ExistT x _ -> (trace "X" (case (trace "X" (s0)) of {
1046                                                                                                             ExistT x0 _ -> (trace "X" ((trace "X" (eq_rec_r (trace "X" ((trace "X" ((mapTree (trace "X" ((\x1 -> (trace "X" (Prelude.Nothing))))) (trace "X" (x0))))))) (trace "X" ((trace "X" ((eq_rec_r (trace "X" ((trace "X" ((mapTree (trace "X" ((\x1 -> (trace "X" (Prelude.Nothing))))) (trace "X" (x))))))) (trace "X" ((Prelude.Left (trace "X" ((ExistT (trace "X" ((T_Branch (trace "X" (x)) (trace "X" (x0))))) (trace "X" (__)))))))) (trace "X" (b1))))))) (trace "X" (b2))))))}))}));
1047                                                                    Prelude.Right u -> (trace "X" (Prelude.Right (trace "X" (u))))}));
1048                                                      Prelude.Right u -> (trace "X" (Prelude.Right (trace "X" (u))))}))))))}))
1049
1050 arrangeCancelEmptyTree :: (Tree a2) -> (Tree (Prelude.Maybe a1)) -> Arrange a1
1051 arrangeCancelEmptyTree q t =
1052   (trace "X" ((trace "X" (tree_rect (trace "X" ((\a t0 _ -> (trace "X" ((trace "X" (eq_rect_r (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((AId (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))) (trace "X" (t0))))))))) (trace "X" ((\q1 iHq1 q2 iHq2 t0 _ ->
1053                             (trace "X" (case (trace "X" (t0)) of {
1054                                          T_Leaf o -> (trace "X" (false_rect));
1055                                          T_Branch t1 t2 -> (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2))))))) (trace "X" ((let {x1 = (trace "X" ((trace "X" (iHq1 (trace "X" (t1)) (trace "X" (__))))))} in (trace "X" (let {x2 = (trace "X" ((trace "X" (iHq2 (trace "X" (t2)) (trace "X" (__))))))} in (trace "X" (AComp (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((ARight (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2))))))) (trace "X" ((trace "X" ((eq_rect (trace "X" (t1)) (trace "X" (x1)) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))))))))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2))))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((ACanL (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))) (trace "X" ((trace "X" ((eq_rect (trace "X" (t2)) (trace "X" (x2)) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))))))))))))))) (trace "X" (t2))))))))) (trace "X" (t1)) (trace "X" (__))))))}))))) (trace "X" (q)) (trace "X" (t)) (trace "X" (__))))))
1056
1057 arrangeUnCancelEmptyTree :: (Tree a2) -> (Tree (Prelude.Maybe a1)) -> Arrange a1
1058 arrangeUnCancelEmptyTree q t =
1059   (trace "X" ((trace "X" (tree_rect (trace "X" ((\a t0 _ -> (trace "X" ((trace "X" (eq_rect_r (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((AId (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))) (trace "X" (t0))))))))) (trace "X" ((\q1 iHq1 q2 iHq2 t0 _ ->
1060                             (trace "X" (case (trace "X" (t0)) of {
1061                                          T_Leaf o -> (trace "X" (false_rect));
1062                                          T_Branch t1 t2 -> (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((\_ -> (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2))))))) (trace "X" ((let {x1 = (trace "X" ((trace "X" (iHq1 (trace "X" (t1)) (trace "X" (__))))))} in (trace "X" (let {x2 = (trace "X" ((trace "X" (iHq2 (trace "X" (t2)) (trace "X" (__))))))} in (trace "X" (AComp (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))) (trace "X" ((AuCanL (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))) (trace "X" ((T_Branch (trace "X" (t1)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))) (trace "X" ((ARight (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" (t1)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" (x1))))) (trace "X" ((AComp (trace "X" ((T_Branch (trace "X" (t1)) (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing)))))))) (trace "X" ((T_Branch (trace "X" (t1)) (trace "X" (t2))))) (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))) (trace "X" ((ALeft (trace "X" ((T_Leaf (trace "X" (Prelude.Nothing))))) (trace "X" (t2)) (trace "X" (t1)) (trace "X" (x2))))) (trace "X" ((trace "X" ((eq_rect_r (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2)))))))))) (trace "X" ((AId (trace "X" ((T_Branch (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q1))))))) (trace "X" ((trace "X" ((mapTree (trace "X" ((\x -> (trace "X" (Prelude.Nothing))))) (trace "X" (q2))))))))))))) (trace "X" ((T_Branch (trace "X" (t1)) (trace "X" (t2))))))))))))))))))))))) (trace "X" (t2))))))))) (trace "X" (t1)) (trace "X" (__))))))}))))) (trace "X" (q)) (trace "X" (t)) (trace "X" (__))))))
1063
1064 natToStringInstance :: ToString Nat
1065 natToStringInstance =
1066   (trace "X" (natToString))
1067
1068 data Kind =
1069    KindStar
1070  | KindArrow Kind Kind
1071  | KindUnliftedType
1072  | KindUnboxedTuple
1073  | KindArgType
1074  | KindOpenType
1075
1076 kind_rect :: a1 -> (Kind -> a1 -> Kind -> a1 -> a1) -> a1 -> a1 -> a1 -> a1 -> Kind -> a1
1077 kind_rect f f0 f1 f2 f3 f4 k =
1078   (trace "X" (case (trace "X" (k)) of {
1079                KindStar -> (trace "X" (f));
1080                KindArrow k0 k1 -> (trace "X" ((trace "X" (f0 (trace "X" (k0)) (trace "X" ((trace "X" ((kind_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (k0))))))) (trace "X" (k1)) (trace "X" ((trace "X" ((kind_rect (trace "X" (f)) (trace "X" (f0)) (trace "X" (f1)) (trace "X" (f2)) (trace "X" (f3)) (trace "X" (f4)) (trace "X" (k1)))))))))));
1081                KindUnliftedType -> (trace "X" (f1));
1082                KindUnboxedTuple -> (trace "X" (f2));
1083                KindArgType -> (trace "X" (f3));
1084                KindOpenType -> (trace "X" (f4))}))
1085
1086 kind_rec :: a1 -> (Kind -> a1 -> Kind -> a1 -> a1) -> a1 -> a1 -> a1 -> a1 -> Kind -> a1
1087 kind_rec =
1088   (trace "X" (kind_rect))
1089
1090 kindToString :: Kind -> Prelude.String
1091 kindToString k =
1092   (trace "X" (case (trace "X" (k)) of {
1093                KindStar -> (trace "X" ((:) (trace "X" ('*')) (trace "X" ([]))));
1094                KindArrow k1 k2 ->
1095                 (trace "X" (case (trace "X" (k1)) of {
1096                              KindStar -> (trace "X" ((trace "X" (concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('*')) (trace "X" (((:) (trace "X" ('=')) (trace "X" (((:) (trace "X" ('>')) (trace "X" ([]))))))))))) (trace "X" ((trace "X" ((kindToString (trace "X" (k2)))))))))));
1097                              _ -> (trace "X" ((trace "X" (concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('(')) (trace "X" ([]))))) (trace "X" ((trace "X" ((kindToString (trace "X" (k1)))))))))))) (trace "X" (((:) (trace "X" (')')) (trace "X" (((:) (trace "X" ('=')) (trace "X" (((:) (trace "X" ('>')) (trace "X" ([])))))))))))))))) (trace "X" ((trace "X" ((kindToString (trace "X" (k2)))))))))))}));
1098                KindUnliftedType -> (trace "X" ((:) (trace "X" ('#')) (trace "X" ([]))));
1099                KindUnboxedTuple -> (trace "X" ((:) (trace "X" ('(')) (trace "X" (((:) (trace "X" ('#')) (trace "X" (((:) (trace "X" (')')) (trace "X" ([]))))))))));
1100                KindArgType -> (trace "X" ((:) (trace "X" ('?')) (trace "X" (((:) (trace "X" ('?')) (trace "X" ([])))))));
1101                KindOpenType -> (trace "X" ((:) (trace "X" ('?')) (trace "X" ([]))))}))
1102
1103 kindToString0 :: ToString Kind
1104 kindToString0 =
1105   (trace "X" (kindToString))
1106
1107 eCKind :: Kind
1108 eCKind =
1109   (trace "X" (KindArrow (trace "X" (KindStar)) (trace "X" ((KindArrow (trace "X" (KindStar)) (trace "X" (KindStar)))))))
1110
1111 kindToLatexMath :: Kind -> LatexMath
1112 kindToLatexMath k =
1113   (trace "X" (case (trace "X" (k)) of {
1114                KindStar -> (trace "X" ((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" ([]))))))))))))))));
1115                KindArrow k1 k2 ->
1116                 (trace "X" (case (trace "X" (k1)) of {
1117                              KindStar -> (trace "X" ((trace "X" (concatenate (trace "X" (concatenableLatexMath)) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('R')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((kindToLatexMath (trace "X" (k2)))))))))));
1118                              _ -> (trace "X" ((trace "X" (concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableLatexMath)) (trace "X" (((:) (trace "X" ('(')) (trace "X" ([]))))) (trace "X" ((trace "X" ((kindToLatexMath (trace "X" (k1)))))))))))) (trace "X" (((:) (trace "X" (')')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('R')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((kindToLatexMath (trace "X" (k2)))))))))))}));
1119                KindUnliftedType -> (trace "X" ((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('#')) (trace "X" (((:) (trace "X" ('}')) (trace "X" (((:) (trace "X" ('}')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))));
1120                KindUnboxedTuple -> (trace "X" ((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('(')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('#')) (trace "X" (((:) (trace "X" (')')) (trace "X" (((:) (trace "X" ('}')) (trace "X" (((:) (trace "X" ('}')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))));
1121                KindArgType -> (trace "X" ((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('?')) (trace "X" (((:) (trace "X" ('?')) (trace "X" (((:) (trace "X" ('}')) (trace "X" (((:) (trace "X" ('}')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))));
1122                KindOpenType -> (trace "X" ((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('\\')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('{')) (trace "X" (((:) (trace "X" ('?')) (trace "X" (((:) (trace "X" ('}')) (trace "X" (((:) (trace "X" ('}')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))}))
1123
1124 kindEqDecidable :: EqDecidable Kind
1125 kindEqDecidable v1 =
1126   (trace "X" ((trace "X" (kind_rec (trace "X" ((\v2 ->
1127                             (trace "X" (case (trace "X" (v2)) of {
1128                                          KindStar -> (trace "X" (Prelude.True));
1129                                          _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v1_1 iHv1_1 v1_2 iHv1_2 v2 ->
1130                             (trace "X" (case (trace "X" (v2)) of {
1131                                          KindArrow v2_1 v2_2 ->
1132                                           (trace "X" (let {s = (trace "X" ((trace "X" (iHv1_1 (trace "X" (v2_1))))))} in
1133                                                       (trace "X" (case (trace "X" (s)) of {
1134                                                                    Prelude.True ->
1135                                                                     (trace "X" (let {s0 = (trace "X" ((trace "X" (iHv1_2 (trace "X" (v2_2))))))} in
1136                                                                                 (trace "X" (case (trace "X" (s0)) of {
1137                                                                                              Prelude.True -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (v2_2)) (trace "X" ((\iHv1_3 -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (v2_1)) (trace "X" ((\iHv1_4 -> (trace "X" (Prelude.True))))) (trace "X" (v1_1)) (trace "X" (iHv1_1))))))))) (trace "X" (v1_2)) (trace "X" (iHv1_2))))));
1138                                                                                              Prelude.False -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (v2_1)) (trace "X" ((\iHv1_3 -> (trace "X" (Prelude.False))))) (trace "X" (v1_1)) (trace "X" (iHv1_1))))))}))));
1139                                                                    Prelude.False ->
1140                                                                     (trace "X" (let {s0 = (trace "X" ((trace "X" (iHv1_2 (trace "X" (v2_2))))))} in
1141                                                                                 (trace "X" (case (trace "X" (s0)) of {
1142                                                                                              Prelude.True -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (v2_2)) (trace "X" ((\iHv1_3 -> (trace "X" (Prelude.False))))) (trace "X" (v1_2)) (trace "X" (iHv1_2))))));
1143                                                                                              Prelude.False -> (trace "X" (Prelude.False))}))))}))));
1144                                          _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v2 ->
1145                             (trace "X" (case (trace "X" (v2)) of {
1146                                          KindUnliftedType -> (trace "X" (Prelude.True));
1147                                          _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v2 ->
1148                             (trace "X" (case (trace "X" (v2)) of {
1149                                          KindUnboxedTuple -> (trace "X" (Prelude.True));
1150                                          _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v2 ->
1151                             (trace "X" (case (trace "X" (v2)) of {
1152                                          KindArgType -> (trace "X" (Prelude.True));
1153                                          _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v2 ->
1154                             (trace "X" (case (trace "X" (v2)) of {
1155                                          KindOpenType -> (trace "X" (Prelude.True));
1156                                          _ -> (trace "X" (Prelude.False))}))))) (trace "X" (v1))))))
1157
1158 tyConToString :: ToString TyCon.TyCon
1159 tyConToString =
1160   (trace "X" (outputableToString))
1161
1162 tyFunToString :: ToString TyCon.TyCon
1163 tyFunToString =
1164   (trace "X" (outputableToString))
1165
1166 arrowTyCon :: TyCon.TyCon
1167 arrowTyCon = Type.funTyCon
1168
1169 haskLiteralToString :: ToString Literal.Literal
1170 haskLiteralToString =
1171   (trace "X" (outputableToString))
1172
1173 haskLiteralToTyCon :: Literal.Literal -> TyCon.TyCon
1174 haskLiteralToTyCon lit =
1175   (trace "X" (case (trace "X" (lit)) of {
1176                Literal.MachChar h -> (trace "X" (TysPrim.charPrimTyCon));
1177                Literal.MachInt h -> (trace "X" (TysPrim.intPrimTyCon));
1178                Literal.MachInt64 h -> (trace "X" (TysPrim.int64PrimTyCon));
1179                Literal.MachWord h -> (trace "X" (TysPrim.wordPrimTyCon));
1180                Literal.MachWord64 h -> (trace "X" (TysPrim.word64PrimTyCon));
1181                Literal.MachFloat h -> (trace "X" (TysPrim.floatPrimTyCon));
1182                Literal.MachDouble h -> (trace "X" (TysPrim.doublePrimTyCon));
1183                _ -> (trace "X" (TysPrim.addrPrimTyCon))}))
1184
1185 coreVarEqDecidable :: EqDecidable Var.Var
1186 coreVarEqDecidable =
1187   (trace "X" ((==)))
1188
1189 coreVarToString :: ToString Var.Var
1190 coreVarToString =
1191   (trace "X" (outputableToString))
1192
1193 tyConEqDecidable :: EqDecidable TyCon.TyCon
1194 tyConEqDecidable =
1195   (trace "X" ((==)))
1196
1197 tyFunEqDecidable :: EqDecidable TyCon.TyCon
1198 tyFunEqDecidable =
1199   (trace "X" ((==)))
1200
1201 coreTypeToString :: ToString TypeRep.Type
1202 coreTypeToString =
1203   (trace "X" ((outputableToString . coreViewDeep)))
1204
1205 coreDataConToString :: ToString DataCon.DataCon
1206 coreDataConToString =
1207   (trace "X" (outputableToString))
1208
1209 coreExprToString :: ToString (CoreSyn.Expr Var.Var)
1210 coreExprToString =
1211   (trace "X" (outputableToString))
1212
1213 data WeakTypeVar0 =
1214    WeakTypeVar Var.Var Kind
1215
1216 data WeakType =
1217    WTyVarTy WeakTypeVar0
1218  | WAppTy WeakType WeakType
1219  | WTyFunApp TyCon.TyCon (([]) WeakType)
1220  | WTyCon TyCon.TyCon
1221  | WFunTyCon
1222  | WCodeTy WeakTypeVar0 WeakType
1223  | WCoFunTy WeakType WeakType WeakType
1224  | WForAllTy WeakTypeVar0 WeakType
1225  | WClassP Class.Class (([]) WeakType)
1226  | WIParam (BasicTypes.IPName Name.Name) WeakType
1227
1228 weakTypeVarEqDecidable :: EqDecidable WeakTypeVar0
1229 weakTypeVarEqDecidable v1 v2 =
1230   (trace "X" (case (trace "X" (v1)) of {
1231                WeakTypeVar cv1 k1 ->
1232                 (trace "X" (case (trace "X" (v2)) of {
1233                              WeakTypeVar cv2 k2 ->
1234                               (trace "X" (let {s = (trace "X" ((trace "X" (eqd_dec (trace "X" (coreVarEqDecidable)) (trace "X" (cv1)) (trace "X" (cv2))))))} in
1235                                           (trace "X" (case (trace "X" (s)) of {
1236                                                        Prelude.True ->
1237                                                         (trace "X" ((trace "X" (eq_rec_r (trace "X" (cv2))
1238                                                                                   (trace "X" ((let {s0 = (trace "X" ((trace "X" (eqd_dec (trace "X" (kindEqDecidable)) (trace "X" (k1)) (trace "X" (k2))))))} in
1239                                                                                                (trace "X" (case (trace "X" (s0)) of {
1240                                                                                                             Prelude.True -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (k2)) (trace "X" (Prelude.True)) (trace "X" (k1))))));
1241                                                                                                             Prelude.False -> (trace "X" (Prelude.False))}))))) (trace "X" (cv1))))));
1242                                                        Prelude.False -> (trace "X" (Prelude.False))}))))}))}))
1243
1244 data WeakCoerVar0 =
1245    WeakCoerVar Var.Var WeakType WeakType
1246
1247 data WeakCoercion =
1248    WCoVar WeakCoerVar0
1249  | WCoType WeakType
1250  | WCoApp WeakCoercion WeakCoercion
1251  | WCoAppT WeakCoercion WeakType
1252  | WCoAll Kind (WeakTypeVar0 -> WeakCoercion)
1253  | WCoSym WeakCoercion
1254  | WCoComp WeakCoercion WeakCoercion
1255  | WCoLeft WeakCoercion
1256  | WCoRight WeakCoercion
1257  | WCoUnsafe WeakType WeakType
1258
1259 weakCoercionTypes :: WeakCoercion -> (,) WeakType WeakType
1260 weakCoercionTypes wc =
1261   (trace "X" (case (trace "X" (wc)) of {
1262                WCoSym c -> (trace "X" (case (trace "X" ((trace "X" (weakCoercionTypes (trace "X" (c)))))) of {
1263                                         (,) t2 t1 -> (trace "X" ((,) (trace "X" (t1)) (trace "X" (t2))))}));
1264                WCoUnsafe t1 t2 -> (trace "X" ((,) (trace "X" (t1)) (trace "X" (t2))));
1265                _ -> (trace "X" ((,) (trace "X" (WFunTyCon)) (trace "X" (WFunTyCon))))}))
1266
1267 weakTypeToString :: ToString WeakType
1268 weakTypeToString =
1269   (trace "X" ((coreTypeToString . weakTypeToCoreType)))
1270
1271 data CoreVarToWeakVarResult =
1272    CVTWVR_EVar TypeRep.Type
1273  | CVTWVR_TyVar Kind
1274  | CVTWVR_CoVar TypeRep.Type TypeRep.Type
1275
1276 data WeakExprVar0 =
1277    WeakExprVar Var.Var WeakType
1278
1279 data WeakVar =
1280    WExprVar WeakExprVar0
1281  | WTypeVar WeakTypeVar0
1282  | WCoerVar WeakCoerVar0
1283
1284 weakTypeVarToKind :: WeakTypeVar0 -> Kind
1285 weakTypeVarToKind tv =
1286   (trace "X" (case (trace "X" (tv)) of {
1287                WeakTypeVar c k -> (trace "X" (k))}))
1288
1289 weakVarToCoreVar :: WeakVar -> Var.Var
1290 weakVarToCoreVar wv =
1291   (trace "X" (case (trace "X" (wv)) of {
1292                WExprVar w -> (trace "X" (case (trace "X" (w)) of {
1293                                           WeakExprVar v w0 -> (trace "X" (v))}));
1294                WTypeVar w -> (trace "X" (case (trace "X" (w)) of {
1295                                           WeakTypeVar v k -> (trace "X" (v))}));
1296                WCoerVar w -> (trace "X" (case (trace "X" (w)) of {
1297                                           WeakCoerVar v w0 w1 -> (trace "X" (v))}))}))
1298
1299 tyFunKind :: TyCon.TyCon -> (,) (([]) Kind) Kind
1300 tyFunKind tc =
1301   (trace "X" ((trace "X" (rawTyFunKind (trace "X" ((trace "X" (((\x -> x) (trace "X" (tc)))))))))))
1302
1303 data WeakAltCon =
1304    WeakDataAlt DataCon.DataCon
1305  | WeakLitAlt Literal.Literal
1306  | WeakDEFAULT
1307
1308 data WeakExpr =
1309    WEVar WeakExprVar0
1310  | WELit Literal.Literal
1311  | WELet WeakExprVar0 WeakExpr WeakExpr
1312  | WELetRec (Tree (Prelude.Maybe ((,) WeakExprVar0 WeakExpr))) WeakExpr
1313  | WECast WeakExpr WeakCoercion
1314  | WENote CoreSyn.Note WeakExpr
1315  | WEApp WeakExpr WeakExpr
1316  | WETyApp WeakExpr WeakType
1317  | WECoApp WeakExpr WeakCoercion
1318  | WELam WeakExprVar0 WeakExpr
1319  | WETyLam WeakTypeVar0 WeakExpr
1320  | WECoLam WeakCoerVar0 WeakExpr
1321  | WEBrak WeakExprVar0 WeakTypeVar0 WeakExpr WeakType
1322  | WEEsc WeakExprVar0 WeakTypeVar0 WeakExpr WeakType
1323  | WECSP WeakExprVar0 WeakTypeVar0 WeakExpr WeakType
1324  | WECase WeakExprVar0 WeakExpr WeakType TyCon.TyCon (([]) WeakType) (Tree (Prelude.Maybe ((,) ((,) ((,) ((,) WeakAltCon (([]) WeakTypeVar0)) (([]) WeakCoerVar0)) (([]) WeakExprVar0)) WeakExpr)))
1325
1326 mkTyFunApplication :: TyCon.TyCon -> (([]) WeakType) -> OrError WeakType
1327 mkTyFunApplication tf lwt =
1328   (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((split_list (trace "X" (lwt)) (trace "X" ((trace "X" ((length (trace "X" ((trace "X" ((fst (trace "X" ((trace "X" ((tyFunKind (trace "X" (tf)))))))))))))))))))))) (trace "X" ((\argsrest -> (trace "X" (case (trace "X" (argsrest)) of {
1329                                                                                                                                                                                                                                                                         (,) args rest -> (trace "X" (OK (trace "X" ((trace "X" ((fold_left (trace "X" ((\x y -> (trace "X" (WAppTy (trace "X" (x)) (trace "X" (y))))))) (trace "X" (rest)) (trace "X" ((WTyFunApp (trace "X" (tf)) (trace "X" (args))))))))))))})))))))))
1330
1331 coreTypeToWeakType' :: TypeRep.Type -> OrError WeakType
1332 coreTypeToWeakType' ct =
1333   (trace "X" (case (trace "X" (ct)) of {
1334                TypeRep.TyVarTy cv ->
1335                 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (cv)))))) of {
1336                              CVTWVR_EVar ct0 -> (trace "X" (Error (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1337                              CVTWVR_TyVar k -> (trace "X" (OK (trace "X" ((WTyVarTy (trace "X" ((WeakTypeVar (trace "X" (cv)) (trace "X" (k))))))))));
1338                              CVTWVR_CoVar t1 t2 -> (trace "X" (Error (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1339                TypeRep.AppTy t1 t2 -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t2))))))) (trace "X" ((\t2' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t1))))))) (trace "X" ((\t1' -> (trace "X" (OK (trace "X" ((WAppTy (trace "X" (t1')) (trace "X" (t2')))))))))))))))))))));
1340                TypeRep.TyConApp tc_ lct ->
1341                 (trace "X" (let {
1342                              recurse = (trace "X" ((trace "X" (let {
1343                                                                 rec tl =
1344                                                                   (trace "X" (case (trace "X" (tl)) of {
1345                                                                                ([]) -> (trace "X" (OK (trace "X" (([])))));
1346                                                                                (:) a b -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (a))))))) (trace "X" ((\a' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((rec (trace "X" (b))))))) (trace "X" ((\b' -> (trace "X" (OK (trace "X" (((:) (trace "X" (a')) (trace "X" (b')))))))))))))))))))))}))}
1347                                                                in rec (trace "X" (lct))))))}
1348                             in
1349                             (trace "X" (case (trace "X" ((trace "X" (tyConOrTyFun (trace "X" (tc_)))))) of {
1350                                          Prelude.Left tc ->
1351                                           (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (tyConEqDecidable)) (trace "X" (tc)) (trace "X" (TysWiredIn.hetMetCodeTypeTyCon)))))) of {
1352                                                        Prelude.True ->
1353                                                         (trace "X" (case (trace "X" (lct)) of {
1354                                                                      ([]) -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('-')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (':')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreTypeToString)) (trace "X" (ct))))))))))))));
1355                                                                      (:) c l ->
1356                                                                       (trace "X" (case (trace "X" (c)) of {
1357                                                                                    TypeRep.TyVarTy ec ->
1358                                                                                     (trace "X" (case (trace "X" (l)) of {
1359                                                                                                  ([]) -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('-')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (':')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreTypeToString)) (trace "X" (ct))))))))))))));
1360                                                                                                  (:) tbody l0 ->
1361                                                                                                   (trace "X" (case (trace "X" (l0)) of {
1362                                                                                                                ([]) ->
1363                                                                                                                 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (ec)))))) of {
1364                                                                                                                              CVTWVR_EVar ct0 -> (trace "X" (Error (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1365                                                                                                                              CVTWVR_TyVar k -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (tbody))))))) (trace "X" ((\tbody' -> (trace "X" (OK (trace "X" ((WCodeTy (trace "X" ((WeakTypeVar (trace "X" (ec)) (trace "X" (k))))) (trace "X" (tbody'))))))))))))));
1366                                                                                                                              CVTWVR_CoVar t1 t2 -> (trace "X" (Error (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1367                                                                                                                (:) c0 l1 -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('-')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (':')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreTypeToString)) (trace "X" (ct))))))))))))))}))}));
1368                                                                                    _ -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('-')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('m')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (':')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreTypeToString)) (trace "X" (ct))))))))))))))}))}));
1369                                                        Prelude.False ->
1370                                                         (trace "X" (let {
1371                                                                      tc' = (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (tyConEqDecidable)) (trace "X" (tc)) (trace "X" (arrowTyCon)))))) of {
1372                                                                                         Prelude.True -> (trace "X" (WFunTyCon));
1373                                                                                         Prelude.False -> (trace "X" (WTyCon (trace "X" (tc))))}))}
1374                                                                     in
1375                                                                     (trace "X" ((trace "X" (orErrorBind (trace "X" (recurse)) (trace "X" ((\recurse' -> (trace "X" (OK (trace "X" ((trace "X" ((fold_left (trace "X" ((\x y -> (trace "X" (WAppTy (trace "X" (x)) (trace "X" (y))))))) (trace "X" (recurse')) (trace "X" (tc'))))))))))))))))))}));
1376                                          Prelude.Right tf -> (trace "X" ((trace "X" (orErrorBind (trace "X" (recurse)) (trace "X" ((\recurse' -> (trace "X" ((trace "X" (mkTyFunApplication (trace "X" (tf)) (trace "X" (recurse')))))))))))))}))));
1377                TypeRep.FunTy t1 t2 ->
1378                 (trace "X" (case (trace "X" (t1)) of {
1379                              TypeRep.PredTy p ->
1380                               (trace "X" (case (trace "X" (p)) of {
1381                                            TypeRep.EqPred t3 t4 -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t3))))))) (trace "X" ((\t1' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t4))))))) (trace "X" ((\t2' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t2))))))) (trace "X" ((\t3' -> (trace "X" (OK (trace "X" ((WCoFunTy (trace "X" (t1')) (trace "X" (t2')) (trace "X" (t3'))))))))))))))))))))))))))));
1382                                            _ -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t1))))))) (trace "X" ((\t1' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t2))))))) (trace "X" ((\t2' -> (trace "X" (OK (trace "X" ((WAppTy (trace "X" ((WAppTy (trace "X" (WFunTyCon)) (trace "X" (t1'))))) (trace "X" (t2')))))))))))))))))))))}));
1383                              _ -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t1))))))) (trace "X" ((\t1' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t2))))))) (trace "X" ((\t2' -> (trace "X" (OK (trace "X" ((WAppTy (trace "X" ((WAppTy (trace "X" (WFunTyCon)) (trace "X" (t1'))))) (trace "X" (t2')))))))))))))))))))))}));
1384                TypeRep.ForAllTy cv t ->
1385                 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (cv)))))) of {
1386                              CVTWVR_EVar ct0 -> (trace "X" (Error (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1387                              CVTWVR_TyVar k -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t))))))) (trace "X" ((\t' -> (trace "X" (OK (trace "X" ((WForAllTy (trace "X" ((WeakTypeVar (trace "X" (cv)) (trace "X" (k))))) (trace "X" (t'))))))))))))));
1388                              CVTWVR_CoVar t1 t2 -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t1))))))) (trace "X" ((\t1' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t2))))))) (trace "X" ((\t2' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (t))))))) (trace "X" ((\t3' -> (trace "X" (OK (trace "X" ((WCoFunTy (trace "X" (t1')) (trace "X" (t2')) (trace "X" (t3'))))))))))))))))))))))))))))}));
1389                TypeRep.PredTy p ->
1390                 (trace "X" (case (trace "X" (p)) of {
1391                              TypeRep.ClassP cl lct ->
1392                               (trace "X" ((trace "X" (orErrorBind
1393                                                         (trace "X" ((trace "X" ((let {
1394                                                                                   rec tl =
1395                                                                                     (trace "X" (case (trace "X" (tl)) of {
1396                                                                                                  ([]) -> (trace "X" (OK (trace "X" (([])))));
1397                                                                                                  (:) a b -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (a))))))) (trace "X" ((\a' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((rec (trace "X" (b))))))) (trace "X" ((\b' -> (trace "X" (OK (trace "X" (((:) (trace "X" (a')) (trace "X" (b')))))))))))))))))))))}))}
1398                                                                                  in rec (trace "X" (lct))))))) (trace "X" ((\lct' -> (trace "X" (OK (trace "X" ((WClassP (trace "X" (cl)) (trace "X" (lct'))))))))))))));
1399                              TypeRep.IParam ipn ct0 -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" (ct0))))))) (trace "X" ((\ct' -> (trace "X" (OK (trace "X" ((WIParam (trace "X" (ipn)) (trace "X" (ct'))))))))))))));
1400                              TypeRep.EqPred c c0 -> (trace "X" (Error (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('q')) (trace "X" (((:) (trace "X" ('P')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))}))}))
1401
1402 coreTypeToWeakType :: TypeRep.Type -> OrError WeakType
1403 coreTypeToWeakType t =
1404   (trace "X" ((trace "X" (addErrorMessage (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('W')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('k')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreTypeToString)) (trace "X" (t)))))))))))) (trace "X" (eol))))))) (trace "X" ((trace "X" ((coreTypeToWeakType' (trace "X" ((trace "X" ((coreViewDeep (trace "X" (t))))))))))))))))
1405
1406 coreVarToWeakVar' :: Var.Var -> OrError WeakVar
1407 coreVarToWeakVar' cv =
1408   (trace "X" ((trace "X" (addErrorMessage (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('V')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('W')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('k')) (trace "X" (((:) (trace "X" ('V')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreVarToString)) (trace "X" (cv)))))))))))) (trace "X" (eol)))))))
1409                             (trace "X" ((case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (cv)))))) of {
1410                                           CVTWVR_EVar ct -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (ct))))))) (trace "X" ((\t' -> (trace "X" (OK (trace "X" ((WExprVar (trace "X" ((WeakExprVar (trace "X" (cv)) (trace "X" (t')))))))))))))))));
1411                                           CVTWVR_TyVar k -> (trace "X" (OK (trace "X" ((WTypeVar (trace "X" ((WeakTypeVar (trace "X" (cv)) (trace "X" (k))))))))));
1412                                           CVTWVR_CoVar t1 t2 -> (trace "X" ((trace "X" (addErrorMessage (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('2')) (trace "X" (((:) (trace "X" ('=')) (trace "X" ([])))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreTypeToString)) (trace "X" (t2)))))))))))) (trace "X" (eol))))))) (trace "X" ((trace "X" ((orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (t2))))))) (trace "X" ((\t2' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((addErrorMessage (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('1')) (trace "X" (((:) (trace "X" ('=')) (trace "X" ([])))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreTypeToString)) (trace "X" (t1)))))))))))) (trace "X" (eol))))))) (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (t1)))))))))))) (trace "X" ((\t1' -> (trace "X" (OK (trace "X" ((WCoerVar (trace "X" ((WeakCoerVar (trace "X" (cv)) (trace "X" (t1')) (trace "X" (t2')))))))))))))))))))))))))))))})))))))
1413
1414 tyConTyVars :: TyCon.TyCon -> ([]) WeakTypeVar0
1415 tyConTyVars tc =
1416   (trace "X" ((trace "X" (filter
1417                             (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1418                                                       (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar' (trace "X" (x)))))) of {
1419                                                                    Error error_message -> (trace "X" (Prelude.Nothing));
1420                                                                    OK w ->
1421                                                                     (trace "X" (case (trace "X" (w)) of {
1422                                                                                  WTypeVar v -> (trace "X" (Prelude.Just (trace "X" (v))));
1423                                                                                  _ -> (trace "X" (Prelude.Nothing))}))}))))) (trace "X" ((trace "X" ((getTyConTyVars (trace "X" (tc))))))))))))))))
1424
1425 tyConKind :: TyCon.TyCon -> ([]) Kind
1426 tyConKind tc =
1427   (trace "X" ((trace "X" (map (trace "X" ((\x -> (trace "X" ((trace "X" (weakTypeVarToKind (trace "X" (x))))))))) (trace "X" ((trace "X" ((tyConTyVars (trace "X" ((trace "X" (((\x -> x) (trace "X" (tc))))))))))))))))
1428
1429 isBrak :: (CoreSyn.Expr Var.Var) -> Prelude.Maybe ((,) ((,) WeakExprVar0 WeakTypeVar0) TypeRep.Type)
1430 isBrak ce =
1431   (trace "X" (case (trace "X" (ce)) of {
1432                CoreSyn.App c c0 ->
1433                 (trace "X" (case (trace "X" (c)) of {
1434                              CoreSyn.App c1 c2 ->
1435                               (trace "X" (case (trace "X" (c1)) of {
1436                                            CoreSyn.Var v ->
1437                                             (trace "X" (case (trace "X" (c2)) of {
1438                                                          CoreSyn.Type c3 ->
1439                                                           (trace "X" (case (trace "X" (c3)) of {
1440                                                                        TypeRep.TyVarTy ec ->
1441                                                                         (trace "X" (case (trace "X" (c0)) of {
1442                                                                                      CoreSyn.Type tbody ->
1443                                                                                       (trace "X" (case (trace "X" ((trace "X" ((==) (trace "X" (PrelNames.hetmet_brak_name)) (trace "X" ((trace "X" ((Var.varName (trace "X" (v))))))))))) of {
1444                                                                                                    Prelude.True ->
1445                                                                                                     (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar' (trace "X" (ec)))))) of {
1446                                                                                                                  Error error_message -> (trace "X" (Prelude.Nothing));
1447                                                                                                                  OK w ->
1448                                                                                                                   (trace "X" (case (trace "X" (w)) of {
1449                                                                                                                                WTypeVar tv ->
1450                                                                                                                                 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar' (trace "X" (v)))))) of {
1451                                                                                                                                              Error error_message -> (trace "X" (Prelude.Nothing));
1452                                                                                                                                              OK w0 ->
1453                                                                                                                                               (trace "X" (case (trace "X" (w0)) of {
1454                                                                                                                                                            WExprVar v' -> (trace "X" (Prelude.Just (trace "X" (((,) (trace "X" (((,) (trace "X" (v')) (trace "X" (tv))))) (trace "X" (tbody)))))));
1455                                                                                                                                                            _ -> (trace "X" (Prelude.Nothing))}))}));
1456                                                                                                                                _ -> (trace "X" (Prelude.Nothing))}))}));
1457                                                                                                    Prelude.False -> (trace "X" (Prelude.Nothing))}));
1458                                                                                      _ -> (trace "X" (Prelude.Nothing))}));
1459                                                                        _ -> (trace "X" (Prelude.Nothing))}));
1460                                                          _ -> (trace "X" (Prelude.Nothing))}));
1461                                            _ -> (trace "X" (Prelude.Nothing))}));
1462                              _ -> (trace "X" (Prelude.Nothing))}));
1463                _ -> (trace "X" (Prelude.Nothing))}))
1464
1465 isEsc :: (CoreSyn.Expr Var.Var) -> Prelude.Maybe ((,) ((,) WeakExprVar0 WeakTypeVar0) TypeRep.Type)
1466 isEsc ce =
1467   (trace "X" (case (trace "X" (ce)) of {
1468                CoreSyn.App c c0 ->
1469                 (trace "X" (case (trace "X" (c)) of {
1470                              CoreSyn.App c1 c2 ->
1471                               (trace "X" (case (trace "X" (c1)) of {
1472                                            CoreSyn.Var v ->
1473                                             (trace "X" (case (trace "X" (c2)) of {
1474                                                          CoreSyn.Type c3 ->
1475                                                           (trace "X" (case (trace "X" (c3)) of {
1476                                                                        TypeRep.TyVarTy ec ->
1477                                                                         (trace "X" (case (trace "X" (c0)) of {
1478                                                                                      CoreSyn.Type tbody ->
1479                                                                                       (trace "X" (case (trace "X" ((trace "X" ((==) (trace "X" (PrelNames.hetmet_esc_name)) (trace "X" ((trace "X" ((Var.varName (trace "X" (v))))))))))) of {
1480                                                                                                    Prelude.True ->
1481                                                                                                     (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar' (trace "X" (ec)))))) of {
1482                                                                                                                  Error error_message -> (trace "X" (Prelude.Nothing));
1483                                                                                                                  OK w ->
1484                                                                                                                   (trace "X" (case (trace "X" (w)) of {
1485                                                                                                                                WTypeVar tv ->
1486                                                                                                                                 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar' (trace "X" (v)))))) of {
1487                                                                                                                                              Error error_message -> (trace "X" (Prelude.Nothing));
1488                                                                                                                                              OK w0 ->
1489                                                                                                                                               (trace "X" (case (trace "X" (w0)) of {
1490                                                                                                                                                            WExprVar v' -> (trace "X" (Prelude.Just (trace "X" (((,) (trace "X" (((,) (trace "X" (v')) (trace "X" (tv))))) (trace "X" (tbody)))))));
1491                                                                                                                                                            _ -> (trace "X" (Prelude.Nothing))}))}));
1492                                                                                                                                _ -> (trace "X" (Prelude.Nothing))}))}));
1493                                                                                                    Prelude.False -> (trace "X" (Prelude.Nothing))}));
1494                                                                                      _ -> (trace "X" (Prelude.Nothing))}));
1495                                                                        _ -> (trace "X" (Prelude.Nothing))}));
1496                                                          _ -> (trace "X" (Prelude.Nothing))}));
1497                                            _ -> (trace "X" (Prelude.Nothing))}));
1498                              _ -> (trace "X" (Prelude.Nothing))}));
1499                _ -> (trace "X" (Prelude.Nothing))}))
1500
1501 isCSP :: (CoreSyn.Expr Var.Var) -> Prelude.Maybe ((,) ((,) WeakExprVar0 WeakTypeVar0) TypeRep.Type)
1502 isCSP ce =
1503   (trace "X" (case (trace "X" (ce)) of {
1504                CoreSyn.App c c0 ->
1505                 (trace "X" (case (trace "X" (c)) of {
1506                              CoreSyn.App c1 c2 ->
1507                               (trace "X" (case (trace "X" (c1)) of {
1508                                            CoreSyn.Var v ->
1509                                             (trace "X" (case (trace "X" (c2)) of {
1510                                                          CoreSyn.Type c3 ->
1511                                                           (trace "X" (case (trace "X" (c3)) of {
1512                                                                        TypeRep.TyVarTy ec ->
1513                                                                         (trace "X" (case (trace "X" (c0)) of {
1514                                                                                      CoreSyn.Type tbody ->
1515                                                                                       (trace "X" (case (trace "X" ((trace "X" ((==) (trace "X" (PrelNames.hetmet_csp_name)) (trace "X" ((trace "X" ((Var.varName (trace "X" (v))))))))))) of {
1516                                                                                                    Prelude.True ->
1517                                                                                                     (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar' (trace "X" (ec)))))) of {
1518                                                                                                                  Error error_message -> (trace "X" (Prelude.Nothing));
1519                                                                                                                  OK w ->
1520                                                                                                                   (trace "X" (case (trace "X" (w)) of {
1521                                                                                                                                WTypeVar tv ->
1522                                                                                                                                 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar' (trace "X" (v)))))) of {
1523                                                                                                                                              Error error_message -> (trace "X" (Prelude.Nothing));
1524                                                                                                                                              OK w0 ->
1525                                                                                                                                               (trace "X" (case (trace "X" (w0)) of {
1526                                                                                                                                                            WExprVar v' -> (trace "X" (Prelude.Just (trace "X" (((,) (trace "X" (((,) (trace "X" (v')) (trace "X" (tv))))) (trace "X" (tbody)))))));
1527                                                                                                                                                            _ -> (trace "X" (Prelude.Nothing))}))}));
1528                                                                                                                                _ -> (trace "X" (Prelude.Nothing))}))}));
1529                                                                                                    Prelude.False -> (trace "X" (Prelude.Nothing))}));
1530                                                                                      _ -> (trace "X" (Prelude.Nothing))}));
1531                                                                        _ -> (trace "X" (Prelude.Nothing))}));
1532                                                          _ -> (trace "X" (Prelude.Nothing))}));
1533                                            _ -> (trace "X" (Prelude.Nothing))}));
1534                              _ -> (trace "X" (Prelude.Nothing))}));
1535                _ -> (trace "X" (Prelude.Nothing))}))
1536
1537 expectTyConApp :: WeakType -> (([]) WeakType) -> OrError ((,) TyCon.TyCon (([]) WeakType))
1538 expectTyConApp wt acc =
1539   (trace "X" (case (trace "X" (wt)) of {
1540                WAppTy t1 t2 -> (trace "X" ((trace "X" (expectTyConApp (trace "X" (t1)) (trace "X" (((:) (trace "X" (t2)) (trace "X" (acc)))))))));
1541                WTyFunApp tc tys -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('F')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" (':')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (weakTypeToString)) (trace "X" (wt))))))))))))));
1542                WTyCon tc -> (trace "X" (OK (trace "X" (((,) (trace "X" (tc)) (trace "X" (acc)))))));
1543                _ -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('A')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (weakTypeToString)) (trace "X" (wt))))))))))))))}))
1544
1545 coreExprToWeakCoercion :: WeakType -> WeakType -> (CoreSyn.Expr Var.Var) -> OrError WeakCoercion
1546 coreExprToWeakCoercion t1 t2 ce =
1547   (trace "X" (case (trace "X" (ce)) of {
1548                CoreSyn.Type t -> (trace "X" (OK (trace "X" ((WCoUnsafe (trace "X" (t1)) (trace "X" (t2)))))));
1549                _ -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('W')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('k')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreExprToString)) (trace "X" (ce))))))))))))))}))
1550
1551 coreExprToWeakType :: (CoreSyn.Expr Var.Var) -> OrError WeakType
1552 coreExprToWeakType ce =
1553   (trace "X" (case (trace "X" (ce)) of {
1554                CoreSyn.Type t -> (trace "X" ((trace "X" (coreTypeToWeakType (trace "X" (t))))));
1555                _ -> (trace "X" (Error (trace "X" ((trace "X" ((concatenate (trace "X" (concatenableString)) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('W')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('k')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('g')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (trace "X" ((trace "X" ((toString (trace "X" (coreExprToString)) (trace "X" (ce))))))))))))))}))
1556
1557 coreExprToWeakExpr :: (CoreSyn.Expr Var.Var) -> OrError WeakExpr
1558 coreExprToWeakExpr ce =
1559   (trace "X" (case (trace "X" (ce)) of {
1560                CoreSyn.Var v ->
1561                 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreVarToWeakVar' (trace "X" (v))))))) (trace "X" ((\v' ->
1562                                           (trace "X" (case (trace "X" (v')) of {
1563                                                        WExprVar ev -> (trace "X" (OK (trace "X" ((WEVar (trace "X" (ev)))))));
1564                                                        WTypeVar w -> (trace "X" (Error (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('V')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('!')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1565                                                        WCoerVar w -> (trace "X" (Error (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('V')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('!')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))})))))))));
1566                CoreSyn.Lit lit -> (trace "X" (OK (trace "X" ((WELit (trace "X" (lit)))))));
1567                CoreSyn.App e1 e2 ->
1568                 (trace "X" (case (trace "X" ((trace "X" (isBrak (trace "X" (e1)))))) of {
1569                              Prelude.Just p ->
1570                               (trace "X" (case (trace "X" (p)) of {
1571                                            (,) p0 t -> (trace "X" (case (trace "X" (p0)) of {
1572                                                                     (,) v tv -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e2))))))) (trace "X" ((\e' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (t))))))) (trace "X" ((\t' -> (trace "X" (OK (trace "X" ((WEBrak (trace "X" (v)) (trace "X" (tv)) (trace "X" (e')) (trace "X" (t')))))))))))))))))))))}))}));
1573                              Prelude.Nothing ->
1574                               (trace "X" (case (trace "X" ((trace "X" (isEsc (trace "X" (e1)))))) of {
1575                                            Prelude.Just p ->
1576                                             (trace "X" (case (trace "X" (p)) of {
1577                                                          (,) p0 t -> (trace "X" (case (trace "X" (p0)) of {
1578                                                                                   (,) v tv -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e2))))))) (trace "X" ((\e' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (t))))))) (trace "X" ((\t' -> (trace "X" (OK (trace "X" ((WEEsc (trace "X" (v)) (trace "X" (tv)) (trace "X" (e')) (trace "X" (t')))))))))))))))))))))}))}));
1579                                            Prelude.Nothing ->
1580                                             (trace "X" (case (trace "X" ((trace "X" (isCSP (trace "X" (e1)))))) of {
1581                                                          Prelude.Just p ->
1582                                                           (trace "X" (case (trace "X" (p)) of {
1583                                                                        (,) p0 t -> (trace "X" (case (trace "X" (p0)) of {
1584                                                                                                 (,) v tv -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e2))))))) (trace "X" ((\e' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (t))))))) (trace "X" ((\t' -> (trace "X" (OK (trace "X" ((WECSP (trace "X" (v)) (trace "X" (tv)) (trace "X" (e')) (trace "X" (t')))))))))))))))))))))}))}));
1585                                                          Prelude.Nothing ->
1586                                                           (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e1))))))) (trace "X" ((\e1' ->
1587                                                                                     (trace "X" (case (trace "X" (e2)) of {
1588                                                                                                  CoreSyn.Type t -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (t))))))) (trace "X" ((\t' -> (trace "X" (OK (trace "X" ((WETyApp (trace "X" (e1')) (trace "X" (t'))))))))))))));
1589                                                                                                  _ -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e2))))))) (trace "X" ((\e2' -> (trace "X" (OK (trace "X" ((WEApp (trace "X" (e1')) (trace "X" (e2'))))))))))))))})))))))))}))}))}));
1590                CoreSyn.Lam v e ->
1591                 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreVarToWeakVar' (trace "X" (v))))))) (trace "X" ((\v' ->
1592                                           (trace "X" (case (trace "X" (v')) of {
1593                                                        WExprVar ev -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" (OK (trace "X" ((WELam (trace "X" (ev)) (trace "X" (e'))))))))))))));
1594                                                        WTypeVar tv -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" (OK (trace "X" ((WETyLam (trace "X" (tv)) (trace "X" (e'))))))))))))));
1595                                                        WCoerVar cv -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" (OK (trace "X" ((WECoLam (trace "X" (cv)) (trace "X" (e'))))))))))))))})))))))));
1596                CoreSyn.Let c e ->
1597                 (trace "X" (case (trace "X" (c)) of {
1598                              CoreSyn.NonRec v ve ->
1599                               (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreVarToWeakVar' (trace "X" (v))))))) (trace "X" ((\v' ->
1600                                                         (trace "X" (case (trace "X" (v')) of {
1601                                                                      WExprVar ev -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (ve))))))) (trace "X" ((\ve' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" (OK (trace "X" ((WELet (trace "X" (ev)) (trace "X" (ve')) (trace "X" (e')))))))))))))))))))));
1602                                                                      WTypeVar tv ->
1603                                                                       (trace "X" (case (trace "X" (e)) of {
1604                                                                                    CoreSyn.Type t -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakType (trace "X" (ve))))))) (trace "X" ((\ty' -> (trace "X" (OK (trace "X" ((WETyApp (trace "X" ((WETyLam (trace "X" (tv)) (trace "X" (e'))))) (trace "X" (ty')))))))))))))))))))));
1605                                                                                    _ -> (trace "X" (Error (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('(')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('L')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('<')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('>')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (')')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('!')) (trace "X" (((:) (trace "X" ('=')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1606                                                                      WCoerVar w -> (trace "X" (case (trace "X" (w)) of {
1607                                                                                                 WeakCoerVar cv t1 t2 -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakCoercion (trace "X" (t1)) (trace "X" (t2)) (trace "X" (ve))))))) (trace "X" ((\co' -> (trace "X" (OK (trace "X" ((WECoApp (trace "X" ((WECoLam (trace "X" ((WeakCoerVar (trace "X" (cv)) (trace "X" (t1)) (trace "X" (t2))))) (trace "X" (e'))))) (trace "X" (co')))))))))))))))))))))}))})))))))));
1608                              CoreSyn.Rec rb ->
1609                               (trace "X" ((trace "X" (orErrorBind
1610                                                         (trace "X" ((trace "X" ((let {
1611                                                                                   coreExprToWeakExprList cel =
1612                                                                                     (trace "X" (case (trace "X" (cel)) of {
1613                                                                                                  ([]) -> (trace "X" (OK (trace "X" (([])))));
1614                                                                                                  (:) p t ->
1615                                                                                                   (trace "X" (case (trace "X" (p)) of {
1616                                                                                                                (,) v' e' ->
1617                                                                                                                 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExprList (trace "X" (t))))))) (trace "X" ((\t' ->
1618                                                                                                                                           (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreVarToWeakVar' (trace "X" (v'))))))) (trace "X" ((\v'' ->
1619                                                                                                                                                                     (trace "X" (case (trace "X" (v'')) of {
1620                                                                                                                                                                                  WExprVar ev -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e'))))))) (trace "X" ((\e'0 -> (trace "X" (OK (trace "X" (((:) (trace "X" (((,) (trace "X" (ev)) (trace "X" (e'0))))) (trace "X" (t'))))))))))))));
1621                                                                                                                                                                                  WTypeVar w -> (trace "X" (Error (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1622                                                                                                                                                                                  WCoerVar w -> (trace "X" (Error (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('t')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}))))))))))))))))}))}))}
1623                                                                                  in coreExprToWeakExprList (trace "X" (rb))))))) (trace "X" ((\rb' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" (OK (trace "X" ((WELetRec (trace "X" ((trace "X" ((unleaves' (trace "X" (rb'))))))) (trace "X" (e')))))))))))))))))))))}));
1624                CoreSyn.Case e v tbranches alts ->
1625                 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreVarToWeakVar' (trace "X" (v))))))) (trace "X" ((\v' ->
1626                                           (trace "X" (case (trace "X" (v')) of {
1627                                                        WExprVar ev ->
1628                                                         (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" ((trace "X" ((CoreUtils.exprType (trace "X" (e)))))))))))) (trace "X" ((\te' ->
1629                                                                                   (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((expectTyConApp (trace "X" (te')) (trace "X" (([])))))))) (trace "X" ((\tca ->
1630                                                                                                             (trace "X" (case (trace "X" (tca)) of {
1631                                                                                                                          (,) tc lt ->
1632                                                                                                                           (trace "X" ((trace "X" (orErrorBind
1633                                                                                                                                                     (trace "X" ((trace "X" ((let {
1634                                                                                                                                                                               mkBranches branches =
1635                                                                                                                                                                                 (trace "X" (case (trace "X" (branches)) of {
1636                                                                                                                                                                                              ([]) -> (trace "X" (OK (trace "X" (([])))));
1637                                                                                                                                                                                              (:) t rest ->
1638                                                                                                                                                                                               (trace "X" (case (trace "X" (t)) of {
1639                                                                                                                                                                                                            (,,) alt vars e0 ->
1640                                                                                                                                                                                                             (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((mkBranches (trace "X" (rest))))))) (trace "X" ((\rest' ->
1641                                                                                                                                                                                                                                       (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e0))))))) (trace "X" ((\e' ->
1642                                                                                                                                                                                                                                                                 (trace "X" (case (trace "X" (alt)) of {
1643                                                                                                                                                                                                                                                                              CoreSyn.DataAlt dc ->
1644                                                                                                                                                                                                                                                                               (trace "X" (let {vars0 = (trace "X" ((trace "X" (map (trace "X" (coreVarToWeakVar')) (trace "X" (vars))))))} in
1645                                                                                                                                                                                                                                                                                           (trace "X" (OK (trace "X" (((:) (trace "X" (((,) (trace "X" (((,) (trace "X" (((,) (trace "X" (((,) (trace "X" ((WeakDataAlt (trace "X" (dc)))))
1646                                                                                                                                                                                                                                                                                           (trace "X" ((trace "X" ((filter
1647                                                                                                                                                                                                                                                                                                                     (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1648                                                                                                                                                                                                                                                                                                                                               (trace "X" (case (trace "X" (x)) of {
1649                                                                                                                                                                                                                                                                                                                                                            Error error_message -> (trace "X" (Prelude.Nothing));
1650                                                                                                                                                                                                                                                                                                                                                            OK y ->
1651                                                                                                                                                                                                                                                                                                                                                             (trace "X" (case (trace "X" (y)) of {
1652                                                                                                                                                                                                                                                                                                                                                                          WTypeVar v0 -> (trace "X" (Prelude.Just (trace "X" (v0))));
1653                                                                                                                                                                                                                                                                                                                                                                          _ -> (trace "X" (Prelude.Nothing))}))}))))) (trace "X" (vars0)))))))))))))))
1654                                                                                                                                                                                                                                                                                           (trace "X" ((trace "X" ((filter
1655                                                                                                                                                                                                                                                                                                                     (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1656                                                                                                                                                                                                                                                                                                                                               (trace "X" (case (trace "X" (x)) of {
1657                                                                                                                                                                                                                                                                                                                                                            Error error_message -> (trace "X" (Prelude.Nothing));
1658                                                                                                                                                                                                                                                                                                                                                            OK y ->
1659                                                                                                                                                                                                                                                                                                                                                             (trace "X" (case (trace "X" (y)) of {
1660                                                                                                                                                                                                                                                                                                                                                                          WCoerVar v0 -> (trace "X" (Prelude.Just (trace "X" (v0))));
1661                                                                                                                                                                                                                                                                                                                                                                          _ -> (trace "X" (Prelude.Nothing))}))}))))) (trace "X" (vars0)))))))))))))))
1662                                                                                                                                                                                                                                                                                           (trace "X" ((trace "X" ((filter
1663                                                                                                                                                                                                                                                                                                                     (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1664                                                                                                                                                                                                                                                                                                                                               (trace "X" (case (trace "X" (x)) of {
1665                                                                                                                                                                                                                                                                                                                                                            Error error_message -> (trace "X" (Prelude.Nothing));
1666                                                                                                                                                                                                                                                                                                                                                            OK y ->
1667                                                                                                                                                                                                                                                                                                                                                             (trace "X" (case (trace "X" (y)) of {
1668                                                                                                                                                                                                                                                                                                                                                                          WExprVar v0 -> (trace "X" (Prelude.Just (trace "X" (v0))));
1669                                                                                                                                                                                                                                                                                                                                                                          _ -> (trace "X" (Prelude.Nothing))}))}))))) (trace "X" (vars0))))))))))))))) (trace "X" (e'))))) (trace "X" (rest')))))))));
1670                                                                                                                                                                                                                                                                              CoreSyn.LitAlt lit -> (trace "X" (OK (trace "X" (((:) (trace "X" (((,) (trace "X" (((,) (trace "X" (((,) (trace "X" (((,) (trace "X" ((WeakLitAlt (trace "X" (lit))))) (trace "X" (([])))))) (trace "X" (([])))))) (trace "X" (([])))))) (trace "X" (e'))))) (trace "X" (rest')))))));
1671                                                                                                                                                                                                                                                                              CoreSyn.DEFAULT -> (trace "X" (OK (trace "X" (((:) (trace "X" (((,) (trace "X" (((,) (trace "X" (((,) (trace "X" (((,) (trace "X" (WeakDEFAULT)) (trace "X" (([])))))) (trace "X" (([])))))) (trace "X" (([])))))) (trace "X" (e'))))) (trace "X" (rest')))))))}))))))))))))))))}))}))}
1672                                                                                                                                                                              in mkBranches (trace "X" (alts))))))) (trace "X" ((\branches -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\scrutinee -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (tbranches))))))) (trace "X" ((\tbranches' -> (trace "X" (OK (trace "X" ((WECase (trace "X" (ev)) (trace "X" (scrutinee)) (trace "X" (tbranches')) (trace "X" (tc)) (trace "X" (lt)) (trace "X" ((trace "X" ((unleaves (trace "X" (branches)))))))))))))))))))))))))))))))))}))))))))))))))));
1673                                                        WTypeVar w -> (trace "X" (Error (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1674                                                        WCoerVar w -> (trace "X" (Error (trace "X" (((:) (trace "X" ('f')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('e')) (trace "X" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))})))))))));
1675                CoreSyn.Cast e co -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" (case (trace "X" ((trace "X" ((\x -> Pair.unPair (Coercion.coercionKind x)) (trace "X" (co)))))) of {
1676                                                                                                                                                                           (,) ct1 ct2 -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (ct1))))))) (trace "X" ((\t1 -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (ct2))))))) (trace "X" ((\t2 -> (trace "X" (OK (trace "X" ((WECast (trace "X" (e')) (trace "X" ((WCoUnsafe (trace "X" (t1)) (trace "X" (t2))))))))))))))))))))))))})))))))));
1677                CoreSyn.Note n e -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e))))))) (trace "X" ((\e' -> (trace "X" (OK (trace "X" ((WENote (trace "X" (n)) (trace "X" (e'))))))))))))));
1678                CoreSyn.Type t -> (trace "X" (Error (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('T')) (trace "X" (((:) (trace "X" ('y')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1679                CoreSyn.Coercion co -> (trace "X" (Error (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('C')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('c')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('t')) (trace "X" (((:) (trace "X" ('i')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('w')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('n')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('E')) (trace "X" (((:) (trace "X" ('x')) (trace "X" (((:) (trace "X" ('p')) (trace "X" (((:) (trace "X" ('r')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('s')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('o')) (trace "X" (((:) (trace "X" ('u')) (trace "X" (((:) (trace "X" ('l')) (trace "X" (((:) (trace "X" ('d')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('h')) (trace "X" (((:) (trace "X" ('a')) (trace "X" (((:) (trace "X" ('v')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" (' ')) (trace "X" (((:) (trace "X" ('b')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('e')) (trace "X" (((:) (trace "X" ('n')) (trace "X" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}))
1680
1681 dataConExTyVars :: DataCon.DataCon -> ([]) WeakTypeVar0
1682 dataConExTyVars cdc =
1683   (trace "X" ((trace "X" (filter
1684                             (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1685                                                       (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar' (trace "X" (x)))))) of {
1686                                                                    Error error_message -> (trace "X" (Prelude.Nothing));
1687                                                                    OK w ->
1688                                                                     (trace "X" (case (trace "X" (w)) of {
1689                                                                                  WTypeVar v -> (trace "X" (Prelude.Just (trace "X" (v))));
1690                                                                                  _ -> (trace "X" (Prelude.Nothing))}))}))))) (trace "X" ((trace "X" ((DataCon.dataConExTyVars (trace "X" (cdc))))))))))))))))
1691
1692 dataConCoerKinds :: DataCon.DataCon -> ([]) ((,) WeakType WeakType)
1693 dataConCoerKinds cdc =
1694   (trace "X" ((trace "X" (filter
1695                             (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1696                                                       (trace "X" (case (trace "X" (x)) of {
1697                                                                    TypeRep.EqPred t1 t2 ->
1698                                                                     (trace "X" (case (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (t1))))))) (trace "X" ((\t1' -> (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" (t2))))))) (trace "X" ((\t2' -> (trace "X" (OK (trace "X" (((,) (trace "X" (t1')) (trace "X" (t2'))))))))))))))))))))) of {
1699                                                                                  Error error_message -> (trace "X" (Prelude.Nothing));
1700                                                                                  OK z -> (trace "X" (Prelude.Just (trace "X" (z))))}));
1701                                                                    _ -> (trace "X" (Prelude.Nothing))}))))) (trace "X" ((trace "X" ((DataCon.dataConTheta (trace "X" (cdc))))))))))))))))
1702
1703 dataConFieldTypes :: DataCon.DataCon -> ([]) WeakType
1704 dataConFieldTypes cdc =
1705   (trace "X" ((trace "X" (filter
1706                             (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1707                                                       (trace "X" (case (trace "X" ((trace "X" (coreTypeToWeakType (trace "X" (x)))))) of {
1708                                                                    Error error_message -> (trace "X" (Prelude.Nothing));
1709                                                                    OK z -> (trace "X" (Prelude.Just (trace "X" (z))))}))))) (trace "X" ((trace "X" ((DataCon.dataConOrigArgTys (trace "X" (cdc))))))))))))))))
1710
1711 type DataCon =
1712   DataCon.DataCon
1713   -- singleton inductive, whose constructor was mkDataCon
1714   
1715 dataConToCoreDataCon :: TyCon.TyCon -> DataCon -> DataCon.DataCon
1716 dataConToCoreDataCon tc dc =
1717   (trace "X" (dc))
1718
1719 tyConKind' :: TyCon.TyCon -> Kind
1720 tyConKind' tc =
1721   (trace "X" ((trace "X" (fold_right (trace "X" ((\x x0 -> (trace "X" (KindArrow (trace "X" (x)) (trace "X" (x0))))))) (trace "X" (KindStar)) (trace "X" ((trace "X" ((tyConKind (trace "X" (tc)))))))))))
1722
1723 data RawHaskType tV =
1724    TVar Kind tV
1725  | TCon TyCon.TyCon
1726  | TArrow
1727  | TCoerc Kind (RawHaskType tV) (RawHaskType tV) (RawHaskType tV)
1728  | TApp Kind Kind (RawHaskType tV) (RawHaskType tV)
1729  | TAll Kind (tV -> RawHaskType tV)
1730  | TCode (RawHaskType tV) (RawHaskType tV)
1731  | TyFunApp TyCon.TyCon (([]) Kind) Kind (RawHaskTypeList tV)
1732 data RawHaskTypeList tV =
1733    TyFunApp_nil
1734  | TyFunApp_cons Kind (([]) Kind) (RawHaskType tV) (RawHaskTypeList tV)
1735
1736 data RawCoercionKind tV =
1737    MkRawCoercionKind Kind (RawHaskType tV) (RawHaskType tV)
1738
1739 type TypeEnv = ([]) Kind
1740
1741 type InstantiatedTypeEnv tV = IList Kind tV
1742
1743 type HaskCoercionKind = () -> (InstantiatedTypeEnv ()) -> RawCoercionKind ()
1744
1745 type CoercionEnv = ([]) HaskCoercionKind
1746
1747 type InstantiatedCoercionEnv tV cV = Vec cV
1748
1749 type HaskTyVar = () -> (InstantiatedTypeEnv ()) -> ()