summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Instance/FunDeps.hs
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc/Instance/FunDeps.hs')
-rw-r--r--compiler/GHC/Tc/Instance/FunDeps.hs682
1 files changed, 682 insertions, 0 deletions
diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
new file mode 100644
index 0000000000..73a1317692
--- /dev/null
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -0,0 +1,682 @@
+{-
+(c) The University of Glasgow 2006
+(c) The GRASP/AQUA Project, Glasgow University, 2000
+
+
+-}
+
+{-# LANGUAGE CPP #-}
+
+-- | 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
+ )
+where
+
+#include "HsVersions.h"
+
+import GhcPrelude
+
+import GHC.Types.Name
+import GHC.Types.Var
+import GHC.Core.Class
+import GHC.Core.Predicate
+import GHC.Core.Type
+import GHC.Tc.Utils.TcType( transSuperClasses )
+import GHC.Core.Coercion.Axiom( TypeEqn )
+import GHC.Core.Unify
+import GHC.Core.InstEnv
+import GHC.Types.Var.Set
+import GHC.Types.Var.Env
+import GHC.Core.TyCo.FVs
+import GHC.Core.TyCo.Ppr( pprWithExplicitKindsWhen )
+import FV
+import Outputable
+import ErrUtils( Validity(..), allValid )
+import GHC.Types.SrcLoc
+import Util
+
+import Pair ( Pair(..) )
+import Data.List ( nubBy )
+import Data.Maybe
+import Data.Foldable ( fold )
+
+{-
+************************************************************************
+* *
+\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_pred1 = C Int Bool
+ , fd_pred2 = C Int 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_pred1 = C Int Bool
+ , fd_pred2 = C Int alpha
+ , fd_loc = ... }
+
+INVARIANT: Corresponding types aren't already equal
+That is, there exists at least one non-identity equality in FDEqs.
+
+Assume:
+ class C a b c | a -> b c
+ instance C Int x x
+And: [Wanted] C Int Bool alpha
+We will /match/ the LHS of fundep equations, producing a matching substitution
+and create equations for the RHS sides. In our last example we'd have generated:
+ ({x}, [fd1,fd2])
+where
+ fd1 = FDEq 1 Bool x
+ fd2 = FDEq 2 alpha x
+To ``execute'' the equation, make fresh type variable for each tyvar in the set,
+instantiate the two types with these fresh variables, and then unify or generate
+a new constraint. In the above example we would generate a new unification
+variable 'beta' for x and produce the following constraints:
+ [Wanted] (Bool ~ beta)
+ [Wanted] (alpha ~ beta)
+
+Notice the subtle difference between the above class declaration and:
+ class C a b c | a -> b, a -> c
+where we would generate:
+ ({x},[fd1]),({x},[fd2])
+This means that the template variable would be instantiated to different
+unification variables when producing the FD constraints.
+
+Finally, the position parameters will help us rewrite the wanted constraint ``on the spot''
+-}
+
+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
+ , fd_pred1 :: PredType -- The FunDepEqn arose from
+ , fd_pred2 :: PredType -- combining these two constraints
+ , fd_loc :: loc }
+
+{-
+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_pred1 = pred1, fd_pred2 = pred2, 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
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+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])]
+
+improveFromInstEnv :: InstEnvs
+ -> (PredType -> SrcSpan -> loc)
+ -> PredType
+ -> [FunDepEqn loc] -- Needs to be a FunDepEqn because
+ -- of quantified variables
+-- Post: Equations oriented from the template (matching instance) to the workitem!
+improveFromInstEnv inst_env mk_loc pred
+ | Just (cls, tys) <- ASSERT2( isClassPred pred, ppr pred )
+ getClassPredTys_maybe pred
+ , let (cls_tvs, cls_fds) = classTvsFds cls
+ instances = classInstances inst_env cls
+ rough_tcs = roughMatchTcs tys
+ = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs
+ , fd_pred1 = p_inst, fd_pred2 = pred
+ , fd_loc = mk_loc p_inst (getSrcSpan (is_dfun 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
+ , let p_inst = mkClassPred cls (is_tys ispec)
+ ]
+improveFromInstEnv _ _ _ = []
+
+
+improveClsFD :: [TyVar] -> FunDep TyVar -- One functional dependency from the class
+ -> ClsInst -- An instance template
+ -> [Type] -> [Maybe Name] -- Arguments of this (C tys) predicate
+ -> [([TyCoVar], [TypeEqn])] -- Empty or singleton
+
+improveClsFD clas_tvs fd
+ (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
+ tys_actual rough_tcs_actual
+
+-- Compare instance {a,b} C sx sp sy sq
+-- with wanted [W] C tx tp ty tq
+-- for fundep (x,y -> p,q) from class (C x p y q)
+-- If (sx,sy) unifies with (tx,ty), take the subst S
+
+-- 'qtvs' are the quantified type variables, the ones which can be instantiated
+-- to make the types match. For example, given
+-- class C a b | a->b where ...
+-- instance C (Maybe x) (Tree x) where ..
+--
+-- and a wanted constraint of form (C (Maybe t1) t2),
+-- then we will call checkClsFD with
+--
+-- is_qtvs = {x}, is_tys = [Maybe x, Tree x]
+-- tys_actual = [Maybe t1, t2]
+--
+-- We can instantiate x to t1, and then we want to force
+-- (Tree x) [t1/x] ~ t2
+
+ | instanceCantMatch rough_tcs_inst rough_tcs_actual
+ = [] -- Filter out ones that can't possibly match,
+
+ | otherwise
+ = ASSERT2( equalLength tys_inst tys_actual &&
+ equalLength tys_inst clas_tvs
+ , ppr tys_inst <+> ppr tys_actual )
+
+ case tcMatchTyKis ltys1 ltys2 of
+ Nothing -> []
+ Just subst | isJust (tcMatchTyKisX subst rtys1 rtys2)
+ -- Don't include any equations that already hold.
+ -- Reason: then we know if any actual improvement has happened,
+ -- in which case we need to iterate the solver
+ -- 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 (substTyUnchecked 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 (substTyUnchecked subst (varType tv))
+ | tv <- qtvs, tv `notElemTCvSubst` subst ]
+ -- 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
+ where
+ (ltys1, rtys1) = instFD fd clas_tvs tys_inst
+ (ltys2, rtys2) = instFD fd clas_tvs tys_actual
+
+{-
+%************************************************************************
+%* *
+ 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` oclose(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` oclose( 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
+-- "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
+ = allValid (map fundep_ok fds)
+ where
+ (tyvars, fds) = classTvsFds clas
+ fundep_ok fd
+ | and (isEmptyVarSet <$> undetermined_tvs) = IsValid
+ | otherwise = NotValid msg
+ where
+ (ls,rs) = instFD fd tyvars inst_taus
+ ls_tvs = tyCoVarsOfTypes ls
+ rs_tvs = splitVisVarsOfTypes rs
+
+ undetermined_tvs | be_liberal = liberal_undet_tvs
+ | otherwise = conserv_undet_tvs
+
+ closed_ls_tvs = oclose theta ls_tvs
+ liberal_undet_tvs = (`minusVarSet` closed_ls_tvs) <$> rs_tvs
+ conserv_undet_tvs = (`minusVarSet` ls_tvs) <$> rs_tvs
+
+ undet_set = fold undetermined_tvs
+
+ msg = pprWithExplicitKindsWhen
+ (isEmptyVarSet $ pSnd undetermined_tvs) $
+ vcat [ -- text "ls_tvs" <+> ppr ls_tvs
+ -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
+ -- , text "theta" <+> ppr theta
+ -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
+ -- , text "rs_tvs" <+> ppr rs_tvs
+ sep [ text "The"
+ <+> ppWhen be_liberal (text "liberal")
+ <+> text "coverage condition fails in class"
+ <+> quotes (ppr clas)
+ , nest 2 $ text "for functional dependency:"
+ <+> quotes (pprFunDep fd) ]
+ , sep [ text "Reason: lhs type"<>plural ls <+> pprQuotedList ls
+ , nest 2 $
+ (if isSingleton ls
+ then text "does not"
+ else text "do not jointly")
+ <+> text "determine rhs type"<>plural rs
+ <+> pprQuotedList rs ]
+ , text "Un-determined variable" <> pluralVarSet undet_set <> colon
+ <+> pprVarSet undet_set (pprWithCommas ppr)
+ , ppWhen (not be_liberal &&
+ and (isEmptyVarSet <$> liberal_undet_tvs)) $
+ text "Using UndecidableInstances might help" ]
+
+{- 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 oclose, 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 oclose 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 oclose! 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 oclose)
+
+Note [The liberal coverage condition]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(oclose 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
+ oclose [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 oclose [C (x,y) z, a ~ x] {a,y} = {a,y,z,x}
+
+oclose is used (only) when checking the coverage condition for
+an instance declaration
+
+Note [Equality superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+ class (a ~ [b]) => C a b
+
+Remember from Note [The equality types story] in TysPrim, that
+ * (a ~~ b) is a superclass of (a ~ b)
+ * (a ~# b) is a superclass of (a ~~ b)
+
+So when oclose 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 oclose. 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
+ oclose (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.
+-}
+
+oclose :: [PredType] -> TyCoVarSet -> TyCoVarSet
+-- See Note [The liberal coverage condition]
+oclose preds fixed_tvs
+ | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
+ | otherwise = 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 -> [ instFD fd cls_tvs tys
+ | let (cls_tvs, cls_fds) = classTvsFds cls
+ , fd <- cls_fds ]
+ _ -> []
+
+
+{- *********************************************************************
+* *
+ 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 *contradicatory*, 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 tcUnifyTyKis bind_fn ltys1 ltys2 of
+ Nothing -> False
+ Just subst
+ -> isNothing $ -- Bogus legacy test (#10675)
+ -- See Note [Bogus consistency check]
+ tcUnifyTyKis bind_fn (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
+ bind_fn tv | tv `elemVarSet` qtv_set1 = BindMe
+ | tv `elemVarSet` qtv_set2 = BindMe
+ | otherwise = Skolem
+
+ 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 -> [Maybe Name] -> [Maybe Name]
+-- 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 (ltvs, _) mb_tcs
+ = zipWith select clas_tvs mb_tcs
+ where
+ select clas_tv mb_tc | clas_tv `elem` ltvs = mb_tc
+ | otherwise = Nothing