+Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
+Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep".
+Variable coercionKind : CoreCoercion -> (CoreType * CoreType).
+ Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))".
+
+(* extracts the Name from a CoreVar *)
+Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName".
+
+(* the magic wired-in name for the modal type introduction/elimination forms *)
+Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
+Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
+Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
+
+Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
+ split_list lwt (length (fst (tyFunKind tf))) >>=
+ fun argsrest =>
+ let (args,rest) := argsrest in
+ OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)).
+
+(* a hack to evade the guardedness check of Fixpoint *)
+Variable coreTypeToWeakTypeCheat' : CoreType -> ???WeakType.
+Extract Inlined Constant coreTypeToWeakTypeCheat' => "coreTypeToWeakType'".
+
+Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
+ match ct with
+ | TyVarTy cv => match coreVarToWeakVar cv with
+ | CVTWVR_EVar ct => Error "encountered expression variable in a type"
+ | CVTWVR_TyVar k => OK (WTyVarTy (weakTypeVar cv k))
+ | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a type"
+ end
+
+ | AppTy t1 t2 => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
+
+ | TyConApp tc_ lct =>
+ let recurse := ((fix rec tl := match tl with
+ | nil => OK nil
+ | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
+ end) lct)
+ in match tyConOrTyFun tc_ with
+ | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'
+ | inl tc => if eqd_dec tc ModalBoxTyCon
+ then match lct with
+ | ((TyVarTy ec)::tbody::nil) =>
+ match coreVarToWeakVar ec with
+ | CVTWVR_EVar ct => Error "encountered expression variable in a modal box type"
+ | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a modal box type"
+ | CVTWVR_TyVar k => coreTypeToWeakType' tbody >>= fun tbody' =>
+ OK (WCodeTy (weakTypeVar ec k) tbody')
+ end
+ | _ => Error ("mis-applied modal box tycon: " +++ toString ct)
+ end
+ else let tc' := if eqd_dec tc ArrowTyCon
+ then WFunTyCon
+ else WTyCon tc
+ in recurse >>= fun recurse' => OK (fold_left (fun x y => WAppTy x y) recurse' tc')
+ end
+ | FunTy (PredTy (EqPred t1 t2)) t3 => coreTypeToWeakType' t1 >>= fun t1' =>
+ coreTypeToWeakType' t2 >>= fun t2' =>
+ coreTypeToWeakType' t3 >>= fun t3' =>
+ OK (WCoFunTy t1' t2' t3')
+ | FunTy t1 t2 => coreTypeToWeakType' t1 >>= fun t1' =>
+ coreTypeToWeakType' t2 >>= fun t2' =>
+ OK (WAppTy (WAppTy WFunTyCon t1') t2')
+ | ForAllTy cv t => match coreVarToWeakVar cv with
+ | CVTWVR_EVar ct => Error "encountered expression variable in a type abstraction"
+ | CVTWVR_TyVar k => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy (weakTypeVar cv k) t')
+ | CVTWVR_CoVar t1 t2 => coreTypeToWeakTypeCheat' t1 >>= fun t1' =>
+ coreTypeToWeakTypeCheat' t2 >>= fun t2' =>
+ coreTypeToWeakType' t >>= fun t3' =>
+ OK (WCoFunTy t1' t2' t3')
+ end
+ | PredTy (ClassP cl lct) => ((fix rec tl := match tl with
+ | nil => OK nil
+ | a::b => coreTypeToWeakType' a >>= fun a' =>
+ rec b >>= fun b' => OK (a'::b')
+ end) lct) >>= fun lct' => OK (WClassP cl lct')
+ | PredTy (IParam ipn ct) => coreTypeToWeakType' ct >>= fun ct' => OK (WIParam ipn ct')
+ | PredTy (EqPred _ _) => Error "hit a bare EqPred"
+ end.
+
+Definition coreTypeToWeakType t :=
+ addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).
+
+Definition coreVarToWeakVar' (cv:CoreVar) : ???WeakVar :=
+ addErrorMessage ("during coreVarToWeakVar on " +++ toString cv +++ eol)
+ match coreVarToWeakVar cv with
+ | CVTWVR_EVar ct => coreTypeToWeakType ct >>= fun t' => OK (WExprVar (weakExprVar cv t'))
+ | CVTWVR_TyVar k => OK (WTypeVar (weakTypeVar cv k))
+ | CVTWVR_CoVar t1 t2 =>
+ (* this will choke if given a coercion-between-coercions (EqPred (EqPred c1 c2) (EqPred c3 c4)) *)
+ addErrorMessage ("with t2=" +++ toString t2 +++ eol)
+ ((coreTypeToWeakType t2) >>= fun t2' =>
+ addErrorMessage ("with t1=" +++ toString t1 +++ eol)
+ (coreTypeToWeakType t1) >>= fun t1' =>
+ OK (WCoerVar (weakCoerVar cv t1' t2')))
+ end.
+Definition tyConTyVars (tc:CoreTyCon) :=
+ filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (getTyConTyVars_ tc)).
+ Opaque tyConTyVars.
+Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).