diff --git a/frege/compiler/tc/Util.fr b/frege/compiler/tc/Util.fr index e02df0a0..3c95d68c 100644 --- 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]