X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=7dd93ad0dffbb1d8b2af303722454ac9f2b42a18;hp=122db2afc13408cffed68494a968c0a7c7bd4abc;hb=68f41d71d573b422b04ed3f4a3eb3ab41de09a79;hpb=b4857a6f575dffd5c9c9d5decbc21ff63a338270

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 122db2a..7dd93ad 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -10,7 +10,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
@@ -18,6 +19,7 @@ Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
@@ -140,7 +142,11 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
                       end
           | tx::lt' => weakTypeToType Γ φ tx >>= fun t' =>
                         match lk as LK return ???(forall TV (ite:InstantiatedTypeEnv TV Γ), @RawHaskTypeList TV LK) with
-                          | nil    => Error "WTyFunApp applied to too many types"
+                          | nil    => Error ("WTyFunApp applied to too many types"(* +++ eol +++
+                                             "  tyCon= "           +++ toString tc +++ eol +++
+                                             "  tyConKindArgs= "   +++ toString (fst (tyFunKind tc)) +++ eol +++
+                                             "  tyConKindResult= " +++ toString (snd (tyFunKind tc)) +++ eol +++
+                                             "  types= "           +++ toString lt +++ eol*))
                           | k::lk' => weakTypeListToTypeList lk' lt' >>= fun rhtl' =>
                                         let case_weakTypeListToTypeList := tt in _
                         end
@@ -164,7 +170,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
       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: "+++err)).
-   
+
   destruct case_weakTypeListToTypeList.
     apply (addErrorMessage "case_weakTypeListToTypeList").
     destruct t' as [ k' t' ].
@@ -415,7 +421,7 @@ Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Ex
   Defined.
 
 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
-  match wcv with weakCoerVar _ κ _ _ => κ end.
+  match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
   Coercion coVarKind : WeakCoerVar >-> Kind.
 
 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
@@ -630,7 +636,7 @@ Definition weakExprToStrongExpr : forall
                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++toString te)
                                            end
 
-    | WECoLam cv e                      => let (_,_,t1,t2) := cv in
+    | WECoLam cv e                      => let (_,t1,t2) := cv in
                                            weakTypeOfWeakExpr e >>= fun te =>
                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>