content: {-
  (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
  