[commit: ghc] master: Make the unifier a fixpoint even for the free kind vars of a tyvar (d8d9711)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/d8d97113c24e7216be36c9cdfc58e91f26528f06/ghc

>---------------------------------------------------------------

commit d8d97113c24e7216be36c9cdfc58e91f26528f06
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri May 23 07:47:17 2014 +0100

    Make the unifier a fixpoint even for the free kind vars of a tyvar
    
    The (pure) unifier tcUnifyTys returns an idempotent substitution.
    But previously the kinds of type variables free in the range of
    the subst could have un-substituted kind variables.
    
    This patch fixes that, fixing Trac #9106.
    
    See Note [Finding the substitution fixpoint] in Unify


>---------------------------------------------------------------

d8d97113c24e7216be36c9cdfc58e91f26528f06
 compiler/types/Unify.lhs               | 46 ++++++++++++++++++++++++++++------
 testsuite/tests/polykinds/T9106.hs     | 14 +++++++++++
 testsuite/tests/polykinds/T9106.stderr |  8 ++++++
 testsuite/tests/polykinds/all.T        |  1 +
 4 files changed, 62 insertions(+), 7 deletions(-)

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 1ce1d62..24aa7a7 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -24,7 +24,6 @@ module Unify (
 
         -- Side-effect free unification
         tcUnifyTy, tcUnifyTys, BindFlag(..),
-        niFixTvSubst, niSubstTvSet,
 
         UnifyResultM(..), UnifyResult, tcUnifyTysFG
 
@@ -471,19 +470,52 @@ During unification we use a TvSubstEnv that is
   (a) non-idempotent
   (b) loop-free; ie repeatedly applying it yields a fixed point
 
+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
+   T k (H k (f:k)) ~ T * (g:*)
+If we unify, we get the substitution
+   [ k -> *
+   , g -> H k (f:k) ]
+To make it idempotent we don't want to get just
+   [ k -> *
+   , g -> H * (f:k) ]
+We also want to substitute inside f's kind, to get
+   [ k -> *
+   , g -> H k (f:*) ]
+If we don't do this, we may apply the substitition 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
+
 \begin{code}
 niFixTvSubst :: TvSubstEnv -> TvSubst
 -- Find the idempotent fixed point of the non-idempotent substitution
+-- See Note [Finding the substitution fixpoint]
 -- ToDo: use laziness instead of iteration?
 niFixTvSubst env = f env
   where
-    f e | not_fixpoint = f (mapVarEnv (substTy subst) e)
-        | otherwise    = subst
+    f env | not_fixpoint = f (mapVarEnv (substTy subst') env)
+          | otherwise    = subst
         where
-          range_tvs    = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet e
-          subst        = mkTvSubst (mkInScopeSet range_tvs) e 
-          not_fixpoint = foldVarSet ((||) . in_domain) False range_tvs
-          in_domain tv = tv `elemVarEnv` e
+          not_fixpoint  = foldVarSet ((||) . in_domain) False all_range_tvs
+          in_domain tv  = tv `elemVarEnv` env
+
+          range_tvs     = foldVarEnv (unionVarSet . tyVarsOfType) emptyVarSet env
+          all_range_tvs = closeOverKinds range_tvs
+          subst         = mkTvSubst (mkInScopeSet all_range_tvs) env
+
+             -- env' extends env by replacing any free type with 
+             -- that same tyvar with a substituted kind
+             -- See note [Finding the substitution fixpoint]
+          env'          = extendVarEnvList env [ (rtv, mkTyVarTy $ setTyVarKind rtv $
+                                                       substTy subst $ tyVarKind rtv)
+                                               | rtv <- varSetElems range_tvs
+                                               , not (in_domain rtv) ]
+          subst'        = mkTvSubst (mkInScopeSet all_range_tvs) env'
 
 niSubstTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
 -- Apply the non-idempotent substitution to a set of type variables,
diff --git a/testsuite/tests/polykinds/T9106.hs b/testsuite/tests/polykinds/T9106.hs
new file mode 100644
index 0000000..eaf0364
--- /dev/null
+++ b/testsuite/tests/polykinds/T9106.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE MultiParamTypeClasses, DataKinds, FunctionalDependencies,
+   KindSignatures, PolyKinds, FlexibleInstances, FlexibleContexts,
+   UndecidableInstances #-}
+
+module T9106 where
+
+import GHC.TypeLits
+
+class FunctorN (n :: Nat) f (a :: *) (fa :: *) | n f a -> fa where
+
+instance FunctorN 0 f a a where
+
+instance FunctorN n f a (f fa)
+
diff --git a/testsuite/tests/polykinds/T9106.stderr b/testsuite/tests/polykinds/T9106.stderr
new file mode 100644
index 0000000..0b239f2
--- /dev/null
+++ b/testsuite/tests/polykinds/T9106.stderr
@@ -0,0 +1,8 @@
+
+T9106.hs:13:10:
+    Illegal instance declaration for ‘FunctorN n f a (f fa)’
+      The liberal coverage condition fails in class ‘FunctorN’
+        for functional dependency: ‘n f a -> fa’
+      Reason: lhs types ‘n’, ‘f’, ‘a’
+        do not jointly determine rhs type ‘f fa’
+    In the instance declaration for ‘FunctorN n f a (f fa)’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 3634d83..96faa67 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -100,3 +100,4 @@ test('T8566a', expect_broken(8566), compile,[''])
 test('T7481', normal, compile_fail,[''])
 test('T8705', normal, compile, [''])
 test('T8985', normal, compile, [''])
+test('T9106', normal, compile_fail, [''])