Commit d6216443 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix an infinite loop in niFixTCvSubst

Trac #14164 made GHC loop, a pretty serious error. It turned
out that Unify.niFixTCvSubst was looping forever, because we
had a substitution like
    a :-> ....(b :: (c :: d))....
    d :-> ...
We correctly recognised that d was free in the range of the
substitution, but then failed to apply it "deeeply enough"
to the range of the substiuttion, so d was /still/ free in
the range, and we kept on going.

Trac #9106 was caused by a similar problem, but alas my
fix to Trac #9106 was inadequate when the offending type
variable is more deeply buried.  Urk.

This time I think I've fixed it!  It's much more subtle
than I though, and it took most of a long train journey
to figure it out.  I wrote a long note to explain:
Note [Finding the substitution fixpoint]
parent 50d7b2ac
......@@ -37,6 +37,7 @@ import Type hiding ( getTvSubstEnv )
import Coercion hiding ( getCvSubstEnv )
import TyCon
import TyCoRep hiding ( getTvSubstEnv, getCvSubstEnv )
import FV( FV, fvVarSet, fvVarList )
import Util
import Pair
import Outputable
......@@ -546,7 +547,7 @@ During unification we use a TvSubstEnv/CvSubstEnv pair that is
Note [Finding the substitution fixpoint]
Finding the fixpoint of a non-idempotent substitution arising from a
unification is harder than it looks, because of kinds. Consider
unification is much trickier than it looks, because of kinds. Consider
T k (H k (f:k)) ~ T * (g:*)
If we unify, we get the substitution
[ k -> *
......@@ -561,41 +562,96 @@ If we don't do this, we may apply the substitution to something,
and get an ill-formed type, i.e. one where typeKind will fail.
This happened, for example, in Trac #9106.
This is the reason for extending env with [f:k -> f:*], in the
definition of env' in niFixTvSubst
It gets worse. In Trac #14164 we wanted to take the fixpoint of
this substitution
[ xs_asV :-> F a_aY6 (z_aY7 :: a_aY6)
(rest_aWF :: G a_aY6 (z_aY7 :: a_aY6))
, a_aY6 :-> a_aXQ ]
We have to apply the substitution for a_aY6 two levels deep inside
the invocation of F! We don't have a function that recursively
applies substitutions inside the kinds of variable occurrences (and
probably rightly so).
So, we work as follows:
1. Start with the current substitution (which we are
trying to fixpoint
[ xs :-> F a (z :: a) (rest :: G a (z :: a))
, a :-> b ]
2. Take all the free vars of the range of the substitution:
{a, z, rest, b}
NB: the free variable finder closes over
the kinds of variable occurrences
3. If none are in the domain of the substitution, stop.
We have found a fixpoint.
4. Remove the variables that are bound by the substitution, leaving
{z, rest, b}
5. Do a topo-sort to put them in dependency order:
[ b :: *, z :: a, rest :: G a z ]
6. Apply the substitution left-to-right to the kinds of these
tyvars, extendinng it each time with a new binding, so we
finish up with
[ xs :-> before..
, a :-> before..
, b :-> b :: *
, z :-> z :: b
, rest :-> rest :: G a (z :: b) ]
Note that rest now has the right kind
7. Apply this extended substution (once) to the range of
the /original/ substituion. (Note that we do the
extended substitution would go on forever if you tried
to find its fixpoint, becuase it maps z to z.)
8. And go back to step 1
In Step 6 we use the free vars from Step 2 as the initial
in-scope set, because all of those variables appear in the
range of the substitution, so they must all be in the in-scope
set. But NB that the type substitution engine does not look up
variables in the in-scope set; it is used only to ensure no
niFixTCvSubst :: TvSubstEnv -> TCvSubst
-- Find the idempotent fixed point of the non-idempotent substitution
-- See Note [Finding the substitution fixpoint]
-- This is surprisingly tricky:
-- see Note [Finding the substitution fixpoint]
-- ToDo: use laziness instead of iteration?
niFixTCvSubst tenv = f tenv
niFixTCvSubst tenv
| not_fixpoint = niFixTCvSubst (mapVarEnv (substTy subst) tenv)
| otherwise = subst
f tenv
| not_fixpoint = f (mapVarEnv (substTy subst') tenv)
| otherwise = subst
not_fixpoint = anyVarSet in_domain range_tvs
in_domain tv = tv `elemVarEnv` tenv
range_tvs = nonDetFoldUFM (unionVarSet . tyCoVarsOfType) emptyVarSet tenv
-- It's OK to use nonDetFoldUFM here because we
-- forget the order immediately by creating a set
subst = mkTvSubst (mkInScopeSet range_tvs) tenv
-- env' extends env by replacing any free type with
-- that same tyvar with a substituted kind
-- See note [Finding the substitution fixpoint]
tenv' = extendVarEnvList tenv [ (rtv, mkTyVarTy $
setTyVarKind rtv $
substTy subst $
tyVarKind rtv)
| rtv <- nonDetEltsUniqSet range_tvs
-- It's OK to use nonDetEltsUniqSet here
-- because we forget the order
-- immediatedly by putting it in VarEnv
, not (in_domain rtv) ]
subst' = mkTvSubst (mkInScopeSet range_tvs) tenv'
range_fvs :: FV
range_fvs = tyCoFVsOfTypes (nonDetEltsUFM tenv)
-- It's OK to use nonDetEltsUFM here because the
-- order of range_fvs, range_tvs is immaterial
range_tvs :: [TyVar]
range_tvs = fvVarList range_fvs
not_fixpoint = any in_domain range_tvs
in_domain tv = tv `elemVarEnv` tenv
free_tvs = toposortTyVars (filterOut in_domain range_tvs)
-- See Note [Finding the substitution fixpoint], Step 6
init_in_scope = mkInScopeSet (fvVarSet range_fvs)
subst = foldl add_free_tv
(mkTvSubst init_in_scope tenv)
add_free_tv :: TCvSubst -> TyVar -> TCvSubst
add_free_tv subst tv
= extendTvSubst subst tv (mkTyVarTy tv')
tv' = updateTyVarKind (substTy subst) tv
niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
-- Apply the non-idempotent substitution to a set of type variables,
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module T14164 where
data G (x :: a) = GNil | GCons (G x)
type family F (xs :: [a]) (g :: G (z :: a)) = (res :: [a]) | res -> a where
F (x:xs) GNil = x:xs
F (x:xs) (GCons rest) = x:F xs rest
......@@ -283,3 +283,4 @@ test('T15057', normal, compile, [''])
test('T15144', normal, compile, [''])
test('T15122', normal, compile, [''])
test('T13777', normal, compile, [''])
test('T14164', normal, compile, [''])
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment