+ | WECoApp e co => weakTypeOfWeakExpr e >>= fun te =>
+ match te with
+ | WCoFunTy t1 t2 t3 =>
+ weakTypeToType φ t1 >>= fun t1' =>
+ match t1' with
+ haskTypeOfSomeKind κ t1'' =>
+ weakTypeToType'' φ t2 κ >>= fun t2'' =>
+ weakTypeToType'' φ t3 ★ >>= fun t3'' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' =>
+ castExpr "WECoApp" _ e' >>= fun e'' =>
+ OK (ECoApp Γ Δ κ t1'' t2''
+ (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'')
+ end
+ | _ => Error ("weakTypeToType: WECoApp body with type "+++te)
+ end
+
+ | WECoLam cv e => let (_,_,t1,t2) := cv in
+ weakTypeOfWeakExpr e >>= fun te =>
+ weakTypeToType'' φ te ★ >>= fun te' =>
+ weakTypeToType'' φ t1 cv >>= fun t1' =>
+ weakTypeToType'' φ t2 cv >>= fun t2' =>
+ weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
+ castExpr "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
+
+ | WECast e co => let (κ,t1,t2,_) := co in
+ weakTypeToType'' φ t1 ★ >>= fun t1' =>
+ weakTypeToType'' φ t2 ★ >>= fun t2' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>
+ castExpr "WECast" _
+ (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e')
+
+ | WELetRec rb e =>
+ let ξ' := update_ξ ξ (map (fun x => ((fst x),(snd x @@ lev))) _)
+ in let binds :=
+ (fix binds (t:Tree ??(WeakExprVar * WeakExpr))
+ : ???(ELetRecBindings Γ Δ ξ' lev (varsTypes t φ)) :=
+ match t with
+ | T_Leaf None => let case_nil := tt in OK (ELR_nil _ _ _ _)
+ | T_Leaf (Some (wev,e)) => let case_some := tt in (fun e' => _) (fun τ => weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e)
+ | T_Branch b1 b2 =>
+ binds b1 >>= fun b1' =>
+ binds b2 >>= fun b2' =>
+ OK (ELR_branch Γ Δ ξ' lev _ _ b1' b2')
+ end) rb
+ in binds >>= fun binds' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' =>
+ OK (ELetRec Γ Δ ξ lev τ _ binds' e')
+
+ | WECase e tbranches tc avars alts =>
+ mkAvars avars (tyConKind tc) φ >>= fun avars' =>
+ weakTypeToType'' φ tbranches ★ >>= fun tbranches' =>
+ weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' =>
+(fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree
+ ??{scb
+ : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars'
+ &
+ Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))
+ (scbwv_ξ scb ξ lev) (weakLT' (tbranches' @@ lev))}) :=
+ match t with
+ | T_Leaf None => OK []
+ | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) =>
+ mkStrongAltConPlusJunk' tc ac >>= fun sac =>
+ list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") >>= fun exprvars' =>
+ let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in
+ weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ)
+ (scbwv_ξ scb ξ lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' =>
+ let case_case := tt in OK [ _ ]
+ | T_Branch b1 b2 =>
+ mkTree b1 >>= fun b1' =>
+ mkTree b2 >>= fun b2' =>
+ OK (b1',,b2')
+ end
+) alts >>= fun tree =>
+ castExpr "ECase" _ (ECase Γ Δ ξ lev tc tbranches' avars' e' tree)