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