Require Import HaskStrong.
Require Import HaskCoreTypes.
Require Import HaskCoreVars.
-Require Import HaskCoreToWeak.
Open Scope string_scope.
Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
apply (addErrorMessage "case_WAppTy").
destruct t1' as [k1' t1'].
destruct t2' as [k2' t2'].
+ set ("tried to apply type "+++t1'+++" of kind "+++k1'+++" to type "+++t2'+++" of kind "+++k2') as err.
destruct k1';
try (matchThings k1'1 k2' "Kind mismatch in WAppTy: ";
subst; apply OK; apply (haskTypeOfSomeKind (fun TV env => TApp (t1' TV env) (t2' TV env))));
- apply (Error "Kind mismatch in WAppTy:: ").
+ apply (Error ("Kind mismatch in WAppTy: "+++err)).
destruct case_weakTypeListToTypeList.
apply (addErrorMessage "case_weakTypeListToTypeList").
weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
- | WECast e co => let (_,t1,t2,_) := co in
+ | WECast e co => let (t1,t2) := weakCoercionTypes co in
weakTypeToType'' φ t1 ★ >>= fun t1' =>
weakTypeToType'' φ t2 ★ >>= fun t2' =>
weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>