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

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index d8dcf42..0acc0af 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' =>
@@ -604,9 +609,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