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

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
parent bc58d2e8
......@@ -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
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
f e | not_fixpoint = f (mapVarEnv (substTy subst) e)
| otherwise = subst
f env | not_fixpoint = f (mapVarEnv (substTy subst') env)
| otherwise = subst
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,
{-# 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)
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)’
......@@ -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, [''])
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