{-
(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.Name
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.Types.SrcLoc

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_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.

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 (Int ~ 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 seconde (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 { forall loc. FunDepEqn loc -> [TyVar]
fd_qtvs :: [TyVar]   -- Instantiate these type and kind vars
                                 --   to fresh unification vars,
                                 -- Non-empty only for FunDepEqns arising from instance decls

          , forall loc. FunDepEqn loc -> [TypeEqn]
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]

          , forall loc. FunDepEqn loc -> Type
fd_pred1 :: PredType   -- The FunDepEqn arose from
          , forall loc. FunDepEqn loc -> Type
fd_pred2 :: PredType   --  combining these two constraints
          , forall loc. FunDepEqn loc -> loc
fd_loc   :: loc  }
    deriving (forall a b. (a -> b) -> FunDepEqn a -> FunDepEqn b)
-> (forall a b. a -> FunDepEqn b -> FunDepEqn a)
-> Functor FunDepEqn
forall a b. a -> FunDepEqn b -> FunDepEqn a
forall a b. (a -> b) -> FunDepEqn a -> FunDepEqn b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> FunDepEqn a -> FunDepEqn b
fmap :: forall a b. (a -> b) -> FunDepEqn a -> FunDepEqn b
$c<$ :: forall a b. a -> FunDepEqn b -> FunDepEqn a
<$ :: forall a b. a -> FunDepEqn b -> FunDepEqn a
Functor

instance Outputable (FunDepEqn a) where
  ppr :: FunDepEqn a -> SDoc
ppr = FunDepEqn a -> SDoc
forall a. FunDepEqn a -> SDoc
pprEquation

pprEquation :: FunDepEqn a -> SDoc
pprEquation :: forall a. FunDepEqn a -> SDoc
pprEquation (FDEqn { fd_qtvs :: forall loc. FunDepEqn loc -> [TyVar]
fd_qtvs = [TyVar]
qtvs, fd_eqs :: forall loc. FunDepEqn loc -> [TypeEqn]
fd_eqs = [TypeEqn]
pairs })
  = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"forall" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces ((TyVar -> SDoc) -> [TyVar] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
qtvs),
          Int -> SDoc -> SDoc
nest Int
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t1 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"~" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t2
                       | Pair Type
t1 Type
t2 <- [TypeEqn]
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 :: FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD ([TyVar]
ls,[TyVar]
rs) [TyVar]
tvs [Type]
tys
  = ((TyVar -> Type) -> [TyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Type
lookup [TyVar]
ls, (TyVar -> Type) -> [TyVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> Type
lookup [TyVar]
rs)
  where
    env :: VarEnv Type
env       = [TyVar] -> [Type] -> VarEnv Type
forall a. [TyVar] -> [a] -> VarEnv a
zipVarEnv [TyVar]
tvs [Type]
tys
    lookup :: TyVar -> Type
lookup TyVar
tv = VarEnv Type -> TyVar -> Type
forall a. VarEnv a -> TyVar -> a
lookupVarEnv_NF VarEnv Type
env TyVar
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 :: (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs Type -> Type -> Bool
discard (Type
ty1:[Type]
tys1) (Type
ty2:[Type]
tys2)
 | Type -> Type -> Bool
discard Type
ty1 Type
ty2 = (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs Type -> Type -> Bool
discard [Type]
tys1 [Type]
tys2
 | Bool
otherwise       = Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair Type
ty1 Type
ty2 TypeEqn -> [TypeEqn] -> [TypeEqn]
forall a. a -> [a] -> [a]
: (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs Type -> Type -> Bool
discard [Type]
tys1 [Type]
tys2
zipAndComputeFDEqs Type -> Type -> Bool
_ [Type]
_ [Type]
_ = []

-- 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 :: forall loc. loc -> Type -> Type -> [FunDepEqn loc]
improveFromAnother loc
loc Type
pred1 Type
pred2
  | Just (Class
cls1, [Type]
tys1) <- Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred1
  , Just (Class
cls2, [Type]
tys2) <- Type -> Maybe (Class, [Type])
getClassPredTys_maybe Type
pred2
  , Class
cls1 Class -> Class -> Bool
forall a. Eq a => a -> a -> Bool
== Class
cls2
  = [ FDEqn { fd_qtvs :: [TyVar]
fd_qtvs = [], fd_eqs :: [TypeEqn]
fd_eqs = [TypeEqn]
eqs, fd_pred1 :: Type
fd_pred1 = Type
pred1, fd_pred2 :: Type
fd_pred2 = Type
pred2, fd_loc :: loc
fd_loc = loc
loc }
    | let ([TyVar]
cls_tvs, [FunDep TyVar]
cls_fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
cls1
    , FunDep TyVar
fd <- [FunDep TyVar]
cls_fds
    , let ([Type]
ltys1, [Type]
rs1) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys1
          ([Type]
ltys2, [Type]
rs2) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys2
    , [Type] -> [Type] -> Bool
eqTypes [Type]
ltys1 [Type]
ltys2               -- The LHSs match
    , let eqs :: [TypeEqn]
eqs = (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs Type -> Type -> Bool
eqType [Type]
rs1 [Type]
rs2
    , Bool -> Bool
not ([TypeEqn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeEqn]
eqs) ]

improveFromAnother loc
_ Type
_ Type
_ = []


-- Improve a class constraint from instance declarations
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

improveFromInstEnv :: InstEnvs
                   -> (PredType -> SrcSpan -> 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 :: forall loc.
InstEnvs
-> (Type -> SrcSpan -> loc) -> Class -> [Type] -> [FunDepEqn loc]
improveFromInstEnv InstEnvs
inst_env Type -> SrcSpan -> loc
mk_loc Class
cls [Type]
tys
  = [ FDEqn { fd_qtvs :: [TyVar]
fd_qtvs = [TyVar]
meta_tvs, fd_eqs :: [TypeEqn]
fd_eqs = [TypeEqn]
eqs
            , fd_pred1 :: Type
fd_pred1 = Type
p_inst, fd_pred2 :: Type
fd_pred2 = Type
pred
            , fd_loc :: loc
fd_loc = Type -> SrcSpan -> loc
mk_loc Type
p_inst (TyVar -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan (ClsInst -> TyVar
is_dfun ClsInst
ispec)) }
    | FunDep TyVar
fd <- [FunDep TyVar]
cls_fds             -- Iterate through the fundeps first,
                                -- because there often are none!
    , let trimmed_tcs :: [RoughMatchTc]
trimmed_tcs = [TyVar] -> FunDep TyVar -> [RoughMatchTc] -> [RoughMatchTc]
trimRoughMatchTcs [TyVar]
cls_tvs FunDep TyVar
fd [RoughMatchTc]
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
    , ClsInst
ispec <- [ClsInst]
instances
    , ([TyVar]
meta_tvs, [TypeEqn]
eqs) <- [TyVar]
-> FunDep TyVar
-> ClsInst
-> [Type]
-> [RoughMatchTc]
-> [([TyVar], [TypeEqn])]
improveClsFD [TyVar]
cls_tvs FunDep TyVar
fd ClsInst
ispec
                                      [Type]
tys [RoughMatchTc]
trimmed_tcs -- NB: orientation
    , let p_inst :: Type
p_inst = Class -> [Type] -> Type
mkClassPred Class
cls (ClsInst -> [Type]
is_tys ClsInst
ispec)
    ]
  where
    ([TyVar]
cls_tvs, [FunDep TyVar]
cls_fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
cls
    instances :: [ClsInst]
instances          = InstEnvs -> Class -> [ClsInst]
classInstances InstEnvs
inst_env Class
cls
    rough_tcs :: [RoughMatchTc]
rough_tcs          = Name -> RoughMatchTc
RM_KnownTc (Class -> Name
className Class
cls) RoughMatchTc -> [RoughMatchTc] -> [RoughMatchTc]
forall a. a -> [a] -> [a]
: [Type] -> [RoughMatchTc]
roughMatchTcs [Type]
tys
    pred :: Type
pred               = Class -> [Type] -> Type
mkClassPred Class
cls [Type]
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 :: [TyVar]
-> FunDep TyVar
-> ClsInst
-> [Type]
-> [RoughMatchTc]
-> [([TyVar], [TypeEqn])]
improveClsFD [TyVar]
clas_tvs FunDep TyVar
fd
             (ClsInst { is_tvs :: ClsInst -> [TyVar]
is_tvs = [TyVar]
qtvs, is_tys :: ClsInst -> [Type]
is_tys = [Type]
tys_inst, is_tcs :: ClsInst -> [RoughMatchTc]
is_tcs = [RoughMatchTc]
rough_tcs_inst })
             [Type]
tys_actual [RoughMatchTc]
rough_tcs_actual

  | [RoughMatchTc] -> [RoughMatchTc] -> Bool
instanceCantMatch [RoughMatchTc]
rough_tcs_inst [RoughMatchTc]
rough_tcs_actual
  = []          -- Filter out ones that can't possibly match,

  | Bool
otherwise
  = Bool -> SDoc -> [([TyVar], [TypeEqn])] -> [([TyVar], [TypeEqn])]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [Type]
tys_inst [Type]
tys_actual Bool -> Bool -> Bool
&&
               [Type] -> [TyVar] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [Type]
tys_inst [TyVar]
clas_tvs)
              ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys_inst SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys_actual) ([([TyVar], [TypeEqn])] -> [([TyVar], [TypeEqn])])
-> [([TyVar], [TypeEqn])] -> [([TyVar], [TypeEqn])]
forall a b. (a -> b) -> a -> b
$

    case Subst -> [Type] -> [Type] -> Maybe Subst
tcMatchTyKisX Subst
init_subst [Type]
ltys1 [Type]
ltys2 of
        Maybe Subst
Nothing  -> []
        Just Subst
subst | Maybe Subst -> Bool
forall a. Maybe a -> Bool
isJust (Subst -> [Type] -> [Type] -> Maybe Subst
tcMatchTyKisX Subst
subst [Type]
rtys1 [Type]
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.
                  -> []

                  | [TypeEqn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeEqn]
fdeqs
                  -> []

                  | Bool
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 ]) $
                     [([TyVar]
meta_tvs, [TypeEqn]
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' :: [Type]
rtys1' = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) [Type]
rtys1

                    fdeqs :: [TypeEqn]
fdeqs = (Type -> Type -> Bool) -> [Type] -> [Type] -> [TypeEqn]
zipAndComputeFDEqs (\Type
_ Type
_ -> Bool
False) [Type]
rtys1' [Type]
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 :: [TyVar]
meta_tvs = [ TyVar -> Type -> TyVar
setVarType TyVar
tv (HasDebugCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst (TyVar -> Type
varType TyVar
tv))
                               | TyVar
tv <- [TyVar]
qtvs
                               , TyVar
tv TyVar -> Subst -> Bool
`notElemSubst` Subst
subst
                               , TyVar
tv TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
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 :: Subst
init_subst     = InScopeSet -> Subst
mkEmptySubst (InScopeSet -> Subst) -> InScopeSet -> Subst
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet -> InScopeSet) -> TyCoVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
                     [TyVar] -> TyCoVarSet
mkVarSet [TyVar]
qtvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
ltys2
    ([Type]
ltys1, [Type]
rtys1) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
clas_tvs [Type]
tys_inst
    ([Type]
ltys2, [Type]
rtys2) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
clas_tvs [Type]
tys_actual
    rtys1_tvs :: TyCoVarSet
rtys1_tvs      = [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
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 :: Bool -> Class -> [Type] -> [Type] -> Validity' CoverageProblem
checkInstCoverage Bool
be_liberal Class
clas [Type]
theta [Type]
inst_taus
  | (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool) -> (Type -> Maybe Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Type
isUnsatisfiableCt_maybe) [Type]
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).
  = Validity' CoverageProblem
forall a. Validity' a
IsValid
  | Bool
otherwise
  = [Validity' CoverageProblem] -> Validity' CoverageProblem
forall a. [Validity' a] -> Validity' a
allValid ((FunDep TyVar -> Validity' CoverageProblem)
-> [FunDep TyVar] -> [Validity' CoverageProblem]
forall a b. (a -> b) -> [a] -> [b]
map FunDep TyVar -> Validity' CoverageProblem
fundep_ok [FunDep TyVar]
fds)
  where
    ([TyVar]
tyvars, [FunDep TyVar]
fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
clas
    fundep_ok :: FunDep TyVar -> Validity' CoverageProblem
fundep_ok FunDep TyVar
fd
       | (TyCoVarSet -> Bool) -> Pair TyCoVarSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TyCoVarSet -> Bool
isEmptyVarSet Pair TyCoVarSet
undetermined_tvs
       = Validity' CoverageProblem
forall a. Validity' a
IsValid
       | Bool
otherwise
       = CoverageProblem -> Validity' CoverageProblem
forall a. a -> Validity' a
NotValid CoverageProblem
not_covered_msg
       where
         ([Type]
ls,[Type]
rs) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
tyvars [Type]
inst_taus
         ls_tvs :: TyCoVarSet
ls_tvs = [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
ls
         rs_tvs :: Pair TyCoVarSet
rs_tvs = [Type] -> Pair TyCoVarSet
visVarsOfTypes [Type]
rs

         undetermined_tvs :: Pair TyCoVarSet
undetermined_tvs | Bool
be_liberal = Pair TyCoVarSet
liberal_undet_tvs
                          | Bool
otherwise  = Pair TyCoVarSet
conserv_undet_tvs

         closed_ls_tvs :: TyCoVarSet
closed_ls_tvs = [Type] -> TyCoVarSet -> TyCoVarSet
closeWrtFunDeps [Type]
theta TyCoVarSet
ls_tvs
         liberal_undet_tvs :: Pair TyCoVarSet
liberal_undet_tvs = (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`minusVarSet` TyCoVarSet
closed_ls_tvs) (TyCoVarSet -> TyCoVarSet) -> Pair TyCoVarSet -> Pair TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair TyCoVarSet
rs_tvs
         conserv_undet_tvs :: Pair TyCoVarSet
conserv_undet_tvs = (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`minusVarSet` TyCoVarSet
ls_tvs)        (TyCoVarSet -> TyCoVarSet) -> Pair TyCoVarSet -> Pair TyCoVarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair TyCoVarSet
rs_tvs

         not_covered_msg :: CoverageProblem
not_covered_msg =
           CoverageProblem
            { not_covered_fundep :: FunDep TyVar
not_covered_fundep        = FunDep TyVar
fd
            , not_covered_fundep_inst :: FunDep Type
not_covered_fundep_inst   = ([Type]
ls, [Type]
rs)
            , not_covered_invis_vis_tvs :: Pair TyCoVarSet
not_covered_invis_vis_tvs = Pair TyCoVarSet
undetermined_tvs
            , not_covered_liberal :: FailedCoverageCondition
not_covered_liberal       =
                if Bool
be_liberal
                then FailedCoverageCondition
FailedLICC
                else FailedICC
                      { alsoFailedLICC :: Bool
alsoFailedLICC = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (TyCoVarSet -> Bool) -> Pair TyCoVarSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TyCoVarSet -> Bool
isEmptyVarSet Pair TyCoVarSet
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.decideMonoTyVars.

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 :: [Type] -> TyCoVarSet -> TyCoVarSet
closeWrtFunDeps [Type]
preds TyCoVarSet
fixed_tvs
  | [(TyCoVarSet, TyCoVarSet)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TyCoVarSet, TyCoVarSet)]
tv_fds = TyCoVarSet
fixed_tvs -- Fast escape hatch for common case.
  | Bool
otherwise   = Bool -> SDoc -> TyCoVarSet -> TyCoVarSet
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCoVarSet -> TyCoVarSet
closeOverKinds TyCoVarSet
fixed_tvs TyCoVarSet -> TyCoVarSet -> Bool
forall a. Eq a => a -> a -> Bool
== TyCoVarSet
fixed_tvs)
                    ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"closeWrtFunDeps: fixed_tvs is not closed over kinds"
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"fixed_tvs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyCoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCoVarSet
fixed_tvs
                          , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"closure:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyCoVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCoVarSet -> TyCoVarSet
closeOverKinds TyCoVarSet
fixed_tvs) ])
                (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
fixVarSet TyCoVarSet -> TyCoVarSet
extend TyCoVarSet
fixed_tvs
  where

    extend :: TyCoVarSet -> TyCoVarSet
extend TyCoVarSet
fixed_tvs = (TyCoVarSet -> (TyCoVarSet, TyCoVarSet) -> TyCoVarSet)
-> TyCoVarSet -> [(TyCoVarSet, TyCoVarSet)] -> TyCoVarSet
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' TyCoVarSet -> (TyCoVarSet, TyCoVarSet) -> TyCoVarSet
add TyCoVarSet
fixed_tvs [(TyCoVarSet, TyCoVarSet)]
tv_fds
       where
          add :: TyCoVarSet -> (TyCoVarSet, TyCoVarSet) -> TyCoVarSet
add TyCoVarSet
fixed_tvs (TyCoVarSet
ls,TyCoVarSet
rs)
            | TyCoVarSet
ls TyCoVarSet -> TyCoVarSet -> Bool
`subVarSet` TyCoVarSet
fixed_tvs = TyCoVarSet
fixed_tvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet -> TyCoVarSet
closeOverKinds TyCoVarSet
rs
            | Bool
otherwise                = TyCoVarSet
fixed_tvs
            -- closeOverKinds: see Note [Closing over kinds in coverage]

    tv_fds  :: [(TyCoVarSet,TyCoVarSet)]
    tv_fds :: [(TyCoVarSet, TyCoVarSet)]
tv_fds  = [ ([Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
ls, FV -> TyCoVarSet
fvVarSet (FV -> TyCoVarSet) -> FV -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ Bool -> [Type] -> FV
injectiveVarsOfTypes Bool
True [Type]
rs)
                  -- See Note [Care with type functions]
              | Type
pred <- [Type]
preds
              , Type
pred' <- Type
pred Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type -> [Type]
transSuperClasses Type
pred
                   -- Look for fundeps in superclasses too
              , ([Type]
ls, [Type]
rs) <- Type -> [FunDep Type]
determined Type
pred' ]

    determined :: PredType -> [([Type],[Type])]
    determined :: Type -> [FunDep Type]
determined Type
pred
       = case Type -> Pred
classifyPredType Type
pred of
            EqPred EqRel
NomEq Type
t1 Type
t2 -> [([Type
t1],[Type
t2]), ([Type
t2],[Type
t1])]
               -- See Note [Equality superclasses]
            ClassPred Class
cls [Type]
tys  -> [ FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys
                                  | let ([TyVar]
cls_tvs, [FunDep TyVar]
cls_fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
cls
                                  , FunDep TyVar
fd <- [FunDep TyVar]
cls_fds ]
            Pred
_ -> []


{- *********************************************************************
*                                                                      *
        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 :: InstEnvs -> ClsInst -> [ClsInst]
checkFunDeps InstEnvs
inst_envs (ClsInst { is_tvs :: ClsInst -> [TyVar]
is_tvs = [TyVar]
qtvs1, is_cls :: ClsInst -> Class
is_cls = Class
cls
                                , is_tys :: ClsInst -> [Type]
is_tys = [Type]
tys1, is_tcs :: ClsInst -> [RoughMatchTc]
is_tcs = [RoughMatchTc]
rough_tcs1 })
  | [FunDep TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FunDep TyVar]
fds
  = []
  | Bool
otherwise
  = (ClsInst -> ClsInst -> Bool) -> [ClsInst] -> [ClsInst]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy ClsInst -> ClsInst -> Bool
eq_inst ([ClsInst] -> [ClsInst]) -> [ClsInst] -> [ClsInst]
forall a b. (a -> b) -> a -> b
$
    [ ClsInst
ispec | ClsInst
ispec <- [ClsInst]
cls_insts
            , FunDep TyVar
fd    <- [FunDep TyVar]
fds
            , FunDep TyVar -> ClsInst -> Bool
is_inconsistent FunDep TyVar
fd ClsInst
ispec ]
  where
    cls_insts :: [ClsInst]
cls_insts      = InstEnvs -> Class -> [ClsInst]
classInstances InstEnvs
inst_envs Class
cls
    ([TyVar]
cls_tvs, [FunDep TyVar]
fds) = Class -> ([TyVar], [FunDep TyVar])
classTvsFds Class
cls
    qtv_set1 :: TyCoVarSet
qtv_set1       = [TyVar] -> TyCoVarSet
mkVarSet [TyVar]
qtvs1

    is_inconsistent :: FunDep TyVar -> ClsInst -> Bool
is_inconsistent FunDep TyVar
fd (ClsInst { is_tvs :: ClsInst -> [TyVar]
is_tvs = [TyVar]
qtvs2, is_tys :: ClsInst -> [Type]
is_tys = [Type]
tys2, is_tcs :: ClsInst -> [RoughMatchTc]
is_tcs = [RoughMatchTc]
rough_tcs2 })
      | [RoughMatchTc] -> [RoughMatchTc] -> Bool
instanceCantMatch [RoughMatchTc]
trimmed_tcs [RoughMatchTc]
rough_tcs2
      = Bool
False
      | Bool
otherwise
      = case BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTyKis BindFun
bind_fn [Type]
ltys1 [Type]
ltys2 of
          Maybe Subst
Nothing         -> Bool
False
          Just Subst
subst
            -> Maybe Subst -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$   -- Bogus legacy test (#10675)
                             -- See Note [Bogus consistency check]
               BindFun -> [Type] -> [Type] -> Maybe Subst
tcUnifyTyKis BindFun
bind_fn (Subst -> [Type] -> [Type]
substTysUnchecked Subst
subst [Type]
rtys1) (Subst -> [Type] -> [Type]
substTysUnchecked Subst
subst [Type]
rtys2)

      where
        trimmed_tcs :: [RoughMatchTc]
trimmed_tcs    = [TyVar] -> FunDep TyVar -> [RoughMatchTc] -> [RoughMatchTc]
trimRoughMatchTcs [TyVar]
cls_tvs FunDep TyVar
fd [RoughMatchTc]
rough_tcs1
        ([Type]
ltys1, [Type]
rtys1) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys1
        ([Type]
ltys2, [Type]
rtys2) = FunDep TyVar -> [TyVar] -> [Type] -> FunDep Type
instFD FunDep TyVar
fd [TyVar]
cls_tvs [Type]
tys2
        qtv_set2 :: TyCoVarSet
qtv_set2       = [TyVar] -> TyCoVarSet
mkVarSet [TyVar]
qtvs2
        bind_fn :: BindFun
bind_fn        = TyCoVarSet -> BindFun
matchBindFun (TyCoVarSet
qtv_set1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
qtv_set2)

    eq_inst :: ClsInst -> ClsInst -> Bool
eq_inst ClsInst
i1 ClsInst
i2 = ClsInst -> TyVar
instanceDFunId ClsInst
i1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== ClsInst -> TyVar
instanceDFunId ClsInst
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 :: [TyVar] -> FunDep TyVar -> [RoughMatchTc] -> [RoughMatchTc]
trimRoughMatchTcs [TyVar]
_clas_tvs FunDep TyVar
_ [] = String -> [RoughMatchTc]
forall a. HasCallStack => String -> a
panic String
"trimRoughMatchTcs: nullary [RoughMatchTc]"
trimRoughMatchTcs [TyVar]
clas_tvs ([TyVar]
ltvs, [TyVar]
_) (RoughMatchTc
cls:[RoughMatchTc]
mb_tcs)
  = RoughMatchTc
cls RoughMatchTc -> [RoughMatchTc] -> [RoughMatchTc]
forall a. a -> [a] -> [a]
: (TyVar -> RoughMatchTc -> RoughMatchTc)
-> [TyVar] -> [RoughMatchTc] -> [RoughMatchTc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TyVar -> RoughMatchTc -> RoughMatchTc
select [TyVar]
clas_tvs [RoughMatchTc]
mb_tcs
  where
    select :: TyVar -> RoughMatchTc -> RoughMatchTc
select TyVar
clas_tv RoughMatchTc
mb_tc | TyVar
clas_tv TyVar -> [TyVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyVar]
ltvs = RoughMatchTc
mb_tc
                         | Bool
otherwise           = RoughMatchTc
RM_WildCard