Fix an infinite loop in niFixTCvSubst
authorSimon Peyton Jones <simonpj@microsoft.com>
Sat, 16 Jun 2018 22:25:53 +0000 (23:25 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 18 Jun 2018 07:23:16 +0000 (08:23 +0100)
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]

compiler/types/Unify.hs
testsuite/tests/indexed-types/should_compile/T14164.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T

index 9833f8e..8f69172 100644 (file)
@@ -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 (file)
index 0000000..1cf6f2d
--- /dev/null
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilyDependencies #-}\r
+{-# LANGUAGE TypeInType #-}\r
+{-# LANGUAGE TypeOperators #-}\r
+module T14164 where\r
+\r
+data G (x :: a) = GNil | GCons (G x)\r
+\r
+type family F (xs :: [a]) (g :: G (z :: a)) = (res :: [a]) | res -> a where\r
+  F (x:xs) GNil         = x:xs\r
+  F (x:xs) (GCons rest) = x:F xs rest\r
index c58424f..56448ac 100644 (file)
@@ -283,3 +283,4 @@ test('T15057', normal, compile, [''])
 test('T15144', normal, compile, [''])
 test('T15122', normal, compile, [''])
 test('T13777', normal, compile, [''])
+test('T14164', normal, compile, [''])