minor cleanups in HaskStrongToWeak

[coq-hetmet.git] / src / HaskWeakToStrong.v

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index d765f0f..8a5fbe5 100644 (file)
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -19,7 +19,6 @@ Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
-Require Import HaskCoreToWeak.
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
@@ -158,10 +157,11 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     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").
@@ -559,7 +559,7 @@ Definition weakExprToStrongExpr : forall
                                                    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' =>