+Fixpoint coreTypeToWeakType (ct:CoreType) : ???WeakType :=
+ match ct with
+ | TyVarTy cv => match coreVarToWeakVar cv with
+ | WExprVar _ => Error "encountered expression variable in a type"
+ | WTypeVar tv => OK (WTyVarTy tv)
+ | WCoerVar _ => 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 if (isFamilyTyCon tc)
+ then recurse >>= fun recurse' => OK (WTyFunApp tc recurse')
+ else if eqd_dec tc ModalBoxTyCon
+ then match lct with
+ | ((TyVarTy ec)::tbody::nil) =>
+ match coreVarToWeakVar ec with
+ | WTypeVar ec' => coreTypeToWeakType tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
+ | WExprVar _ => Error "encountered expression variable in a modal box type"
+ | WCoerVar _ => Error "encountered coercion variable in a modal box type"
+ end
+ | _ => Error "mis-applied modal box tycon"
+ 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')
+ | 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
+ | WExprVar _ => Error "encountered expression variable in a type"
+ | WTypeVar tv => coreTypeToWeakType t >>= fun t' => OK (WForAllTy tv t')
+ | WCoerVar _ => Error "encountered coercion variable in a type"
+ 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.
+