X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=8a5fbe50f075565b776de5ae6a25b89e3d229b05;hp=e5c88f8472c3c9002dd34873c3c979115618e28d;hb=825fa62636c32762ac2e1c1357209119de74c281;hpb=54e3d85658516dcf7d8504e94f973a87e255f8f3

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index e5c88f8..8a5fbe5 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -157,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").