X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;fp=src%2FHaskStrongToWeak.v;h=8bb52e12f6ee81c217dd02d4ccc323519f395be2;hp=deb7adc20b2b1bb7dfd4edf42c319d1cfad65240;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=6282ce834832ba35e81d8019cae1ca38d187d07e

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index deb7adc..8bb52e1 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -79,6 +79,18 @@ Section HaskStrongToWeak.
   Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ)
     := tv::::ite.
   
+  Definition updateITE_ {Γ:TypeEnv}{TV:Kind->Type}{κ}{n}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ)
+    : InstantiatedTypeEnv TV (list_ins n κ Γ).
+    rewrite list_ins_app.
+    rewrite <- (list_take_drop _ Γ n) in ite.
+    apply ilist_app.
+    apply ilist_chop in ite; auto.
+    apply ICons.
+    apply tv.
+    apply ilist_chop' in ite.
+    apply ite.
+    Defined.
+  
   Definition coercionToWeakCoercion Γ Δ κ t1 t2 ite (γ:@HaskCoercion Γ Δ (@mkHaskCoercionKind Γ κ t1 t2))
     : UniqM WeakCoercion
     := bind t1' = @typeToWeakType Γ κ t1 ite
@@ -144,8 +156,8 @@ Section HaskStrongToWeak.
     | ECast Γ Δ ξ t1 t2 γ l e      => fun ite  => bind e' = exprToWeakExpr χ e ite
                                                 ; bind c' = coercionToWeakCoercion _ _ _ _ _ ite γ
                                                 ; return WECast e' c'
-    | ETyLam _ _ _ k _ _ e          => fun ite => bind tv = mkWeakTypeVar k
-                                                ; bind e' = exprToWeakExpr χ e (updateITE tv ite)
+    | ETyLam _ _ _ k _ _ n e        => fun ite => bind tv = mkWeakTypeVar k
+                                                ; bind e' = exprToWeakExpr χ e (updateITE_ tv ite)
                                                 ; return WETyLam tv e'
     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => fun ite => bind t1' = typeToWeakType σ₁ ite
                                                 ; bind t2' = typeToWeakType σ₂ ite