correct quantification for generic kinds

Frege · Apr 8, 2018 · 992b70b · 992b70b
1 parent b518102
commit 992b70b
Showing 1 changed file with 16 additions and 2 deletions.
diff --git a/frege/compiler/tc/Util.fr b/frege/compiler/tc/Util.fr
@@ -541,6 +541,11 @@ zonkTau (m@Meta tv)      = do
                             stio ty
 zonkTau other = stio other      -- TVar and TCon
 
+zonkKind ∷ Kind → StG Kind
+zonkKind (KGen t) = KGen <$> zonkTau t
+zonkKind other    = pure other
+
+
 substRigidSigma [] sigma = sigma
 substRigidSigma bound (ForAll b rho) = ForAll b
         (substRigidRho (filter (`notElem` map _.var b) bound) rho)
@@ -588,7 +593,10 @@ quantifiedExcept exc rhos = do
             bound   = zip newvars allTvs
             -- make sigma for rho with the tvs that appear in that rho
             mksig ∷ [(String,MetaTv)] → (Rho,[MetaTv]) → StG Sigma
-            mksig bound (rho,tvs) = liftM (ForAll nv) (zonkRho rho)
+            mksig bound (rho,tvs) = do
+                    nvz ← mapM (\tv → zonkKind tv.kind >>= pure . tv.{kind=}) nv
+                    rhoz ← zonkRho rho
+                    pure (ForAll nvz rhoz) 
                 where nv = [ TVar{pos, kind=MetaTv.kind v, var=n} | (n,v) <- bound, v `elem` tvs]
                       pos = getpos rho
         foreach bound bind                              -- actually write TVars in the MetaTvs
@@ -598,7 +606,13 @@ quantifiedExcept exc rhos = do
         -- TVar names used in the Rhos
         used = [ u | r <- rhos, u <- tyVarBndrs r ]
         bind ∷ (String,MetaTv) → StG ()
-        bind (var,tv) = writeTv tv (TVar {pos, var, kind=tv.kind})
+        bind (var,tv) = case tv.kind of
+            KGen t → do
+                        writeTv tv (TVar {pos, var, kind=KVar})
+                        t' ← zonkTau t
+                        writeTv tv (TVar {pos, var, kind=KGen t'})
+            other  → writeTv tv (TVar {pos, var, kind=tv.kind})
+
 
 quantify rho = do
     sigs <- quantified [rho]