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