X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=f6dc70149d77fff47d45a0adeffdd113f446caa0;hp=d8dcf42003abbef5304e67118b85579ade405d90;hb=6eacd82007b7dacd704e50e5da0a9c988827f86c;hpb=4c5c94487aa2bf5489371f112607f0a4c4f01a94

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index d8dcf42..f6dc701 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -26,6 +26,11 @@ Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
 Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ).
 
+Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a  b) c) κ) : HaskType (app a (app b c)) κ.
+  rewrite <- ass_app in lt.
+  exact lt.
+  Defined.
+
 Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ).
   unfold TyVarResolver.
   refine (fun tv' =>
@@ -484,6 +489,10 @@ Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool :=
     | WELet    cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
     | WEApp    e1 e2    => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
     | WELam    cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+(*
+    | WEKappaApp  e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
+    | WEKappa  cv e     => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+*)
     | WETyLam  cv e     => doesWeakVarOccur wev e
     | WECoLam  cv e     => doesWeakVarOccur wev e
     | WECase vscrut escrut tbranches tc avars alts =>
@@ -604,9 +613,11 @@ Definition weakExprToStrongExpr : forall
     | WETyLam tv e                      => let φ2 := upPhi tv φ in
                                              weakTypeOfWeakExpr e >>= fun te =>
                                                weakTypeToTypeOfKind φ2 te ★ >>= fun τ' =>
-                                                 weakExprToStrongExpr _ (weakCE Δ) φ2
-                                                   (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e
-                                                     >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e')
+                                                 weakExprToStrongExpr _ (weakCE_(n:=O) Δ) φ2
+                                                   (fun x => (ψ x) >>= fun y =>
+                                                     OK (weakCV_ y)) (weakLT_○ξ) ig _ (weakL_ lev) e
+                                                   >>= fun e' => castExpr we "WETyLam2" _ _
+                                                     (ETyLam Γ Δ ξ tv (mkTAll' τ') lev 0 e')
 
     | WETyApp e t                       => weakTypeOfWeakExpr e >>= fun te =>
                                            match te with