1 {-# OPTIONS_GHC -fno-warn-unused-matches -fno-warn-unused-binds -fno-warn-unused-imports #-}
2 module CoqPass ( coqPassCoreToString, coqPassCoreToCore )
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
13 import qualified Literal
15 import qualified TypeRep
16 import qualified DataCon
17 import qualified TyCon
18 import qualified Coercion
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
37 getTyConTyVars :: TyCon.TyCon -> [Var.TyVar]
39 if TyCon.isFunTyCon tc
41 else if TyCon.isPrimTyCon tc
43 else TyCon.tyConTyVars tc
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
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
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))))))
61 Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!"
63 errOrFail :: OrError t -> t
65 errOrFail (Error s) = Prelude.error s
67 rawTyFunKind :: TyCon.TyCon -> ( [Kind] , Kind )
68 rawTyFunKind tc = ((Prelude.map coreKindToKind (Prelude.take (TyCon.tyConArity tc) argk))
70 coreKindToKind (Coercion.mkArrowKinds (Prelude.drop (TyCon.tyConArity tc) argk) retk))
71 where (argk,retk) = Coercion.splitKindFunTys (TyCon.tyConKind tc)
73 tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon
75 if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars
77 else if TyCon.isFamInstTyCon n
79 else if TyCon.isSynTyCon n
83 nat2int :: Nat -> Prelude.Int
85 nat2int (S x) = 1 + (nat2int x)
87 natToString :: Nat -> Prelude.String
88 natToString n = show (nat2int n)
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)
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 "
103 coreKindToKind :: TypeRep.Kind -> Kind
105 case Coercion.splitKindFunTy_maybe k of
106 Prelude.Just (k1,k2) -> KindArrow (coreKindToKind k1) (coreKindToKind k2)
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
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.
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
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))
129 coreViewDeep :: Type.Type -> Type.Type
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'
144 coreCoercionToWeakCoercion :: Type.Type -> WeakCoercion
145 coreCoercionToWeakCoercion c =
146 WCoUnsafe (errOrFail (coreTypeToWeakType t1)) (errOrFail (coreTypeToWeakType t2))
148 (t1,t2) = Coercion.coercionKind c
150 -- REMEMBER: cotycon applications may be oversaturated
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) ->
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))
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)
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)
192 {-# NOINLINE trace #-}
193 trace :: Prelude.String -> a -> a
196 --trace = Debug.Trace.trace
198 --trace msg x = System.IO.Unsafe.unsafePerformIO $ Prelude.return 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)
206 {- -- used for extracting strings WITHOUT the patch for Coq
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))
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" -}
221 #ifdef __GLASGOW_HASKELL__
222 unsafeCoerce = GHC.Base.unsafeCoerce#
225 unsafeCoerce = IOExts.unsafeCoerce
228 __ = Prelude.error "Logical or arity value used"
232 (trace "X" (Prelude.error "absurd case"))
234 eq_rect :: a1 -> a2 -> a1 -> a2
238 eq_rec :: a1 -> a2 -> a1 -> a2
240 (trace "X" ((trace "X" (eq_rect (trace "X" (x)) (trace "X" (f)) (trace "X" (y))))))
242 eq_rec_r :: a1 -> a2 -> a1 -> a2
244 (trace "X" ((trace "X" (eq_rec (trace "X" (x)) (trace "X" (h)) (trace "X" (y))))))
246 eq_rect_r :: a1 -> a2 -> a1 -> a2
248 (trace "X" ((trace "X" (eq_rect (trace "X" (x)) (trace "X" (h)) (trace "X" (y))))))
254 nat_rect :: a1 -> (Nat -> a1 -> a1) -> Nat -> a1
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)))))))))))}))
260 nat_rec :: a1 -> (Nat -> a1 -> a1) -> Nat -> a1
262 (trace "X" (nat_rect))
264 fst :: ((,) a1 a2) -> a1
266 (trace "X" (case (trace "X" (p)) of {
267 (,) x y -> (trace "X" (x))}))
269 snd :: ((,) a1 a2) -> a2
271 (trace "X" (case (trace "X" (p)) of {
272 (,) x y -> (trace "X" (y))}))
274 list_rect :: a2 -> (a1 -> (([]) a1) -> a2 -> a2) -> (([]) a1) -> a2
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)))))))))))}))
280 list_rec :: a2 -> (a1 -> (([]) a1) -> a2 -> a2) -> (([]) a1) -> a2
282 (trace "X" (list_rect))
284 length :: (([]) a1) -> Nat
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')))))))))}))
290 app :: (([]) a1) -> (([]) a1) -> ([]) a1
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)))))))))}))
298 -- singleton inductive, whose constructor was exist
303 projT1 :: (SigT a1 a2) -> a1
305 (trace "X" (case (trace "X" (x)) of {
306 ExistT a p -> (trace "X" (a))}))
308 projT2 :: (SigT a1 a2) -> a2
310 (trace "X" (case (trace "X" (x)) of {
311 ExistT x0 h -> (trace "X" (h))}))
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" (__))))))}))
319 sumbool_rec :: (() -> a1) -> (() -> a1) -> Prelude.Bool -> a1
321 (trace "X" (sumbool_rect))
323 plus :: Nat -> Nat -> Nat
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)))))))))}))
329 eq_nat_dec :: Nat -> Nat -> Prelude.Bool
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))))))
339 map :: (a1 -> a2) -> (([]) a1) -> ([]) a2
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)))))))))}))
345 fold_left :: (a1 -> a2 -> a1) -> (([]) a2) -> a1 -> a1
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)))))))))))}))
351 fold_right :: (a2 -> a1 -> a1) -> a1 -> (([]) a2) -> a1
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)))))))))))}))
357 append :: Prelude.String -> Prelude.String -> Prelude.String
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)))))))))}))
363 type EqDecider t = t -> t -> Prelude.Bool
366 t -> t -> Prelude.Bool
367 -- singleton inductive, whose constructor was Build_EqDecidable
369 eqd_dec :: (EqDecidable a1) -> a1 -> a1 -> Prelude.Bool
370 eqd_dec eqDecidable =
371 (trace "X" (eqDecidable))
373 eqDecidableOption :: (EqDecidable a1) -> EqDecidable (Prelude.Maybe a1)
374 eqDecidableOption eQDT v1 v2 =
375 (trace "X" (case (trace "X" (v1)) of {
377 (trace "X" (case (trace "X" (v2)) of {
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))}));
385 (trace "X" (case (trace "X" (v2)) of {
386 Prelude.Just t -> (trace "X" (Prelude.False));
387 Prelude.Nothing -> (trace "X" (Prelude.True))}))}))
391 -- singleton inductive, whose constructor was Build_ToString
393 toString :: (ToString a1) -> a1 -> Prelude.String
395 (trace "X" (toString0))
397 type Concatenable t =
399 -- singleton inductive, whose constructor was Build_Concatenable
401 concatenate :: (Concatenable a1) -> a1 -> a1 -> a1
402 concatenate concatenable =
403 (trace "X" (concatenable))
405 concatenableString :: Concatenable Prelude.String
411 | T_Branch (Tree a) (Tree a)
413 tree_rect :: (a1 -> a2) -> ((Tree a1) -> a2 -> (Tree a1) -> a2 -> a2) -> (Tree a1) -> a2
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)))))))))))}))
419 mapTree :: (a1 -> a2) -> (Tree a1) -> Tree a2
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)))))))))}))
425 mapOptionTree :: (a1 -> a2) -> (Tree (Prelude.Maybe a1)) -> Tree (Prelude.Maybe a2)
427 (trace "X" (case (trace "X" (t)) of {
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)))))))))}))
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 {
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)))))))))}))
443 reduceTree :: a1 -> (a1 -> a1 -> a1) -> (Tree (Prelude.Maybe a1)) -> a1
444 reduceTree unit0 merge tt =
445 (trace "X" (case (trace "X" (tt)) of {
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)))))))))))}))
452 leaves :: (Tree (Prelude.Maybe a1)) -> ([]) a1
454 (trace "X" (case (trace "X" (t)) of {
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)))))))))))}))
461 unleaves :: (([]) a1) -> Tree (Prelude.Maybe a1)
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)))))))))}))
467 unleaves' :: (([]) a1) -> Tree (Prelude.Maybe a1)
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))))))))))}))
473 filter :: (([]) (Prelude.Maybe a1)) -> ([]) a1
475 (trace "X" (case (trace "X" (l)) of {
476 ([]) -> (trace "X" (([])));
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))))))}))}))
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));
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))))))
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 {
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))))))
504 list_eq_dec :: (([]) a1) -> (([]) a1) -> (a1 -> a1 -> Prelude.Bool) -> Prelude.Bool
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));
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 {
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))))))
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)))))))))))
530 | Tf_branch (Tree t) (Tree t) (TreeFlags t) (TreeFlags t)
532 mkFlags :: (a1 -> Prelude.Bool) -> (Tree a1) -> TreeFlags a1
534 (trace "X" (case (trace "X" (t)) of {
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)))))))))}))
541 dropT :: (Tree (Prelude.Maybe a1)) -> (TreeFlags (Prelude.Maybe a1)) -> Tree (Prelude.Maybe a1)
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)))))))))}))
548 liftBoolFunc :: Prelude.Bool -> (a1 -> Prelude.Bool) -> (Prelude.Maybe a1) -> Prelude.Bool
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))}))
554 tree_eq_dec :: (Tree a1) -> (Tree a1) -> (a1 -> a1 -> Prelude.Bool) -> Prelude.Bool
556 (trace "X" ((trace "X" (tree_rect (trace "X" ((\a l2 dec ->
557 (trace "X" (case (trace "X" (l2)) of {
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 {
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))))))}))));
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))))))
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)))))))))))
586 | Vec_cons Nat a (Vec a)
588 vec2list :: Nat -> (Vec a1) -> ([]) a1
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)))))))))}))
594 vec_zip :: Nat -> (Vec a1) -> (Vec a2) -> Vec ((,) a1 a2)
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));
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))))))
605 vec_map :: Nat -> (a1 -> a2) -> (Vec a1) -> Vec a2
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))))))
612 list2vec :: (([]) a1) -> Vec a1
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 {
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))))))
622 vec_chop' :: (([]) a1) -> (([]) a1) -> (Vec a2) -> Vec a2
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))))))
632 | ICons i (([]) i) f (IList i f)
634 ilist_head :: a1 -> (([]) a1) -> (IList a1 a2) -> a2
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))))))}))
640 ilist_tail :: a1 -> (([]) a1) -> (IList a1 a2) -> IList a1 a2
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))))))}))
646 ilmap :: (([]) a1) -> (a1 -> a2 -> a3) -> (IList a1 a2) -> IList a1 a3
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))))))
653 ilist_chop :: (([]) a1) -> (([]) a1) -> (IList a1 a2) -> IList a1 a2
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))))))
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))))))
672 ilist_to_list :: (([]) a1) -> (IList a1 a2) -> ([]) a2
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)))))))))}))
681 | IBranch (Tree (Prelude.Maybe i)) (Tree (Prelude.Maybe i)) (ITree i f) (ITree i f)
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)))))))))))}))
690 itmap :: (Tree (Prelude.Maybe a1)) -> (a1 -> a2 -> a3) -> (ITree a1 a2) -> ITree a1 a3
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))))))
710 bnot :: Prelude.Bool -> Prelude.Bool
712 (trace "X" (case (trace "X" (b)) of {
713 Prelude.True -> (trace "X" (Prelude.False));
714 Prelude.False -> (trace "X" (Prelude.True))}))
716 eol :: Prelude.String
720 Build_Monad (() -> () -> t) (() -> () -> t -> (() -> t) -> t)
722 returnM :: (Monad a1) -> a2 -> a1
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))))))}))
727 bindM :: (Monad a1) -> a1 -> (a2 -> a1) -> a1
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))))))}))
736 orErrorBind :: (OrError a1) -> (a1 -> OrError a2) -> OrError a2
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))))))}))
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))))))}))
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))))))
752 eqDecidableNat :: EqDecidable Nat
753 eqDecidableNat v1 v2 =
754 (trace "X" ((trace "X" (eq_nat_dec (trace "X" (v1)) (trace "X" (v2))))))
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)))))))))}))))))
764 split_list :: (([]) a1) -> Nat -> OrError ((,) (([]) a1) (([]) a1))
766 (trace "X" (case (trace "X" (n)) of {
767 O -> (trace "X" (OK (trace "X" (((,) (trace "X" (([]))) (trace "X" (l)))))));
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)))))))})))))))))}))}))
775 UniqSupply.UniqSupply -> OrError ((,) UniqSupply.UniqSupply t)
776 -- singleton inductive, whose constructor was uniqM
778 uniqMonad :: Monad (UniqM ())
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'))))))}))})))))))
786 getU :: UniqM Unique.Unique
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))))))))))))}))
792 Build_FreshMonad (Monad ()) ((([]) t) -> ())
796 fMT_Monad :: (FreshMonad a1) -> Monad (FMT a1 ())
798 (trace "X" (case (trace "X" (f)) of {
799 Build_FreshMonad fMT_Monad0 fMT_fresh0 -> (trace "X" (fMT_Monad0))}))
801 fMT_fresh :: (FreshMonad a1) -> (([]) a1) -> FMT a1 (SigT a1 ())
803 (trace "X" (case (trace "X" (f)) of {
804 Build_FreshMonad fMT_Monad0 fMT_fresh0 -> (trace "X" (fMT_fresh0))}))
806 mapM :: (Monad a1) -> (([]) a1) -> a1
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')))))))))))))))))))))))}))
812 treeM :: (Monad a2) -> (Tree (Prelude.Maybe a2)) -> a2
814 (trace "X" (case (trace "X" (t)) of {
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')))))))))))))))))))))))}))
823 -- singleton inductive, whose constructor was rawLatex
827 -- singleton inductive, whose constructor was rawLatexMath
831 -- singleton inductive, whose constructor was Build_ToLatex
833 toLatex :: (ToLatex a1) -> a1 -> Latex
835 (trace "X" (toLatex0))
837 latexToString :: ToString Latex
843 -- singleton inductive, whose constructor was Build_ToLatexMath
845 toLatexMath :: (ToLatexMath a1) -> a1 -> LatexMath
846 toLatexMath toLatexMath0 =
847 (trace "X" (toLatexMath0))
849 concatenableLatexMath :: Concatenable LatexMath
850 concatenableLatexMath l1 l2 =
851 (trace "X" ((trace "X" (concatenate (trace "X" (concatenableString)) (trace "X" (l1)) (trace "X" (l2))))))
853 latexMathToString :: ToString LatexMath
854 latexMathToString x =
857 toLatexMathLatex :: ToLatexMath Latex
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" ([])))))))))
861 stringToLatex :: ToLatex Prelude.String
863 (trace "X" ((trace "X" (sanitizeForLatex (trace "X" (x))))))
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)))))))))))
869 latexMathToLatexMath :: ToLatexMath LatexMath
870 latexMathToLatexMath x =
873 treeToLatexMath :: (ToLatexMath a1) -> (Tree (Prelude.Maybe a1)) -> LatexMath
874 treeToLatexMath toLatexV t =
875 (trace "X" (case (trace "X" (t)) of {
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" ([])))))))))))))))))))))))))))}))
882 data ND judgment rule =
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
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))))))}))
916 nd_id :: (Tree (Prelude.Maybe a1)) -> ND a1 a2
918 (trace "X" (case (trace "X" (sl)) of {
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)))))))))}))
925 nd_weak :: (Tree (Prelude.Maybe a1)) -> ND a1 a2
927 (trace "X" (case (trace "X" (sl)) of {
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))))))))))}))
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)
939 mkSIND :: (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (Tree (Prelude.Maybe a1)) -> (ND a1 a2) -> (SIND a1 a2) -> SIND a1 a2
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 {
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))))))
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
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))))))}))
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)))))))))))}))
1019 natToStringInstance :: ToString Nat
1020 natToStringInstance =
1021 (trace "X" (natToString))
1025 | KindArrow Kind Kind
1031 kind_rect :: a1 -> (Kind -> a1 -> Kind -> a1 -> a1) -> a1 -> a1 -> a1 -> a1 -> Kind -> a1
1032 kind_rect f f0 f1 f2 f3 f4 k =
1033 (trace "X" (case (trace "X" (k)) of {
1034 KindStar -> (trace "X" (f));
1035 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)))))))))));
1036 KindUnliftedType -> (trace "X" (f1));
1037 KindUnboxedTuple -> (trace "X" (f2));
1038 KindArgType -> (trace "X" (f3));
1039 KindOpenType -> (trace "X" (f4))}))
1041 kind_rec :: a1 -> (Kind -> a1 -> Kind -> a1 -> a1) -> a1 -> a1 -> a1 -> a1 -> Kind -> a1
1043 (trace "X" (kind_rect))
1045 kindToString :: Kind -> Prelude.String
1047 (trace "X" (case (trace "X" (k)) of {
1048 KindStar -> (trace "X" ((:) (trace "X" ('*')) (trace "X" ([]))));
1050 (trace "X" (case (trace "X" (k1)) of {
1051 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)))))))))));
1052 _ -> (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)))))))))))}));
1053 KindUnliftedType -> (trace "X" ((:) (trace "X" ('#')) (trace "X" ([]))));
1054 KindUnboxedTuple -> (trace "X" ((:) (trace "X" ('(')) (trace "X" (((:) (trace "X" ('#')) (trace "X" (((:) (trace "X" (')')) (trace "X" ([]))))))))));
1055 KindArgType -> (trace "X" ((:) (trace "X" ('?')) (trace "X" (((:) (trace "X" ('?')) (trace "X" ([])))))));
1056 KindOpenType -> (trace "X" ((:) (trace "X" ('?')) (trace "X" ([]))))}))
1058 kindToString0 :: ToString Kind
1060 (trace "X" (kindToString))
1064 (trace "X" (KindArrow (trace "X" (KindStar)) (trace "X" ((KindArrow (trace "X" (KindStar)) (trace "X" (KindStar)))))))
1066 kindToLatexMath :: Kind -> LatexMath
1068 (trace "X" (case (trace "X" (k)) of {
1069 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" ([]))))))))))))))));
1071 (trace "X" (case (trace "X" (k1)) of {
1072 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)))))))))));
1073 _ -> (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)))))))))))}));
1074 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" ([])))))))))))))))))))))))))))))))))))))))))));
1075 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" ([])))))))))))))))))))))))))))))))))))))))))))))))));
1076 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" ([])))))))))))))))))))))))))))))))))))))))))));
1077 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" ([]))))))))))))))))))))))))))))))))))))))))}))
1079 kindEqDecidable :: EqDecidable Kind
1080 kindEqDecidable v1 =
1081 (trace "X" ((trace "X" (kind_rec (trace "X" ((\v2 ->
1082 (trace "X" (case (trace "X" (v2)) of {
1083 KindStar -> (trace "X" (Prelude.True));
1084 _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v1_1 iHv1_1 v1_2 iHv1_2 v2 ->
1085 (trace "X" (case (trace "X" (v2)) of {
1086 KindArrow v2_1 v2_2 ->
1087 (trace "X" (let {s = (trace "X" ((trace "X" (iHv1_1 (trace "X" (v2_1))))))} in
1088 (trace "X" (case (trace "X" (s)) of {
1090 (trace "X" (let {s0 = (trace "X" ((trace "X" (iHv1_2 (trace "X" (v2_2))))))} in
1091 (trace "X" (case (trace "X" (s0)) of {
1092 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))))));
1093 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))))))}))));
1095 (trace "X" (let {s0 = (trace "X" ((trace "X" (iHv1_2 (trace "X" (v2_2))))))} in
1096 (trace "X" (case (trace "X" (s0)) of {
1097 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))))));
1098 Prelude.False -> (trace "X" (Prelude.False))}))))}))));
1099 _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v2 ->
1100 (trace "X" (case (trace "X" (v2)) of {
1101 KindUnliftedType -> (trace "X" (Prelude.True));
1102 _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v2 ->
1103 (trace "X" (case (trace "X" (v2)) of {
1104 KindUnboxedTuple -> (trace "X" (Prelude.True));
1105 _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v2 ->
1106 (trace "X" (case (trace "X" (v2)) of {
1107 KindArgType -> (trace "X" (Prelude.True));
1108 _ -> (trace "X" (Prelude.False))}))))) (trace "X" ((\v2 ->
1109 (trace "X" (case (trace "X" (v2)) of {
1110 KindOpenType -> (trace "X" (Prelude.True));
1111 _ -> (trace "X" (Prelude.False))}))))) (trace "X" (v1))))))
1113 tyConToString :: ToString TyCon.TyCon
1115 (trace "X" (outputableToString))
1117 tyFunToString :: ToString TyCon.TyCon
1119 (trace "X" (outputableToString))
1121 arrowTyCon :: TyCon.TyCon
1122 arrowTyCon = Type.funTyCon
1124 haskLiteralToString :: ToString Literal.Literal
1125 haskLiteralToString =
1126 (trace "X" (outputableToString))
1128 haskLiteralToTyCon :: Literal.Literal -> TyCon.TyCon
1129 haskLiteralToTyCon lit =
1130 (trace "X" (case (trace "X" (lit)) of {
1131 Literal.MachChar h -> (trace "X" (TysPrim.charPrimTyCon));
1132 Literal.MachInt h -> (trace "X" (TysPrim.intPrimTyCon));
1133 Literal.MachInt64 h -> (trace "X" (TysPrim.int64PrimTyCon));
1134 Literal.MachWord h -> (trace "X" (TysPrim.wordPrimTyCon));
1135 Literal.MachWord64 h -> (trace "X" (TysPrim.word64PrimTyCon));
1136 Literal.MachFloat h -> (trace "X" (TysPrim.floatPrimTyCon));
1137 Literal.MachDouble h -> (trace "X" (TysPrim.doublePrimTyCon));
1138 _ -> (trace "X" (TysPrim.addrPrimTyCon))}))
1140 coreVarEqDecidable :: EqDecidable Var.Var
1141 coreVarEqDecidable =
1144 coreVarToString :: ToString Var.Var
1146 (trace "X" (outputableToString))
1148 tyConEqDecidable :: EqDecidable TyCon.TyCon
1152 tyFunEqDecidable :: EqDecidable TyCon.TyCon
1156 coreTypeToString :: ToString TypeRep.Type
1158 (trace "X" ((outputableToString . coreViewDeep)))
1160 coreDataConToString :: ToString DataCon.DataCon
1161 coreDataConToString =
1162 (trace "X" (outputableToString))
1164 coreExprToString :: ToString (CoreSyn.Expr Var.Var)
1166 (trace "X" (outputableToString))
1169 WeakTypeVar Var.Var Kind
1172 WTyVarTy WeakTypeVar0
1173 | WAppTy WeakType WeakType
1174 | WTyFunApp TyCon.TyCon (([]) WeakType)
1175 | WTyCon TyCon.TyCon
1177 | WCodeTy WeakTypeVar0 WeakType
1178 | WCoFunTy WeakType WeakType WeakType
1179 | WForAllTy WeakTypeVar0 WeakType
1180 | WClassP Class.Class (([]) WeakType)
1181 | WIParam (BasicTypes.IPName Name.Name) WeakType
1183 weakTypeVarEqDecidable :: EqDecidable WeakTypeVar0
1184 weakTypeVarEqDecidable v1 v2 =
1185 (trace "X" (case (trace "X" (v1)) of {
1186 WeakTypeVar cv1 k1 ->
1187 (trace "X" (case (trace "X" (v2)) of {
1188 WeakTypeVar cv2 k2 ->
1189 (trace "X" (let {s = (trace "X" ((trace "X" (eqd_dec (trace "X" (coreVarEqDecidable)) (trace "X" (cv1)) (trace "X" (cv2))))))} in
1190 (trace "X" (case (trace "X" (s)) of {
1192 (trace "X" ((trace "X" (eq_rec_r (trace "X" (cv2))
1193 (trace "X" ((let {s0 = (trace "X" ((trace "X" (eqd_dec (trace "X" (kindEqDecidable)) (trace "X" (k1)) (trace "X" (k2))))))} in
1194 (trace "X" (case (trace "X" (s0)) of {
1195 Prelude.True -> (trace "X" ((trace "X" (eq_rec_r (trace "X" (k2)) (trace "X" (Prelude.True)) (trace "X" (k1))))));
1196 Prelude.False -> (trace "X" (Prelude.False))}))))) (trace "X" (cv1))))));
1197 Prelude.False -> (trace "X" (Prelude.False))}))))}))}))
1200 WeakCoerVar Var.Var WeakType WeakType
1205 | WCoApp WeakCoercion WeakCoercion
1206 | WCoAppT WeakCoercion WeakType
1207 | WCoAll Kind (WeakTypeVar0 -> WeakCoercion)
1208 | WCoSym WeakCoercion
1209 | WCoComp WeakCoercion WeakCoercion
1210 | WCoLeft WeakCoercion
1211 | WCoRight WeakCoercion
1212 | WCoUnsafe WeakType WeakType
1214 weakCoercionTypes :: WeakCoercion -> (,) WeakType WeakType
1215 weakCoercionTypes wc =
1216 (trace "X" (case (trace "X" (wc)) of {
1217 WCoSym c -> (trace "X" (case (trace "X" ((trace "X" (weakCoercionTypes (trace "X" (c)))))) of {
1218 (,) t2 t1 -> (trace "X" ((,) (trace "X" (t1)) (trace "X" (t2))))}));
1219 WCoUnsafe t1 t2 -> (trace "X" ((,) (trace "X" (t1)) (trace "X" (t2))));
1220 _ -> (trace "X" ((,) (trace "X" (WFunTyCon)) (trace "X" (WFunTyCon))))}))
1222 weakTypeToString :: ToString WeakType
1224 (trace "X" ((coreTypeToString . weakTypeToCoreType)))
1227 WeakExprVar Var.Var WeakType
1230 WExprVar WeakExprVar0
1231 | WTypeVar WeakTypeVar0
1232 | WCoerVar WeakCoerVar0
1234 weakTypeVarToKind :: WeakTypeVar0 -> Kind
1235 weakTypeVarToKind tv =
1236 (trace "X" (case (trace "X" (tv)) of {
1237 WeakTypeVar c k -> (trace "X" (k))}))
1239 weakVarToCoreVar :: WeakVar -> Var.Var
1240 weakVarToCoreVar wv =
1241 (trace "X" (case (trace "X" (wv)) of {
1242 WExprVar w -> (trace "X" (case (trace "X" (w)) of {
1243 WeakExprVar v w0 -> (trace "X" (v))}));
1244 WTypeVar w -> (trace "X" (case (trace "X" (w)) of {
1245 WeakTypeVar v k -> (trace "X" (v))}));
1246 WCoerVar w -> (trace "X" (case (trace "X" (w)) of {
1247 WeakCoerVar v w0 w1 -> (trace "X" (v))}))}))
1249 tyConTyVars :: TyCon.TyCon -> ([]) WeakTypeVar0
1251 (trace "X" ((trace "X" (filter
1252 (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1253 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (x)))))) of {
1254 WTypeVar v -> (trace "X" (Prelude.Just (trace "X" (v))));
1255 _ -> (trace "X" (Prelude.Nothing))}))))) (trace "X" ((trace "X" ((getTyConTyVars (trace "X" (tc))))))))))))))))
1257 tyConKind :: TyCon.TyCon -> ([]) Kind
1259 (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))))))))))))))))
1261 tyFunKind :: TyCon.TyCon -> (,) (([]) Kind) Kind
1263 (trace "X" ((trace "X" (rawTyFunKind (trace "X" ((trace "X" (((\x -> x) (trace "X" (tc)))))))))))
1266 WeakDataAlt DataCon.DataCon
1267 | WeakLitAlt Literal.Literal
1272 | WELit Literal.Literal
1273 | WELet WeakExprVar0 WeakExpr WeakExpr
1274 | WELetRec (Tree (Prelude.Maybe ((,) WeakExprVar0 WeakExpr))) WeakExpr
1275 | WECast WeakExpr WeakCoercion
1276 | WENote CoreSyn.Note WeakExpr
1277 | WEApp WeakExpr WeakExpr
1278 | WETyApp WeakExpr WeakType
1279 | WECoApp WeakExpr WeakCoercion
1280 | WELam WeakExprVar0 WeakExpr
1281 | WETyLam WeakTypeVar0 WeakExpr
1282 | WECoLam WeakCoerVar0 WeakExpr
1283 | WEBrak WeakExprVar0 WeakTypeVar0 WeakExpr WeakType
1284 | WEEsc WeakExprVar0 WeakTypeVar0 WeakExpr WeakType
1285 | WECSP WeakExprVar0 WeakTypeVar0 WeakExpr WeakType
1286 | WECase WeakExprVar0 WeakExpr WeakType TyCon.TyCon (([]) WeakType) (Tree (Prelude.Maybe ((,) ((,) ((,) ((,) WeakAltCon (([]) WeakTypeVar0)) (([]) WeakCoerVar0)) (([]) WeakExprVar0)) WeakExpr)))
1288 mkTyFunApplication :: TyCon.TyCon -> (([]) WeakType) -> OrError WeakType
1289 mkTyFunApplication tf lwt =
1290 (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 {
1291 (,) 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))))))))))))})))))))))
1293 coreTypeToWeakType' :: TypeRep.Type -> OrError WeakType
1294 coreTypeToWeakType' ct =
1295 (trace "X" (case (trace "X" (ct)) of {
1296 TypeRep.TyVarTy cv ->
1297 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (cv)))))) of {
1298 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1299 WTypeVar tv -> (trace "X" (OK (trace "X" ((WTyVarTy (trace "X" (tv)))))));
1300 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1301 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')))))))))))))))))))));
1302 TypeRep.TyConApp tc_ lct ->
1304 recurse = (trace "X" ((trace "X" (let {
1306 (trace "X" (case (trace "X" (tl)) of {
1307 ([]) -> (trace "X" (OK (trace "X" (([])))));
1308 (:) 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')))))))))))))))))))))}))}
1309 in rec (trace "X" (lct))))))}
1311 (trace "X" (case (trace "X" ((trace "X" (tyConOrTyFun (trace "X" (tc_)))))) of {
1313 (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (tyConEqDecidable)) (trace "X" (tc)) (trace "X" (TysWiredIn.hetMetCodeTypeTyCon)))))) of {
1315 (trace "X" (case (trace "X" (lct)) of {
1316 ([]) -> (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))))))))))))));
1318 (trace "X" (case (trace "X" (c)) of {
1319 TypeRep.TyVarTy ec ->
1320 (trace "X" (case (trace "X" (l)) of {
1321 ([]) -> (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))))))))))))));
1323 (trace "X" (case (trace "X" (l0)) of {
1325 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (ec)))))) of {
1326 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1327 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'))))))))))))));
1328 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1329 (:) 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))))))))))))))}))}));
1330 _ -> (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))))))))))))))}))}));
1333 tc' = (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (tyConEqDecidable)) (trace "X" (tc)) (trace "X" (arrowTyCon)))))) of {
1334 Prelude.True -> (trace "X" (WFunTyCon));
1335 Prelude.False -> (trace "X" (WTyCon (trace "X" (tc))))}))}
1337 (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'))))))))))))))))))}));
1338 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')))))))))))))}))));
1339 TypeRep.FunTy t1 t2 ->
1340 (trace "X" (case (trace "X" (t1)) of {
1342 (trace "X" (case (trace "X" (p)) of {
1343 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'))))))))))))))))))))))))))));
1344 _ -> (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')))))))))))))))))))))}));
1345 _ -> (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')))))))))))))))))))))}));
1346 TypeRep.ForAllTy cv t ->
1347 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (cv)))))) of {
1348 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1349 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'))))))))))))));
1350 WCoerVar w -> (trace "X" (case (trace "X" (w)) of {
1351 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'))))))))))))))}))}));
1353 (trace "X" (case (trace "X" (p)) of {
1354 TypeRep.ClassP cl lct ->
1355 (trace "X" ((trace "X" (orErrorBind
1356 (trace "X" ((trace "X" ((let {
1358 (trace "X" (case (trace "X" (tl)) of {
1359 ([]) -> (trace "X" (OK (trace "X" (([])))));
1360 (:) 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')))))))))))))))))))))}))}
1361 in rec (trace "X" (lct))))))) (trace "X" ((\lct' -> (trace "X" (OK (trace "X" ((WClassP (trace "X" (cl)) (trace "X" (lct'))))))))))))));
1362 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'))))))))))))));
1363 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))}))}))
1365 coreTypeToWeakType :: TypeRep.Type -> OrError WeakType
1366 coreTypeToWeakType t =
1367 (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))))))))))))))))
1369 isBrak :: (CoreSyn.Expr Var.Var) -> Prelude.Maybe ((,) ((,) WeakExprVar0 WeakTypeVar0) TypeRep.Type)
1371 (trace "X" (case (trace "X" (ce)) of {
1373 (trace "X" (case (trace "X" (c)) of {
1374 CoreSyn.App c1 c2 ->
1375 (trace "X" (case (trace "X" (c1)) of {
1377 (trace "X" (case (trace "X" (c2)) of {
1379 (trace "X" (case (trace "X" (c3)) of {
1380 TypeRep.TyVarTy ec ->
1381 (trace "X" (case (trace "X" (c0)) of {
1382 CoreSyn.Type tbody ->
1383 (trace "X" (case (trace "X" ((trace "X" ((==) (trace "X" (PrelNames.hetmet_brak_name)) (trace "X" ((trace "X" ((Var.varName (trace "X" (v))))))))))) of {
1385 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (ec)))))) of {
1387 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (v)))))) of {
1388 WExprVar v' -> (trace "X" (Prelude.Just (trace "X" (((,) (trace "X" (((,) (trace "X" (v')) (trace "X" (tv))))) (trace "X" (tbody)))))));
1389 _ -> (trace "X" (Prelude.Nothing))}));
1390 _ -> (trace "X" (Prelude.Nothing))}));
1391 Prelude.False -> (trace "X" (Prelude.Nothing))}));
1392 _ -> (trace "X" (Prelude.Nothing))}));
1393 _ -> (trace "X" (Prelude.Nothing))}));
1394 _ -> (trace "X" (Prelude.Nothing))}));
1395 _ -> (trace "X" (Prelude.Nothing))}));
1396 _ -> (trace "X" (Prelude.Nothing))}));
1397 _ -> (trace "X" (Prelude.Nothing))}))
1399 isEsc :: (CoreSyn.Expr Var.Var) -> Prelude.Maybe ((,) ((,) WeakExprVar0 WeakTypeVar0) TypeRep.Type)
1401 (trace "X" (case (trace "X" (ce)) of {
1403 (trace "X" (case (trace "X" (c)) of {
1404 CoreSyn.App c1 c2 ->
1405 (trace "X" (case (trace "X" (c1)) of {
1407 (trace "X" (case (trace "X" (c2)) of {
1409 (trace "X" (case (trace "X" (c3)) of {
1410 TypeRep.TyVarTy ec ->
1411 (trace "X" (case (trace "X" (c0)) of {
1412 CoreSyn.Type tbody ->
1413 (trace "X" (case (trace "X" ((trace "X" ((==) (trace "X" (PrelNames.hetmet_esc_name)) (trace "X" ((trace "X" ((Var.varName (trace "X" (v))))))))))) of {
1415 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (ec)))))) of {
1417 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (v)))))) of {
1418 WExprVar v' -> (trace "X" (Prelude.Just (trace "X" (((,) (trace "X" (((,) (trace "X" (v')) (trace "X" (tv))))) (trace "X" (tbody)))))));
1419 _ -> (trace "X" (Prelude.Nothing))}));
1420 _ -> (trace "X" (Prelude.Nothing))}));
1421 Prelude.False -> (trace "X" (Prelude.Nothing))}));
1422 _ -> (trace "X" (Prelude.Nothing))}));
1423 _ -> (trace "X" (Prelude.Nothing))}));
1424 _ -> (trace "X" (Prelude.Nothing))}));
1425 _ -> (trace "X" (Prelude.Nothing))}));
1426 _ -> (trace "X" (Prelude.Nothing))}));
1427 _ -> (trace "X" (Prelude.Nothing))}))
1429 isCSP :: (CoreSyn.Expr Var.Var) -> Prelude.Maybe ((,) ((,) WeakExprVar0 WeakTypeVar0) TypeRep.Type)
1431 (trace "X" (case (trace "X" (ce)) of {
1433 (trace "X" (case (trace "X" (c)) of {
1434 CoreSyn.App c1 c2 ->
1435 (trace "X" (case (trace "X" (c1)) of {
1437 (trace "X" (case (trace "X" (c2)) of {
1439 (trace "X" (case (trace "X" (c3)) of {
1440 TypeRep.TyVarTy ec ->
1441 (trace "X" (case (trace "X" (c0)) of {
1442 CoreSyn.Type tbody ->
1443 (trace "X" (case (trace "X" ((trace "X" ((==) (trace "X" (PrelNames.hetmet_csp_name)) (trace "X" ((trace "X" ((Var.varName (trace "X" (v))))))))))) of {
1445 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (ec)))))) of {
1447 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (v)))))) of {
1448 WExprVar v' -> (trace "X" (Prelude.Just (trace "X" (((,) (trace "X" (((,) (trace "X" (v')) (trace "X" (tv))))) (trace "X" (tbody)))))));
1449 _ -> (trace "X" (Prelude.Nothing))}));
1450 _ -> (trace "X" (Prelude.Nothing))}));
1451 Prelude.False -> (trace "X" (Prelude.Nothing))}));
1452 _ -> (trace "X" (Prelude.Nothing))}));
1453 _ -> (trace "X" (Prelude.Nothing))}));
1454 _ -> (trace "X" (Prelude.Nothing))}));
1455 _ -> (trace "X" (Prelude.Nothing))}));
1456 _ -> (trace "X" (Prelude.Nothing))}));
1457 _ -> (trace "X" (Prelude.Nothing))}))
1459 expectTyConApp :: WeakType -> (([]) WeakType) -> OrError ((,) TyCon.TyCon (([]) WeakType))
1460 expectTyConApp wt acc =
1461 (trace "X" (case (trace "X" (wt)) of {
1462 WAppTy t1 t2 -> (trace "X" ((trace "X" (expectTyConApp (trace "X" (t1)) (trace "X" (((:) (trace "X" (t2)) (trace "X" (acc)))))))));
1463 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))))))))))))));
1464 WTyCon tc -> (trace "X" (OK (trace "X" (((,) (trace "X" (tc)) (trace "X" (acc)))))));
1465 _ -> (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))))))))))))))}))
1467 coreExprToWeakExpr :: (CoreSyn.Expr Var.Var) -> OrError WeakExpr
1468 coreExprToWeakExpr ce =
1469 (trace "X" (case (trace "X" (ce)) of {
1471 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (v)))))) of {
1472 WExprVar ev -> (trace "X" (OK (trace "X" ((WEVar (trace "X" (ev)))))));
1473 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1474 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1475 CoreSyn.Lit lit -> (trace "X" (OK (trace "X" ((WELit (trace "X" (lit)))))));
1476 CoreSyn.App e1 e2 ->
1477 (trace "X" (case (trace "X" ((trace "X" (isBrak (trace "X" (e1)))))) of {
1479 (trace "X" (case (trace "X" (p)) of {
1480 (,) p0 t -> (trace "X" (case (trace "X" (p0)) of {
1481 (,) 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')))))))))))))))))))))}))}));
1483 (trace "X" (case (trace "X" ((trace "X" (isEsc (trace "X" (e1)))))) of {
1485 (trace "X" (case (trace "X" (p)) of {
1486 (,) p0 t -> (trace "X" (case (trace "X" (p0)) of {
1487 (,) 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')))))))))))))))))))))}))}));
1489 (trace "X" (case (trace "X" ((trace "X" (isCSP (trace "X" (e1)))))) of {
1491 (trace "X" (case (trace "X" (p)) of {
1492 (,) p0 t -> (trace "X" (case (trace "X" (p0)) of {
1493 (,) 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')))))))))))))))))))))}))}));
1495 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e1))))))) (trace "X" ((\e1' ->
1496 (trace "X" (case (trace "X" (e2)) of {
1497 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'))))))))))))));
1498 _ -> (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'))))))))))))))})))))))))}))}))}));
1500 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (v)))))) of {
1501 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'))))))))))))));
1502 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'))))))))))))));
1503 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'))))))))))))))}));
1505 (trace "X" (case (trace "X" (c)) of {
1506 CoreSyn.NonRec v ve ->
1507 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (v)))))) of {
1508 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')))))))))))))))))))));
1510 (trace "X" (case (trace "X" (e)) of {
1511 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" ([]))))))))))))))))))))))))))))))))))))))))))))));
1512 _ -> (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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1513 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1515 (trace "X" ((trace "X" (orErrorBind
1516 (trace "X" ((trace "X" ((let {
1517 coreExprToWeakExprList cel =
1518 (trace "X" (case (trace "X" (cel)) of {
1519 ([]) -> (trace "X" (OK (trace "X" (([])))));
1521 (trace "X" (case (trace "X" (p)) of {
1523 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExprList (trace "X" (t))))))) (trace "X" ((\t' ->
1524 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (v')))))) of {
1525 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'))))))))))))));
1526 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" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1527 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" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))})))))))))}))}))}
1528 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')))))))))))))))))))))}));
1529 CoreSyn.Case e v tbranches alts ->
1530 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (v)))))) of {
1532 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreTypeToWeakType (trace "X" ((trace "X" ((CoreUtils.exprType (trace "X" (e)))))))))))) (trace "X" ((\te' ->
1533 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((expectTyConApp (trace "X" (te')) (trace "X" (([])))))))) (trace "X" ((\tca ->
1534 (trace "X" (case (trace "X" (tca)) of {
1536 (trace "X" ((trace "X" (orErrorBind
1537 (trace "X" ((trace "X" ((let {
1538 mkBranches branches =
1539 (trace "X" (case (trace "X" (branches)) of {
1540 ([]) -> (trace "X" (OK (trace "X" (([])))));
1542 (trace "X" (case (trace "X" (t)) of {
1544 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((mkBranches (trace "X" (rest))))))) (trace "X" ((\rest' ->
1545 (trace "X" ((trace "X" (orErrorBind (trace "X" ((trace "X" ((coreExprToWeakExpr (trace "X" (e0))))))) (trace "X" ((\e' ->
1546 (trace "X" (case (trace "X" (alt)) of {
1547 CoreSyn.DataAlt dc ->
1548 (trace "X" (let {vars0 = (trace "X" ((trace "X" (map (trace "X" (coreVarToWeakVar)) (trace "X" (vars))))))} in
1549 (trace "X" (OK (trace "X" (((:) (trace "X" (((,) (trace "X" (((,) (trace "X" (((,) (trace "X" (((,) (trace "X" ((WeakDataAlt (trace "X" (dc)))))
1550 (trace "X" ((trace "X" ((filter
1551 (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1552 (trace "X" (case (trace "X" (x)) of {
1553 WTypeVar v0 -> (trace "X" (Prelude.Just (trace "X" (v0))));
1554 _ -> (trace "X" (Prelude.Nothing))}))))) (trace "X" (vars0)))))))))))))))
1555 (trace "X" ((trace "X" ((filter
1556 (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1557 (trace "X" (case (trace "X" (x)) of {
1558 WCoerVar v0 -> (trace "X" (Prelude.Just (trace "X" (v0))));
1559 _ -> (trace "X" (Prelude.Nothing))}))))) (trace "X" (vars0)))))))))))))))
1560 (trace "X" ((trace "X" ((filter
1561 (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1562 (trace "X" (case (trace "X" (x)) of {
1563 WExprVar v0 -> (trace "X" (Prelude.Just (trace "X" (v0))));
1564 _ -> (trace "X" (Prelude.Nothing))}))))) (trace "X" (vars0))))))))))))))) (trace "X" (e'))))) (trace "X" (rest')))))))));
1565 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')))))));
1566 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')))))))}))))))))))))))))}))}))}
1567 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)))))))))))))))))))))))))))))))))}))))))))))))))));
1568 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))));
1569 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" ([])))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}));
1570 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)))))))))))))))))));
1571 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'))))))))))))));
1572 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" ([]))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))}))
1574 dataConExTyVars :: DataCon.DataCon -> ([]) WeakTypeVar0
1575 dataConExTyVars cdc =
1576 (trace "X" ((trace "X" (filter
1577 (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1578 (trace "X" (case (trace "X" ((trace "X" (coreVarToWeakVar (trace "X" (x)))))) of {
1579 WTypeVar v -> (trace "X" (Prelude.Just (trace "X" (v))));
1580 _ -> (trace "X" (Prelude.Nothing))}))))) (trace "X" ((trace "X" ((DataCon.dataConExTyVars (trace "X" (cdc))))))))))))))))
1582 dataConCoerKinds :: DataCon.DataCon -> ([]) ((,) WeakType WeakType)
1583 dataConCoerKinds cdc =
1584 (trace "X" ((trace "X" (filter
1585 (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1586 (trace "X" (case (trace "X" (x)) of {
1587 TypeRep.EqPred t1 t2 ->
1588 (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 {
1589 Error error_message -> (trace "X" (Prelude.Nothing));
1590 OK z -> (trace "X" (Prelude.Just (trace "X" (z))))}));
1591 _ -> (trace "X" (Prelude.Nothing))}))))) (trace "X" ((trace "X" ((DataCon.dataConEqTheta (trace "X" (cdc))))))))))))))))
1593 dataConFieldTypes :: DataCon.DataCon -> ([]) WeakType
1594 dataConFieldTypes cdc =
1595 (trace "X" ((trace "X" (filter
1596 (trace "X" ((trace "X" ((map (trace "X" ((\x ->
1597 (trace "X" (case (trace "X" ((trace "X" (coreTypeToWeakType (trace "X" (x)))))) of {
1598 Error error_message -> (trace "X" (Prelude.Nothing));
1599 OK z -> (trace "X" (Prelude.Just (trace "X" (z))))}))))) (trace "X" ((trace "X" ((DataCon.dataConOrigArgTys (trace "X" (cdc))))))))))))))))
1603 -- singleton inductive, whose constructor was mkDataCon
1605 dataConToCoreDataCon :: TyCon.TyCon -> DataCon -> DataCon.DataCon
1606 dataConToCoreDataCon tc dc =
1609 tyConKind' :: TyCon.TyCon -> Kind
1611 (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)))))))))))
1613 data RawHaskType tV =
1617 | TCoerc Kind (RawHaskType tV) (RawHaskType tV) (RawHaskType tV)
1618 | TApp Kind Kind (RawHaskType tV) (RawHaskType tV)
1619 | TAll Kind (tV -> RawHaskType tV)
1620 | TCode (RawHaskType tV) (RawHaskType tV)
1621 | TyFunApp TyCon.TyCon (([]) Kind) Kind (RawHaskTypeList tV)
1622 data RawHaskTypeList tV =
1624 | TyFunApp_cons Kind (([]) Kind) (RawHaskType tV) (RawHaskTypeList tV)
1626 data RawCoercionKind tV =
1627 MkRawCoercionKind Kind (RawHaskType tV) (RawHaskType tV)
1629 type TypeEnv = ([]) Kind
1631 type InstantiatedTypeEnv tV = IList Kind tV
1633 type HaskCoercionKind = () -> (InstantiatedTypeEnv ()) -> RawCoercionKind ()
1635 type CoercionEnv = ([]) HaskCoercionKind
1637 type InstantiatedCoercionEnv tV cV = Vec cV
1639 type HaskTyVar = () -> (InstantiatedTypeEnv ()) -> ()
1641 type HaskCoVar = () -> () -> (InstantiatedTypeEnv ()) -> (InstantiatedCoercionEnv () ()) -> ()
1643 type HaskLevel = ([]) HaskTyVar
1645 type HaskType = () -> (InstantiatedTypeEnv ()) -> RawHaskType ()
1647 haskTyVarToType :: TypeEnv -> Kind -> HaskTyVar -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1648 haskTyVarToType __U0393_0 __U03ba_ htv ite =
1649 (trace "X" (TVar (trace "X" (__U03ba_)) (trace "X" ((trace "X" ((unsafeCoerce (trace "X" (htv)) (trace "X" (__)) (trace "X" (ite)))))))))
1651 data HaskTypeOfSomeKind0 =
1652 HaskTypeOfSomeKind Kind HaskType
1654 data LeveledHaskType =
1655 MkLeveledHaskType HaskType HaskLevel
1657 freshHaskTyVar :: (([]) Kind) -> Kind -> (InstantiatedTypeEnv a1) -> a1
1658 freshHaskTyVar __U0393_0 __U03ba_ env =
1659 (trace "X" ((trace "X" (ilist_head (trace "X" (__U03ba_)) (trace "X" (__U0393_0)) (trace "X" (env))))))
1661 haskTAll :: TypeEnv -> Kind -> (() -> (InstantiatedTypeEnv ()) -> () -> RawHaskType ()) -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1662 haskTAll __U0393_0 __U03ba_ __U03c3_ env =
1663 (trace "X" (TAll (trace "X" (__U03ba_)) (trace "X" ((trace "X" ((unsafeCoerce (trace "X" (__U03c3_)) (trace "X" (__)) (trace "X" (env)))))))))
1665 haskTApp :: TypeEnv -> Kind -> (() -> (InstantiatedTypeEnv ()) -> () -> RawHaskType ()) -> HaskTyVar -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1666 haskTApp __U0393_0 __U03ba_ __U03c3_ cv env =
1667 (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)))))))))))
1669 haskBrak :: TypeEnv -> HaskTyVar -> HaskType -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1670 haskBrak __U0393_0 v t env =
1671 (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)))))))))
1673 mkHaskCoercionKind :: TypeEnv -> Kind -> HaskType -> HaskType -> (InstantiatedTypeEnv a1) -> RawCoercionKind a1
1674 mkHaskCoercionKind __U0393_0 __U03ba_ t1 t2 ite =
1675 (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)))))))))
1677 flattenT :: Kind -> (RawHaskType (RawHaskType a1)) -> RawHaskType a1
1680 flattenT0 __U03ba_ exp =
1681 (trace "X" (case (trace "X" (exp)) of {
1682 TVar __U03ba_0 x -> (trace "X" (x));
1683 TCon tc -> (trace "X" (TCon (trace "X" (tc))));
1684 TArrow -> (trace "X" (TArrow));
1685 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)))))))));
1686 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)))))))));
1687 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)))))))))))))))))));
1688 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)))))))));
1689 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)))))))))}));
1690 flattenTyFunApp lk exp =
1691 (trace "X" (case (trace "X" (exp)) of {
1692 TyFunApp_nil -> (trace "X" (TyFunApp_nil));
1693 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)))))))))}))}
1696 substT :: TypeEnv -> Kind -> Kind -> (() -> (InstantiatedTypeEnv ()) -> () -> RawHaskType ()) -> HaskType -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1697 substT __U0393_0 __U03ba___U2081_ __U03ba___U2082_ exp v env =
1698 (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))))))))))))))))
1700 unlev :: TypeEnv -> Kind -> LeveledHaskType -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1701 unlev __U0393_0 __U03ba_ lht x =
1702 (trace "X" (case (trace "X" (lht)) of {
1703 MkLeveledHaskType t l -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (t)) (trace "X" (__)) (trace "X" (x))))))}))
1706 Build_Global WeakExprVar0 (([]) Kind) ((IList Kind HaskType) -> HaskType)
1708 glob_wv :: TypeEnv -> Global -> WeakExprVar0
1709 glob_wv __U0393_0 g =
1710 (trace "X" (case (trace "X" (g)) of {
1711 Build_Global glob_wv0 glob_kinds0 glob_tf0 -> (trace "X" (glob_wv0))}))
1713 glob_kinds :: TypeEnv -> Global -> ([]) Kind
1714 glob_kinds __U0393_0 g =
1715 (trace "X" (case (trace "X" (g)) of {
1716 Build_Global glob_wv0 glob_kinds0 glob_tf0 -> (trace "X" (glob_kinds0))}))
1718 glob_tf :: TypeEnv -> Global -> (IList Kind HaskType) -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1719 glob_tf __U0393_0 g x x0 =
1720 (trace "X" (case (trace "X" (g)) of {
1721 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))))))}))
1723 take_arg_types :: Kind -> (RawHaskType a1) -> ([]) (RawHaskType a1)
1724 take_arg_types __U03ba_ exp =
1725 (trace "X" (case (trace "X" (exp)) of {
1726 TApp __U03ba___U2081_ __U03ba___U2082_ x y ->
1727 (trace "X" (let {x0 = (trace "X" ((trace "X" (take_arg_types (trace "X" (__U03ba___U2082_)) (trace "X" (y))))))} in
1728 (trace "X" (case (trace "X" (__U03ba___U2081_)) of {
1730 (trace "X" (case (trace "X" (__U03ba___U2082_)) of {
1732 (trace "X" (case (trace "X" (x)) of {
1733 TApp __U03ba___U2081_'' __U03ba___U2082_'' w'' x'' ->
1734 (trace "X" (case (trace "X" (__U03ba___U2082_'')) of {
1736 (trace "X" (case (trace "X" (w'')) of {
1737 TArrow -> (trace "X" ((:) (trace "X" (x'')) (trace "X" (x0))));
1738 _ -> (trace "X" (([])))}));
1739 _ -> (trace "X" (([])))}));
1740 _ -> (trace "X" (([])))}));
1741 _ -> (trace "X" (([])))}));
1742 _ -> (trace "X" (([])))}))));
1743 _ -> (trace "X" (([])))}))
1745 count_arg_types :: Kind -> (RawHaskType a1) -> Nat
1746 count_arg_types __U03ba_ exp =
1747 (trace "X" (case (trace "X" (exp)) of {
1748 TApp __U03ba___U2081_ __U03ba___U2082_ x y ->
1749 (trace "X" (let {x0 = (trace "X" ((trace "X" (count_arg_types (trace "X" (__U03ba___U2082_)) (trace "X" (y))))))} in
1750 (trace "X" (case (trace "X" (__U03ba___U2081_)) of {
1752 (trace "X" (case (trace "X" (__U03ba___U2082_)) of {
1754 (trace "X" (case (trace "X" (x)) of {
1755 TApp __U03ba___U2081_'' __U03ba___U2082_'' w'' x'' ->
1756 (trace "X" (case (trace "X" (__U03ba___U2082_'')) of {
1758 (trace "X" (case (trace "X" (w'')) of {
1759 TArrow -> (trace "X" (S (trace "X" (x0))));
1760 _ -> (trace "X" (O))}));
1761 _ -> (trace "X" (O))}));
1762 _ -> (trace "X" (O))}));
1763 _ -> (trace "X" (O))}));
1764 _ -> (trace "X" (O))}))));
1765 _ -> (trace "X" (O))}))
1767 ite_unit :: TypeEnv -> InstantiatedTypeEnv ()
1768 ite_unit __U0393_0 =
1769 (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))))))
1771 drop_arg_types :: Kind -> (RawHaskType a1) -> RawHaskType a1
1772 drop_arg_types __U03ba_ exp =
1773 (trace "X" (case (trace "X" (exp)) of {
1774 TCon tc -> (trace "X" (TCon (trace "X" (tc))));
1775 TArrow -> (trace "X" (TArrow));
1776 TApp __U03ba___U2081_ __U03ba___U2082_ x y ->
1778 q = (trace "X" (let {x0 = (trace "X" ((trace "X" (drop_arg_types (trace "X" (__U03ba___U2082_)) (trace "X" (y))))))} in
1779 (trace "X" (case (trace "X" (__U03ba___U2081_)) of {
1781 (trace "X" (case (trace "X" (__U03ba___U2082_)) of {
1783 (trace "X" (case (trace "X" (x)) of {
1784 TVar __U03ba_0 y0 -> (trace "X" (Prelude.Nothing));
1785 TCon tc -> (trace "X" (Prelude.Nothing));
1786 TArrow -> (trace "X" (Prelude.Nothing));
1787 TCoerc __U03ba_0 r r0 r1 -> (trace "X" (Prelude.Nothing));
1788 TApp __U03ba___U2081_'' __U03ba___U2082_'' w'' x'' ->
1789 (trace "X" (case (trace "X" (__U03ba___U2082_'')) of {
1791 (trace "X" (case (trace "X" (w'')) of {
1792 TVar __U03ba_0 y0 -> (trace "X" (Prelude.Nothing));
1793 TCon tc -> (trace "X" (Prelude.Nothing));
1794 TArrow -> (trace "X" (Prelude.Just (trace "X" (x0))));
1795 _ -> (trace "X" (Prelude.Nothing))}));
1796 _ -> (trace "X" (Prelude.Nothing))}));
1797 _ -> (trace "X" (Prelude.Nothing))}));
1798 _ -> (trace "X" (Prelude.Nothing))}));
1799 _ -> (trace "X" (Prelude.Nothing))}))))}
1801 (trace "X" (case (trace "X" (q)) of {
1802 Prelude.Just y0 -> (trace "X" (y0));
1803 Prelude.Nothing -> (trace "X" (TApp (trace "X" (__U03ba___U2081_)) (trace "X" (__U03ba___U2082_)) (trace "X" (x)) (trace "X" (y))))}))));
1804 x -> (trace "X" (x))}))
1806 weakITE :: TypeEnv -> Kind -> (InstantiatedTypeEnv a1) -> InstantiatedTypeEnv a1
1807 weakITE __U0393_0 __U03ba_ ite =
1808 (trace "X" ((trace "X" (ilist_tail (trace "X" (__U03ba_)) (trace "X" (__U0393_0)) (trace "X" (ite))))))
1810 weakCE :: TypeEnv -> Kind -> CoercionEnv -> CoercionEnv
1811 weakCE __U0393_0 __U03ba_ __U0394_0 =
1812 (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))))))
1814 weakV :: TypeEnv -> Kind -> Kind -> HaskTyVar -> (InstantiatedTypeEnv a1) -> a1
1815 weakV __U0393_0 __U03ba_ __U03ba_v cv' ite =
1816 (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)))))))))))
1818 weakV' :: TypeEnv -> (([]) Kind) -> Kind -> HaskTyVar -> (InstantiatedTypeEnv a1) -> a1
1819 weakV' __U0393_0 __U03ba_ __U03ba_v cv' env =
1820 (trace "X" ((trace "X" (list_rect (trace "X" ((unsafeCoerce (trace "X" (cv'))))) (trace "X" ((\a __U03ba_0 iH__U03ba_ _ ->
1821 (trace "X" ((trace "X" (weakV
1822 (trace "X" ((trace "X" ((let {
1824 (trace "X" (case (trace "X" (l)) of {
1825 ([]) -> (trace "X" (m));
1826 (:) a0 l1 -> (trace "X" ((:) (trace "X" (a0)) (trace "X" ((trace "X" ((app0 (trace "X" (l1)) (trace "X" (m)))))))))}))}
1827 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))))))
1829 weakT :: TypeEnv -> Kind -> Kind -> HaskType -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1830 weakT __U0393_0 __U03ba_ __U03ba___U2082_ lt ite =
1831 (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)))))))))))
1833 weakL :: TypeEnv -> Kind -> HaskLevel -> HaskLevel
1834 weakL __U0393_0 __U03ba_ lt =
1835 (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))))))
1837 weakT' :: TypeEnv -> (([]) Kind) -> Kind -> HaskType -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1838 weakT' __U0393_0 __U03ba_ __U03ba___U2082_ lt x =
1839 (trace "X" ((trace "X" (list_rect (trace "X" ((unsafeCoerce (trace "X" (lt))))) (trace "X" ((\a __U03ba_0 iH__U03ba_ _ ->
1840 (trace "X" ((trace "X" (weakT
1841 (trace "X" ((trace "X" ((let {
1843 (trace "X" (case (trace "X" (l)) of {
1844 ([]) -> (trace "X" (m));
1845 (:) a0 l1 -> (trace "X" ((:) (trace "X" (a0)) (trace "X" ((trace "X" ((app0 (trace "X" (l1)) (trace "X" (m)))))))))}))}
1846 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))))))
1848 weakT'' :: TypeEnv -> (([]) Kind) -> Kind -> HaskType -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1849 weakT'' __U0393_0 __U03ba_ __U03ba___U2082_ lt x =
1850 (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))))))))
1852 lamer :: (([]) Kind) -> (([]) Kind) -> (([]) Kind) -> Kind -> HaskType -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1853 lamer a b c __U03ba_ lt x =
1854 (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))))))))
1856 weakL' :: TypeEnv -> (([]) Kind) -> HaskLevel -> HaskLevel
1857 weakL' __U0393_0 __U03ba_ lev =
1858 (trace "X" ((trace "X" (list_rect (trace "X" (lev)) (trace "X" ((\a __U03ba_0 iH__U03ba_ ->
1859 (trace "X" ((trace "X" (weakL
1860 (trace "X" ((trace "X" ((let {
1862 (trace "X" (case (trace "X" (l)) of {
1863 ([]) -> (trace "X" (m));
1864 (:) a0 l1 -> (trace "X" ((:) (trace "X" (a0)) (trace "X" ((trace "X" ((app0 (trace "X" (l1)) (trace "X" (m)))))))))}))}
1865 in app0 (trace "X" (__U03ba_0)) (trace "X" (__U0393_0))))))) (trace "X" (a)) (trace "X" (iH__U03ba_))))))))) (trace "X" (__U03ba_))))))
1867 weakLT :: TypeEnv -> Kind -> Kind -> LeveledHaskType -> LeveledHaskType
1868 weakLT __U0393_0 __U03ba_ __U03ba___U2082_ lt =
1869 (trace "X" (case (trace "X" (lt)) of {
1870 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)))))))))}))
1872 weakLT' :: TypeEnv -> (([]) Kind) -> Kind -> LeveledHaskType -> LeveledHaskType
1873 weakLT' __U0393_0 __U03ba_ __U03ba___U2082_ lt =
1874 (trace "X" (case (trace "X" (lt)) of {
1875 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)))))))))}))
1877 weakICE :: TypeEnv -> Kind -> CoercionEnv -> (InstantiatedCoercionEnv a1 a2) -> InstantiatedCoercionEnv a1 a2
1878 weakICE __U0393_0 __U03ba_ __U0394_0 ice =
1879 (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)))))))))))
1881 weakCK :: TypeEnv -> Kind -> HaskCoercionKind -> (InstantiatedTypeEnv a1) -> RawCoercionKind a1
1882 weakCK __U0393_0 __U03ba_ hck x =
1883 (trace "X" ((trace "X" (unsafeCoerce (trace "X" (hck)) (trace "X" (__))
1884 (trace "X" ((case (trace "X" (x)) of {
1885 INil -> (trace "X" (false_rect));
1886 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))))))})))))))
1888 weakCK' :: TypeEnv -> (([]) Kind) -> HaskCoercionKind -> (InstantiatedTypeEnv a1) -> RawCoercionKind a1
1889 weakCK' __U0393_0 __U03ba_ hck x =
1890 (trace "X" ((trace "X" (list_rect (trace "X" ((unsafeCoerce (trace "X" (hck))))) (trace "X" ((\a __U03ba_0 iH__U03ba_ _ ->
1891 (trace "X" ((trace "X" (weakCK
1892 (trace "X" ((trace "X" ((let {
1894 (trace "X" (case (trace "X" (l)) of {
1895 ([]) -> (trace "X" (m));
1896 (:) a0 l1 -> (trace "X" ((:) (trace "X" (a0)) (trace "X" ((trace "X" ((app0 (trace "X" (l1)) (trace "X" (m)))))))))}))}
1897 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))))))
1899 weakCK'' :: TypeEnv -> (([]) Kind) -> (([]) HaskCoercionKind) -> ([]) HaskCoercionKind
1900 weakCK'' __U0393_0 __U03ba_ hck =
1901 (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))))))
1903 weakCV :: TypeEnv -> CoercionEnv -> Kind -> HaskCoVar -> (InstantiatedTypeEnv a1) -> (InstantiatedCoercionEnv a1 a2) -> a2
1904 weakCV __U0393_0 __U0394_0 __U03ba_ cv' ite ice =
1905 (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)))))))))))
1907 weakF :: TypeEnv -> Kind -> Kind -> (() -> (InstantiatedTypeEnv ()) -> () -> RawHaskType ()) -> (InstantiatedTypeEnv a1) -> a1 -> RawHaskType a1
1908 weakF __U0393_0 __U03ba_ __U03ba___U2082_ f ite tv =
1909 (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))))))
1911 caseType0 :: TypeEnv -> (([]) Kind) -> (IList Kind HaskType) -> HaskType -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1912 caseType0 __U0393_0 lk x x0 x1 =
1913 (trace "X" (case (trace "X" (lk)) of {
1914 ([]) -> (trace "X" ((trace "X" (unsafeCoerce (trace "X" (x0)) (trace "X" (__)) (trace "X" (x1))))));
1916 (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
1917 (trace "X" ((trace "X" ((let {
1919 (trace "X" (case (trace "X" (l)) of {
1920 ([]) -> (trace "X" (KindStar));
1921 (:) b t -> (trace "X" (KindArrow (trace "X" (b)) (trace "X" ((trace "X" ((fold_right0 (trace "X" (t)))))))))}))}
1922 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))))))}))
1924 caseType :: TypeEnv -> TyCon.TyCon -> (IList Kind HaskType) -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1925 caseType __U0393_0 tc atypes x =
1926 (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))))))
1929 Build_StrongAltCon WeakAltCon Nat Nat Nat (Vec Kind) (TypeEnv -> (IList Kind HaskType) -> Vec HaskCoercionKind) (TypeEnv -> (IList Kind HaskType) -> Vec HaskType)
1931 sac_altcon :: TyCon.TyCon -> StrongAltCon -> WeakAltCon
1933 (trace "X" (case (trace "X" (s)) of {
1934 Build_StrongAltCon x x0 x1 x2 x3 x4 x5 -> (trace "X" (x))}))
1936 sac_numExTyVars :: TyCon.TyCon -> StrongAltCon -> Nat
1937 sac_numExTyVars tc s =
1938 (trace "X" (case (trace "X" (s)) of {
1939 Build_StrongAltCon x x0 x1 x2 x3 x4 x5 -> (trace "X" (x0))}))
1941 sac_numCoerVars :: TyCon.TyCon -> StrongAltCon -> Nat
1942 sac_numCoerVars tc s =
1943 (trace "X" (case (trace "X" (s)) of {
1944 Build_StrongAltCon x x0 x1 x2 x3 x4 x5 -> (trace "X" (x1))}))
1946 sac_numExprVars :: TyCon.TyCon -> StrongAltCon -> Nat
1947 sac_numExprVars tc s =
1948 (trace "X" (case (trace "X" (s)) of {
1949 Build_StrongAltCon x x0 x1 x2 x3 x4 x5 -> (trace "X" (x2))}))
1951 sac_ekinds :: TyCon.TyCon -> StrongAltCon -> Vec Kind
1953 (trace "X" (case (trace "X" (s)) of {
1954 Build_StrongAltCon x x0 x1 x2 x3 x4 x5 -> (trace "X" (x3))}))
1956 sac___U0393_ :: TyCon.TyCon -> StrongAltCon -> (([]) Kind) -> ([]) Kind
1957 sac___U0393_ tc s __U0393_0 =
1958 (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))))))
1960 sac_coercions :: TyCon.TyCon -> StrongAltCon -> TypeEnv -> (IList Kind HaskType) -> Vec HaskCoercionKind
1961 sac_coercions tc s =
1962 (trace "X" (case (trace "X" (s)) of {
1963 Build_StrongAltCon x x0 x1 x2 x3 x4 x5 -> (trace "X" (x4))}))
1965 sac_types :: TyCon.TyCon -> StrongAltCon -> TypeEnv -> (IList Kind HaskType) -> Vec HaskType
1967 (trace "X" (case (trace "X" (s)) of {
1968 Build_StrongAltCon x x0 x1 x2 x3 x4 x5 -> (trace "X" (x5))}))
1970 sac___U0394_ :: TyCon.TyCon -> StrongAltCon -> TypeEnv -> (IList Kind HaskType) -> (([]) HaskCoercionKind) -> ([]) HaskCoercionKind
1971 sac___U0394_ tc s __U0393_0 atypes __U0394_0 =
1972 (trace "X" ((trace "X" (app (trace "X" ((trace "X" ((vec2list (trace "X" ((trace "X" ((sac_numCoerVars (trace "X" ((Prelude.error "Proj Args"))) (trace "X" (s))))))) (trace "X" ((trace "X" ((sac_coercions (trace "X" ((Prelude.error "Proj Args"))) (trace "X" (s)) (trace "X" (__U0393_0)) (trace "X" (atypes)))))))))))) (trace "X" (__U0394_0))))))
1974 literalType :: Literal.Literal -> TypeEnv -> (InstantiatedTypeEnv a1) -> RawHaskType a1
1975 literalType lit __U0393_0 x =
1976 (trace "X" (let {z = (trace "X" (\ite -> (trace "X" (TCon (trace "X" ((trace "X" ((haskLiteralToTyCon (trace "X" (lit)))))))))))} in (trace "X" ((trace "X" (eq_rect (trace "X" ((trace "X" ((tyConKind (trace "X" ((trace "X" ((haskLiteralToTyCon (trace "X" (lit)))))))))))) (trace "X" ((\_ ite -> (trace "X" ((trace "X" (z (trace "X" (ite))))))))) (trace "X" (([]))) (trace "X" (__)) (trace "X" (x))))))))
1978 update___U03be_ :: (EqDecidable a1) -> TypeEnv -> (a1 -> LeveledHaskType) -> HaskLevel -> (([]) ((,) a1 HaskType)) -> a1 -> LeveledHaskType
1979 update___U03be_ eQD_VV __U0393_0 __U03be_0 lev vt =
1980 (trace "X" (case (trace "X" (vt)) of {
1981 ([]) -> (trace "X" (__U03be_0));
1982 (:) p tl -> (trace "X" ((\v' ->
1983 (trace "X" (case (trace "X" (p)) of {
1985 (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eQD_VV)) (trace "X" (v)) (trace "X" (v')))))) of {
1986 Prelude.True -> (trace "X" (MkLeveledHaskType (trace "X" (__U03c4_)) (trace "X" (lev))));
1987 Prelude.False -> (trace "X" ((trace "X" (update___U03be_ (trace "X" (eQD_VV)) (trace "X" (__U0393_0)) (trace "X" (__U03be_0)) (trace "X" (lev)) (trace "X" (tl)) (trace "X" (v'))))))}))})))))}))
1989 compareT :: Nat -> Kind -> (RawHaskType Nat) -> Kind -> (RawHaskType Nat) -> Prelude.Bool
1990 compareT n __U03ba___U2081_ t1 __U03ba___U2082_ t2 =
1991 (trace "X" (case (trace "X" (t1)) of {
1993 (trace "X" (case (trace "X" (t2)) of {
1994 TVar __U03ba_0 x' ->
1995 (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (eqDecidableNat)) (trace "X" (x)) (trace "X" (x')))))) of {
1996 Prelude.True -> (trace "X" (Prelude.True));
1997 Prelude.False -> (trace "X" (Prelude.False))}));
1998 _ -> (trace "X" (Prelude.False))}));
2000 (trace "X" (case (trace "X" (t2)) of {
2002 (trace "X" (case (trace "X" ((trace "X" (eqd_dec (trace "X" (tyConEqDecidable)) (trace "X" (tc)) (trace "X" (tc')))))) of {
2003 Prelude.True -> (trace "X" (Prelude.True));
2004 Prelude.False -> (trace "X" (Prelude.False))}));
2005 _ -> (trace "X" (Prelude.False))}));
2007 (trace "X" (case (trace "X" (t2)) of {
2008 TArrow -> (trace "X" (Prelude.True));
2009 _ -> (trace "X" (Prelude.False))}));
2010 TCoerc __U03ba_ t3 t4 t ->
2011 (trace "X" (case (trace "X" (t4)) of {
2012 TCoerc __U03ba_0 t1' t2' t' ->
2013 (trace "X" (case (trace "X" (case (trace "X" ((trace "X" (compareT (trace "X" (n)) (trace "X" (__U03ba_)) (trace "X" (t3)) (trace "X" (__U03ba_0)) (trace "X" (t1')))))) of {
2014 Prelude.True -> (trace "X" ((trace "X" (compareT (trace "X" (n)) (trace "X" (__U03ba_)) (trace "X" (t4)) (trace "X" (__U03ba_0)) (trace "X" (t2'))))));
2015 Prelude.False -> (trace "X" (Prelude.False))})) of {
2016 Prelude.True -> (trace "X" ((trace "X" (compareT (trace "X" (n)) (trace "X" (KindStar)) (trace "X" (t)) (trace "X" (KindStar)) (trace "X" (t'))))));
2017 Prelude.False -> (trace "X" (Prelude.False))}));
2018 _ -> (trace "X" (Prelude.False))}));
2019 TApp __U03ba___U2081_0 __U03ba___U2082_0 x y ->
2020 (trace "X" (case (trace "X" (t2)) of {
2021 TApp __U03ba___U2081_1 __U03ba___U20