[commit: ghc] master: Fix an infinite loop in niFixTCvSubst (d621644)
git at git.haskell.org
git at git.haskell.org
Mon Jun 18 07:23:51 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/d6216443c61cee94d8ffc31ca8510a534d9406b9/ghc
>---------------------------------------------------------------
commit d6216443c61cee94d8ffc31ca8510a534d9406b9
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Sat Jun 16 23:25:53 2018 +0100
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]
>---------------------------------------------------------------
d6216443c61cee94d8ffc31ca8510a534d9406b9
compiler/types/Unify.hs | 116 +++++++++++++++------
.../tests/indexed-types/should_compile/T14164.hs | 10 ++
testsuite/tests/indexed-types/should_compile/all.T | 1 +
3 files changed, 97 insertions(+), 30 deletions(-)
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index 9833f8e..8f69172 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -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 :-> ..as before..
+ , a :-> ..as 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
+shadowing.
-}
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
where
- f tenv
- | not_fixpoint = f (mapVarEnv (substTy subst') tenv)
- | otherwise = subst
- where
- 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)
+ free_tvs
+
+ add_free_tv :: TCvSubst -> TyVar -> TCvSubst
+ add_free_tv subst tv
+ = extendTvSubst subst tv (mkTyVarTy tv')
+ where
+ tv' = updateTyVarKind (substTy subst) tv
niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
-- Apply the non-idempotent substitution to a set of type variables,
diff --git a/testsuite/tests/indexed-types/should_compile/T14164.hs b/testsuite/tests/indexed-types/should_compile/T14164.hs
new file mode 100644
index 0000000..1cf6f2d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T14164.hs
@@ -0,0 +1,10 @@
+{-# 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
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index c58424f..56448ac 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -283,3 +283,4 @@ test('T15057', normal, compile, [''])
test('T15144', normal, compile, [''])
test('T15122', normal, compile, [''])
test('T13777', normal, compile, [''])
+test('T14164', normal, compile, [''])
More information about the ghc-commits
mailing list