[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/indexedtypes/should_compile/T14164.hs  10 ++
testsuite/tests/indexedtypes/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 nonidempotent 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 illformed 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 toposort to put them in dependency order:
+ [ b :: *, z :: a, rest :: G a z ]
+
+ 6. Apply the substitution lefttoright 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
+inscope set, because all of those variables appear in the
+range of the substitution, so they must all be in the inscope
+set. But NB that the type substitution engine does not look up
+variables in the inscope set; it is used only to ensure no
+shadowing.
}
niFixTCvSubst :: TvSubstEnv > TCvSubst
 Find the idempotent fixed point of the nonidempotent 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 nonidempotent substitution to a set of type variables,
diff git a/testsuite/tests/indexedtypes/should_compile/T14164.hs b/testsuite/tests/indexedtypes/should_compile/T14164.hs
new file mode 100644
index 0000000..1cf6f2d
 /dev/null
+++ b/testsuite/tests/indexedtypes/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/indexedtypes/should_compile/all.T b/testsuite/tests/indexedtypes/should_compile/all.T
index c58424f..56448ac 100644
 a/testsuite/tests/indexedtypes/should_compile/all.T
+++ b/testsuite/tests/indexedtypes/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 ghccommits
mailing list