Require Import HaskWeakTypes.
Require Import HaskWeak.
-Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
-Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
-
Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
| WCoerVar _ => Error "found a coercion variable in a case"
| WExprVar ev =>
coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
- coreExprToWeakExpr e >>= fun e' =>
expectTyConApp te' nil >>= fun tca =>
- let (tc,lt) := tca in
+ let (tc,lt) := tca:(TyCon * list WeakType) in
((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
: ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match branches with