| WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _
| WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _
| WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _
- | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _
+ | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody
+ >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _
| WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in
weakTypeToType _ φ t1 >>= fun t1' =>
weakTypeToType _ φ t2 >>= fun t2' =>
apply OK.
eapply haskTypeOfSomeKind.
unfold HaskType; intros.
- apply TyFunApp.
+ apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
apply lt'.
apply X.
exact (Error "checkDistinct failed").
Defined.
+(* FIXME: check the kind of the type of the weakexprvar to support >0 *)
+Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
+ refine {| glob_kinds := nil |}.
+ apply wev.
+ intros.
+ apply τ.
+ Defined.
+
Definition weakExprToStrongExpr : forall
(Γ:TypeEnv)
(Δ:CoercionEnv Γ)
match we with
| WEVar v => if ig v
- then OK (EGlobal Γ Δ ξ (τ@@lev) v)
+ then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
| WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)