X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=42790b3ae7590afafff90623ceef14089c08077f;hp=e956dd659394f4eb9c9a3853f214ac67a8ce8f7b;hb=35d3a59796735e5341389fa6a145f62dcea9c3fc;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index e956dd6..42790b3 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -61,7 +61,7 @@ Section HaskStrongToWeak.
                                      | WTyVarTy ec => return WCodeTy ec t2'
                                      | _           => failM  "impossible"
                                    end
-    | TyFunApp    tfc tls       => bind tls' = rawHaskTypeListToWeakType tls
+    | TyFunApp    tfc _ _ tls       => bind tls' = rawHaskTypeListToWeakType tls
                                  ; return WTyFunApp tfc tls'
   end
   with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
@@ -111,7 +111,8 @@ Section HaskStrongToWeak.
     -> UniqM WeakExpr :=
     match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
     | EVar  Γ' _ ξ' ev              => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
-    | EGlobal Γ' _ ξ' t wev         => fun ite => return WEVar wev
+    | EGlobal Γ' _ ξ'   g v lev     => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
+                                                ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
     | ELam  Γ'   _ _ tv _ _ cv e    => fun ite => bind tv' = typeToWeakType tv ite
                                                 ; bind ev' = mkWeakExprVar tv'
                                                 ; bind e'  = exprToWeakExpr (update_χ χ cv ev') e ite
@@ -181,7 +182,7 @@ Section HaskStrongToWeak.
                                   (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
                   ; return WECase vscrut' escrut' tbranches' tc tys branches'
 
-    | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
+    | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
                                                                         => bind tleaf = typeToWeakType (snd vt) ite
                                                                          ; bind v' = mkWeakExprVar tleaf
                                                                          ; return ((fst vt),v'))