{-
(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 { 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 -> 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_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 HasCallStack => Type -> Type -> Bool
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
                   -> (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 :: forall loc.
InstEnvs -> (ClsInst -> loc) -> Class -> [Type] -> [FunDepEqn loc]
improveFromInstEnv InstEnvs
inst_env ClsInst -> loc
mk_loc Class
cls [Type]
tys
  = [ FDEqn { fd_qtvs :: [TyVar]
fd_qtvs = [TyVar]
meta_tvs, fd_eqs :: [TypeEqn]
fd_eqs = [TypeEqn]
eqs, fd_loc :: loc
fd_loc = ClsInst -> loc
mk_loc 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
    ]
  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

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.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 :: [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 | Bool -> Bool
not (Class -> Bool
isIPClass Class
cls)
               -- isIPClass: see Note [closeWrtFunDeps ignores implicit parameters]
                              -> [ 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
_ -> []

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