ghc-9.14.1: GHC/Tc/Instance/FunDeps.hs
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 2000
-}
{-# LANGUAGE DeriveFunctor #-}
-- | Functional dependencies
--
-- It's better to read it as: "if we know these, then we're going to know these"
module GHC.Tc.Instance.FunDeps
( FunDepEqn(..)
, pprEquation
, improveFromInstEnv
, improveFromAnother
, checkInstCoverage
, checkFunDeps
, pprFundeps
, instFD, closeWrtFunDeps
)
where
import GHC.Prelude
import GHC.Types.Var
import GHC.Core.Class
import GHC.Core.Predicate
import GHC.Core.Type
import GHC.Core.RoughMap( RoughMatchTc(..) )
import GHC.Core.Coercion.Axiom( TypeEqn )
import GHC.Core.Unify
import GHC.Core.InstEnv
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Compare( eqTypes, eqType )
import GHC.Tc.Errors.Types ( CoverageProblem(..), FailedCoverageCondition(..) )
import GHC.Tc.Types.Constraint ( isUnsatisfiableCt_maybe )
import GHC.Tc.Utils.TcType( transSuperClasses )
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Utils.Outputable
import GHC.Utils.FV
import GHC.Utils.Error( Validity'(..), allValid )
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.Pair ( Pair(..) )
import Data.List ( nubBy )
import Data.Maybe ( isJust, isNothing )
{-
************************************************************************
* *
\subsection{Generate equations from functional dependencies}
* *
************************************************************************
Each functional dependency with one variable in the RHS is responsible
for generating a single equality. For instance:
class C a b | a -> b
The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
will generate the following FunDepEqn
FDEqn { fd_qtvs = []
, fd_eqs = [Pair Bool alpha]
, fd_loc = ... }
However notice that a functional dependency may have more than one variable
in the RHS which will create more than one pair of types in fd_eqs. Example:
class C a b c | a -> b c
[Wanted] C Int alpha alpha
[Wanted] C Int Bool beta
Will generate:
FDEqn { fd_qtvs = []
, fd_eqs = [Pair Bool alpha, Pair alpha beta]
, fd_loc = ... }
INVARIANT: Corresponding types aren't already equal
That is, there exists at least one non-identity equality in FDEqs.
Note [Improving against instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Assume:
class C a b | a -> b
instance C Int Bool
[W] C Int ty
Then `improveFromInstEnv` should return a FDEqn with
FDEqn { fd_qtvs = [], fd_eqs = [Pair Bool ty] }
describing an equality (Bool ~ ty). To do this we /match/ the instance head
against the [W], using just the LHS of the fundep; if we match, we return
an equality for the RHS.
Wrinkles:
(1) meta_tvs: sometimes the instance mentions variables in the RHS that
are not bound in the LHS. For example
class C a b | a -> b
instance C Int (Maybe x)
[W] C Int ty
Note that although the `Int` parts match, that does not fix what `x` is.
So we just make up a fresh unification variable (a meta_tv), to give the
"shape" of the RHS. So we emit the FDEqun
FDEqn { fd_qtvs = [x], fd_eqs = [Pair (Maybe x) ty] }
Note that the fd_qtvs can be free in the /first/ component of the Pair,
but not in the second (which comes from the [W] constraint).
(2) Multi-range fundeps. When these meta_tvs are involved, there is a subtle
difference between the fundep (a -> b c) and the two fundeps (a->b, a->c).
Consider
class D a b c | a -> b c
instance D Int x (Maybe x)
[W] D Int Bool ty
Then we'll generate
FDEqn { fd_qtvs = [x0], fd_eqs = [ x0 ~ Bool, Maybe x0 ~ ty] }
which generates one fresh unification variable x0
But if the fundeps had been (a->b, a->c) we'd generate two FDEqns
FDEqn { fd_qtvs = [x1], fd_eqs = [ x1 ~ Bool ] }
FDEqn { fd_qtvs = [x2], fd_eqs = [ Maybe x2 ~ ty ] }
with two FDEqns, generating two separate unification variables.
(3) improveFromInstEnv doesn't return any equations that already hold.
Reason: then we know if any actual improvement has happened, in
which case we need to iterate the solver
-}
data FunDepEqn loc
= FDEqn { fd_qtvs :: [TyVar] -- Instantiate these type and kind vars
-- to fresh unification vars,
-- Non-empty only for FunDepEqns arising from instance decls
, fd_eqs :: [TypeEqn] -- Make these pairs of types equal
-- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be
-- free in ty1 but not in ty2. See Wrinkle (1) of
-- Note [Improving against instances]
, fd_loc :: loc }
deriving Functor
instance Outputable (FunDepEqn a) where
ppr = pprEquation
pprEquation :: FunDepEqn a -> SDoc
pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
= vcat [text "forall" <+> braces (pprWithCommas ppr qtvs),
nest 2 (vcat [ ppr t1 <+> text "~" <+> ppr t2
| Pair t1 t2 <- pairs])]
{-
Given a bunch of predicates that must hold, such as
C Int t1, C Int t2, C Bool t3, ?x::t4, ?x::t5
improve figures out what extra equations must hold.
For example, if we have
class C a b | a->b where ...
then improve will return
[(t1,t2), (t4,t5)]
NOTA BENE:
* improve does not iterate. It's possible that when we make
t1=t2, for example, that will in turn trigger a new equation.
This would happen if we also had
C t1 t7, C t2 t8
If t1=t2, we also get t7=t8.
improve does *not* do this extra step. It relies on the caller
doing so.
* The equations unify types that are not already equal. So there
is no effect iff the result of improve is empty
-}
instFD :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
-- (instFD fd tvs tys) returns fd instantiated with (tvs -> tys)
instFD (ls,rs) tvs tys
= (map lookup ls, map lookup rs)
where
env = zipVarEnv tvs tys
lookup tv = lookupVarEnv_NF env tv
zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
-> [Type] -> [Type]
-> [TypeEqn]
-- Create a list of (Type,Type) pairs from two lists of types,
-- making sure that the types are not already equal
zipAndComputeFDEqs discard (ty1:tys1) (ty2:tys2)
| discard ty1 ty2 = zipAndComputeFDEqs discard tys1 tys2
| otherwise = Pair ty1 ty2 : zipAndComputeFDEqs discard tys1 tys2
zipAndComputeFDEqs _ _ _ = []
-- Improve a class constraint from another class constraint
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
improveFromAnother :: loc
-> PredType -- Template item (usually given, or inert)
-> PredType -- Workitem [that can be improved]
-> [FunDepEqn loc]
-- Post: FDEqs always oriented from the other to the workitem
-- Equations have empty quantified variables
improveFromAnother loc pred1 pred2
| Just (cls1, tys1) <- getClassPredTys_maybe pred1
, Just (cls2, tys2) <- getClassPredTys_maybe pred2
, cls1 == cls2
= [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_loc = loc }
| let (cls_tvs, cls_fds) = classTvsFds cls1
, fd <- cls_fds
, let (ltys1, rs1) = instFD fd cls_tvs tys1
(ltys2, rs2) = instFD fd cls_tvs tys2
, eqTypes ltys1 ltys2 -- The LHSs match
, let eqs = zipAndComputeFDEqs eqType rs1 rs2
, not (null eqs) ]
improveFromAnother _ _ _ = []
-- Improve a class constraint from instance declarations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
improveFromInstEnv :: InstEnvs
-> (ClsInst -> loc)
-> Class -> [Type]
-> [FunDepEqn loc] -- Needs to be a FunDepEqn because
-- of quantified variables
-- See Note [Improving against instances]
-- Post: Equations oriented from the template (matching instance) to the workitem!
improveFromInstEnv inst_env mk_loc cls tys
= [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs, fd_loc = mk_loc ispec }
| fd <- cls_fds -- Iterate through the fundeps first,
-- because there often are none!
, let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
-- Trim the rough_tcs based on the head of the fundep.
-- Remember that instanceCantMatch treats both arguments
-- symmetrically, so it's ok to trim the rough_tcs,
-- rather than trimming each inst_tcs in turn
, ispec <- instances
, (meta_tvs, eqs) <- improveClsFD cls_tvs fd ispec
tys trimmed_tcs -- NB: orientation
]
where
(cls_tvs, cls_fds) = classTvsFds cls
instances = classInstances inst_env cls
rough_tcs = RM_KnownTc (className cls) : roughMatchTcs tys
improveClsFD :: [TyVar] -> FunDep TyVar -- One functional dependency from the class
-> ClsInst -- An instance template
-> [Type] -> [RoughMatchTc] -- Arguments of this (C tys) predicate
-> [([TyCoVar], [TypeEqn])] -- Empty or singleton
-- See Note [Improving against instances]
improveClsFD clas_tvs fd
(ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
tys_actual rough_tcs_actual
| instanceCantMatch rough_tcs_inst rough_tcs_actual
= [] -- Filter out ones that can't possibly match,
| otherwise
= assertPpr (equalLength tys_inst tys_actual &&
equalLength tys_inst clas_tvs)
(ppr tys_inst <+> ppr tys_actual) $
case tcMatchTyKisX init_subst ltys1 ltys2 of
Nothing -> []
Just subst | isJust (tcMatchTyKisX subst rtys1 rtys2)
-- Don't include any equations that already hold.
-- See Note [Improving against instances] wrinkle (3)
-- In making this check we must taking account of the fact that any
-- qtvs that aren't already instantiated can be instantiated to anything
-- at all
-- NB: We can't do this 'is-useful-equation' check element-wise
-- because of:
-- class C a b c | a -> b c
-- instance C Int x x
-- [Wanted] C Int alpha Int
-- We would get that x -> alpha (isJust) and x -> Int (isJust)
-- so we would produce no FDs, which is clearly wrong.
-> []
| null fdeqs
-> []
| otherwise
-> -- pprTrace "iproveClsFD" (vcat
-- [ text "is_tvs =" <+> ppr qtvs
-- , text "tys_inst =" <+> ppr tys_inst
-- , text "tys_actual =" <+> ppr tys_actual
-- , text "ltys1 =" <+> ppr ltys1
-- , text "ltys2 =" <+> ppr ltys2
-- , text "subst =" <+> ppr subst ]) $
[(meta_tvs, fdeqs)]
-- We could avoid this substTy stuff by producing the eqn
-- (qtvs, ls1++rs1, ls2++rs2)
-- which will re-do the ls1/ls2 unification when the equation is
-- executed. What we're doing instead is recording the partial
-- work of the ls1/ls2 unification leaving a smaller unification problem
where
rtys1' = map (substTy subst) rtys1
fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2
-- Don't discard anything!
-- We could discard equal types but it's an overkill to call
-- eqType again, since we know for sure that /at least one/
-- equation in there is useful)
meta_tvs = [ setVarType tv (substTy subst (varType tv))
| tv <- qtvs
, tv `notElemSubst` subst
, tv `elemVarSet` rtys1_tvs ]
-- meta_tvs are the quantified type variables
-- that have not been substituted out
--
-- Eg. class C a b | a -> b
-- instance C Int [y]
-- Given constraint C Int z
-- we generate the equation
-- ({y}, [y], z)
--
-- But note (a) we get them from the dfun_id, so they are *in order*
-- because the kind variables may be mentioned in the
-- type variables' kinds
-- (b) we must apply 'subst' to the kinds, in case we have
-- matched out a kind variable, but not a type variable
-- whose kind mentions that kind variable! #6015, #6068
-- (c) no need to include tyvars not in rtys1
where
init_subst = mkEmptySubst $ mkInScopeSet $
mkVarSet qtvs `unionVarSet` tyCoVarsOfTypes ltys2
(ltys1, rtys1) = instFD fd clas_tvs tys_inst
(ltys2, rtys2) = instFD fd clas_tvs tys_actual
rtys1_tvs = tyCoVarsOfTypes rtys1
{-
%************************************************************************
%* *
The Coverage condition for instance declarations
* *
************************************************************************
Note [Coverage condition]
~~~~~~~~~~~~~~~~~~~~~~~~~
Example
class C a b | a -> b
instance theta => C t1 t2
For the coverage condition, we check
(normal) fv(t2) `subset` fv(t1)
(liberal) fv(t2) `subset` closeWrtFunDeps(fv(t1), theta)
The liberal version ensures the self-consistency of the instance, but
it does not guarantee termination. Example:
class Mul a b c | a b -> c where
(.*.) :: a -> b -> c
instance Mul Int Int Int where (.*.) = (*)
instance Mul Int Float Float where x .*. y = fromIntegral x * y
instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v
In the third instance, it's not the case that fv([c]) `subset` fv(a,[b]).
But it is the case that fv([c]) `subset` closeWrtFunDeps( theta, fv(a,[b]) )
But it is a mistake to accept the instance because then this defn:
f = \ b x y -> if b then x .*. [y] else y
makes instance inference go into a loop, because it requires the constraint
Mul a [b] b
-}
checkInstCoverage :: Bool -- Be liberal
-> Class -> [PredType] -> [Type]
-> Validity' CoverageProblem
-- "be_liberal" flag says whether to use "liberal" coverage of
-- See Note [Coverage condition] below
--
-- Return values
-- Nothing => no problems
-- Just msg => coverage problem described by msg
checkInstCoverage be_liberal clas theta inst_taus
| any (isJust . isUnsatisfiableCt_maybe) theta
-- As per [GHC proposal #433](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst),
-- we skip checking the coverage condition if there is an "Unsatisfiable"
-- constraint in the instance context.
--
-- See Note [Implementation of Unsatisfiable constraints] in GHC.Tc.Errors,
-- point (E).
= IsValid
| otherwise
= allValid (map fundep_ok fds)
where
(tyvars, fds) = classTvsFds clas
fundep_ok fd
| all isEmptyVarSet undetermined_tvs
= IsValid
| otherwise
= NotValid not_covered_msg
where
(ls,rs) = instFD fd tyvars inst_taus
ls_tvs = tyCoVarsOfTypes ls
rs_tvs = visVarsOfTypes rs
undetermined_tvs | be_liberal = liberal_undet_tvs
| otherwise = conserv_undet_tvs
closed_ls_tvs = closeWrtFunDeps theta ls_tvs
liberal_undet_tvs = (`minusVarSet` closed_ls_tvs) <$> rs_tvs
conserv_undet_tvs = (`minusVarSet` ls_tvs) <$> rs_tvs
not_covered_msg =
CoverageProblem
{ not_covered_fundep = fd
, not_covered_fundep_inst = (ls, rs)
, not_covered_invis_vis_tvs = undetermined_tvs
, not_covered_liberal =
if be_liberal
then FailedLICC
else FailedICC
{ alsoFailedLICC = not $ all isEmptyVarSet liberal_undet_tvs }
}
{- Note [Closing over kinds in coverage]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have a fundep (a::k) -> b
Then if 'a' is instantiated to (x y), where x:k2->*, y:k2,
then fixing x really fixes k2 as well, and so k2 should be added to
the lhs tyvars in the fundep check.
Example (#8391), using liberal coverage
data Foo a = ... -- Foo :: forall k. k -> *
class Bar a b | a -> b
instance Bar a (Foo a)
In the instance decl, (a:k) does fix (Foo k a), but only if we notice
that (a:k) fixes k. #10109 is another example.
Here is a more subtle example, from HList-0.4.0.0 (#10564)
class HasFieldM (l :: k) r (v :: Maybe *)
| l r -> v where ...
class HasFieldM1 (b :: Maybe [*]) (l :: k) r v
| b l r -> v where ...
class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k])
| e1 l -> r
data Label :: k -> *
type family LabelsOf (a :: [*]) :: *
instance (HMemberM (Label {k} (l::k)) (LabelsOf xs) b,
HasFieldM1 b l (r xs) v)
=> HasFieldM l (r xs) v where
Is the instance OK? Does {l,r,xs} determine v? Well:
* From the instance constraint HMemberM (Label k l) (LabelsOf xs) b,
plus the fundep "| el l -> r" in class HMameberM,
we get {l,k,xs} -> b
* Note the 'k'!! We must call closeOverKinds on the seed set
ls_tvs = {l,r,xs}, BEFORE doing closeWrtFunDeps, else the {l,k,xs}->b
fundep won't fire. This was the reason for #10564.
* So starting from seeds {l,r,xs,k} we do closeWrtFunDeps to get
first {l,r,xs,k,b}, via the HMemberM constraint, and then
{l,r,xs,k,b,v}, via the HasFieldM1 constraint.
* And that fixes v.
However, we must closeOverKinds whenever augmenting the seed set
in closeWrtFunDeps! Consider #10109:
data Succ a -- Succ :: forall k. k -> *
class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab
instance (Add a b ab) => Add (Succ {k1} (a :: k1))
b
(Succ {k3} (ab :: k3})
We start with seed set {a:k1,b:k2} and closeOverKinds to {a,k1,b,k2}.
Now use the fundep to extend to {a,k1,b,k2,ab}. But we need to
closeOverKinds *again* now to {a,k1,b,k2,ab,k3}, so that we fix all
the variables free in (Succ {k3} ab).
Bottom line:
* closeOverKinds on initial seeds (done automatically
by tyCoVarsOfTypes in checkInstCoverage)
* and closeOverKinds whenever extending those seeds (in closeWrtFunDeps)
Note [The liberal coverage condition]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(closeWrtFunDeps preds tvs) closes the set of type variables tvs,
wrt functional dependencies in preds. The result is a superset
of the argument set. For example, if we have
class C a b | a->b where ...
then
closeWrtFunDeps [C (x,y) z, C (x,p) q] {x,y} = {x,y,z}
because if we know x and y then that fixes z.
We also use equality predicates in the predicates; if we have an
assumption `t1 ~ t2`, then we use the fact that if we know `t1` we
also know `t2` and the other way.
eg closeWrtFunDeps [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
closeWrtFunDeps is used
- when checking the coverage condition for an instance declaration
- when determining which tyvars are unquantifiable during generalization, in
GHC.Tc.Solver.decidePromotedTyVars.
Note [Equality superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
class (a ~ [b]) => C a b
Remember from Note [The equality types story] in GHC.Builtin.Types.Prim, that
* (a ~~ b) is a superclass of (a ~ b)
* (a ~# b) is a superclass of (a ~~ b)
So when closeWrtFunDeps expands superclasses we'll get a (a ~# [b]) superclass.
But that's an EqPred not a ClassPred, and we jolly well do want to
account for the mutual functional dependencies implied by (t1 ~# t2).
Hence the EqPred handling in closeWrtFunDeps. See #10778.
Note [Care with type functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#12803)
class C x y | x -> y
type family F a b
type family G c d = r | r -> d
Now consider
closeWrtFunDeps (C (F a b) (G c d)) {a,b}
Knowing {a,b} fixes (F a b) regardless of the injectivity of F.
But knowing (G c d) fixes only {d}, because G is only injective
in its second parameter.
Hence the tyCoVarsOfTypes/injTyVarsOfTypes dance in tv_fds.
-}
closeWrtFunDeps :: [PredType] -> TyCoVarSet -> TyCoVarSet
-- See Note [The liberal coverage condition]
closeWrtFunDeps preds fixed_tvs
| null tv_fds = fixed_tvs -- Fast escape hatch for common case.
| otherwise = assertPpr (closeOverKinds fixed_tvs == fixed_tvs)
(vcat [ text "closeWrtFunDeps: fixed_tvs is not closed over kinds"
, text "fixed_tvs:" <+> ppr fixed_tvs
, text "closure:" <+> ppr (closeOverKinds fixed_tvs) ])
$ fixVarSet extend fixed_tvs
where
extend fixed_tvs = foldl' add fixed_tvs tv_fds
where
add fixed_tvs (ls,rs)
| ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` closeOverKinds rs
| otherwise = fixed_tvs
-- closeOverKinds: see Note [Closing over kinds in coverage]
tv_fds :: [(TyCoVarSet,TyCoVarSet)]
tv_fds = [ (tyCoVarsOfTypes ls, fvVarSet $ injectiveVarsOfTypes True rs)
-- See Note [Care with type functions]
| pred <- preds
, pred' <- pred : transSuperClasses pred
-- Look for fundeps in superclasses too
, (ls, rs) <- determined pred' ]
determined :: PredType -> [([Type],[Type])]
determined pred
= case classifyPredType pred of
EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
-- See Note [Equality superclasses]
ClassPred cls tys | not (isIPClass cls)
-- isIPClass: see Note [closeWrtFunDeps ignores implicit parameters]
-> [ instFD fd cls_tvs tys
| let (cls_tvs, cls_fds) = classTvsFds cls
, fd <- cls_fds ]
_ -> []
{- Note [closeWrtFunDeps ignores implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Implicit params don't really determine a type variable (that is, we might have
IP "c" Bool and IP "c" Int in different places within the same program), and
skipping this causes implicit params to monomorphise too many variables; see
Note [Inheriting implicit parameters] in GHC.Tc.Solver. Skipping causes
typecheck/should_compile/tc219 to fail.
-}
{- *********************************************************************
* *
Check that a new instance decl is OK wrt fundeps
* *
************************************************************************
Here is the bad case:
class C a b | a->b where ...
instance C Int Bool where ...
instance C Int Char where ...
The point is that a->b, so Int in the first parameter must uniquely
determine the second. In general, given the same class decl, and given
instance C s1 s2 where ...
instance C t1 t2 where ...
Then the criterion is: if U=unify(s1,t1) then U(s2) = U(t2).
Matters are a little more complicated if there are free variables in
the s2/t2.
class D a b c | a -> b
instance D a b => D [(a,a)] [b] Int
instance D a b => D [a] [b] Bool
The instance decls don't overlap, because the third parameter keeps
them separate. But we want to make sure that given any constraint
D s1 s2 s3
if s1 matches
Note [Bogus consistency check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In checkFunDeps we check that a new ClsInst is consistent with all the
ClsInsts in the environment.
The bogus aspect is discussed in #10675. Currently it if the two
types are *contradictory*, using (isNothing . tcUnifyTys). But all
the papers say we should check if the two types are *equal* thus
not (substTys subst rtys1 `eqTypes` substTys subst rtys2)
For now I'm leaving the bogus form because that's the way it has
been for years.
-}
checkFunDeps :: InstEnvs -> ClsInst -> [ClsInst]
-- The Consistency Check.
-- Check whether adding DFunId would break functional-dependency constraints
-- Used only for instance decls defined in the module being compiled
-- Returns a list of the ClsInst in InstEnvs that are inconsistent
-- with the proposed new ClsInst
checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
, is_tys = tys1, is_tcs = rough_tcs1 })
| null fds
= []
| otherwise
= nubBy eq_inst $
[ ispec | ispec <- cls_insts
, fd <- fds
, is_inconsistent fd ispec ]
where
cls_insts = classInstances inst_envs cls
(cls_tvs, fds) = classTvsFds cls
qtv_set1 = mkVarSet qtvs1
is_inconsistent fd (ClsInst { is_tvs = qtvs2, is_tys = tys2, is_tcs = rough_tcs2 })
| instanceCantMatch trimmed_tcs rough_tcs2
= False
| otherwise
= case tcUnifyFunDeps qtvs ltys1 ltys2 of
Nothing -> False
Just subst
-> isNothing $ -- Bogus legacy test (#10675)
-- See Note [Bogus consistency check]
tcUnifyFunDeps qtvs (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
where
trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs1
(ltys1, rtys1) = instFD fd cls_tvs tys1
(ltys2, rtys2) = instFD fd cls_tvs tys2
qtv_set2 = mkVarSet qtvs2
qtvs = qtv_set1 `unionVarSet` qtv_set2
eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
-- A single instance may appear twice in the un-nubbed conflict list
-- because it may conflict with more than one fundep. E.g.
-- class C a b c | a -> b, a -> c
-- instance C Int Bool Bool
-- instance C Int Char Char
-- The second instance conflicts with the first by *both* fundeps
trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [RoughMatchTc] -> [RoughMatchTc]
-- Computing rough_tcs for a particular fundep
-- class C a b c | a -> b where ...
-- For each instance .... => C ta tb tc
-- we want to match only on the type ta; so our
-- rough-match thing must similarly be filtered.
-- Hence, we Nothing-ise the tb and tc types right here
--
-- Result list is same length as input list, just with more Nothings
trimRoughMatchTcs _clas_tvs _ [] = panic "trimRoughMatchTcs: nullary [RoughMatchTc]"
trimRoughMatchTcs clas_tvs (ltvs, _) (cls:mb_tcs)
= cls : zipWith select clas_tvs mb_tcs
where
select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
| otherwise = RM_WildCard