build/CoqPass.hs

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