{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE MultiWayIf #-}

-- | Solving Class constraints CDictCan
module GHC.Tc.Solver.Dict (
  solveDict, solveDictNC, solveCallStack,
  checkInstanceOK,
  matchLocalInst, chooseInstance,
  makeSuperClasses, mkStrictSuperClasses
  ) where

import GHC.Prelude

import {-# SOURCE #-} GHC.Tc.Solver.Solve( solveSimpleWanteds )

import GHC.Tc.Errors.Types
import GHC.Tc.Instance.Class( matchEqualityInst )
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc
import GHC.Tc.Types.Origin
import GHC.Tc.Solver.FunDeps( tryDictFunDeps )
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Tc.Solver.Types
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Unify( uType, mightEqualLater )

import GHC.Hs.Type( HsIPName(..) )

import GHC.Core
import GHC.Core.Make
import GHC.Core.Type
import GHC.Core.Class
import GHC.Core.Predicate
import GHC.Core.InstEnv( DFunInstType )
import GHC.Core.Multiplicity ( scaledThing )
import GHC.Core.Unify ( ruleMatchTyKiX )

import GHC.Types.TyThing( lookupDataCon, lookupId )
import GHC.Types.Name
import GHC.Types.Name.Set
import GHC.Types.Var
import GHC.Types.Id( mkTemplateLocals )
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.SrcLoc

import GHC.Builtin.Names( srcLocDataConName, pushCallStackName, emptyCallStackName )

import GHC.Utils.Monad ( concatMapM )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc

import GHC.Unit.Module

import GHC.Data.Bag

import GHC.Driver.DynFlags

import qualified GHC.LanguageExtensions as LangExt

import Data.Maybe ( listToMaybe, mapMaybe, isJust )
import Data.Void( Void )

import Control.Monad

{- *********************************************************************
*                                                                      *
*                      Class Canonicalization
*                                                                      *
********************************************************************* -}

solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void
-- NC: this comes from CNonCanonical or CIrredCan
-- Precondition: already rewritten by inert set
solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void
solveDictNC CtEvidence
ev Class
cls [Type]
tys
  = do { TcS () -> SolverStage ()
forall a. TcS a -> SolverStage a
simpleStage (TcS () -> SolverStage ()) -> TcS () -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcS ()
traceTcS String
"solveDictNC" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
       ; dict_ct <- CtEvidence -> Class -> [Type] -> SolverStage DictCt
canDictCt CtEvidence
ev Class
cls [Type]
tys
       ; solveDict dict_ct }

solveDict :: DictCt -> SolverStage Void
-- Preconditions: `tys` are already rewritten by the inert set
solveDict :: DictCt -> SolverStage Void
solveDict dict_ct :: DictCt
dict_ct@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
  | Class -> Bool
isEqualityClass Class
cls
  = CtEvidence -> Class -> [Type] -> SolverStage Void
solveEqualityDict CtEvidence
ev Class
cls [Type]
tys

  | Bool
otherwise
  = Bool -> SDoc -> SolverStage Void -> SolverStage Void
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (HasDebugCallStack => CtEvidence -> Role
CtEvidence -> Role
ctEvRewriteRole CtEvidence
ev Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) (SolverStage Void -> SolverStage Void)
-> SolverStage Void -> SolverStage Void
forall a b. (a -> b) -> a -> b
$
    do { TcS () -> SolverStage ()
forall a. TcS a -> SolverStage a
simpleStage (TcS () -> SolverStage ()) -> TcS () -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcS ()
traceTcS String
"solveDict" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_ct)

       -- Look in the inert dictionaries
       ; DictCt -> SolverStage ()
tryInertDicts DictCt
dict_ct

       -- Try top-level instances
       ; DictCt -> SolverStage ()
tryInstances DictCt
dict_ct

       -- Try fundeps /after/ tryInstances:
       --     see (DFL2) in Note [Do fundeps last]
       ; DictCt -> SolverStage ()
tryDictFunDeps DictCt
dict_ct

       ; TcS () -> SolverStage ()
forall a. TcS a -> SolverStage a
simpleStage (DictCt -> TcS ()
updInertDicts DictCt
dict_ct)
       ; CtEvidence -> String -> SolverStage Void
forall a. CtEvidence -> String -> SolverStage a
stopWithStage (DictCt -> CtEvidence
dictCtEvidence DictCt
dict_ct) String
"Kept inert DictCt" }

canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt
-- Once-only processing of Dict constraints:
--   * expand superclasses
--   * deal with CallStack
canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt
canDictCt CtEvidence
ev Class
cls [Type]
tys
  | CtEvidence -> Bool
isGiven CtEvidence
ev  -- See Note [Eagerly expand given superclasses]
  = TcS (StopOrContinue DictCt) -> SolverStage DictCt
TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt)
-> TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a b. (a -> b) -> a -> b
$
    do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
         -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel]
       ; emitWork (listToBag sc_cts)

       ; continueWith (DictCt { di_ev = ev, di_cls = cls
                              , di_tys = tys, di_pend_sc = doNotExpand }) }
         -- doNotExpand: We have already expanded superclasses for /this/ dict
         -- so set the fuel to doNotExpand to avoid repeating expansion

  | CtWanted (WantedCt { ctev_rewriters :: WantedCtEvidence -> CoHoleSet
ctev_rewriters = CoHoleSet
rws }) <- CtEvidence
ev
  , Just FastString
ip_name <- Class -> [Type] -> Maybe FastString
isCallStackPred Class
cls [Type]
tys
  , Just FastString
fun_fs  <- CtOrigin -> Maybe FastString
isPushCallStackOrigin_maybe CtOrigin
orig
  -- If we're given a CallStack constraint that arose from a function
  -- call, we need to push the current call-site onto the stack instead
  -- of solving it directly from a given.
  -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
  -- and Note [Solving CallStack constraints]
  = TcS (StopOrContinue DictCt) -> SolverStage DictCt
TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt)
-> TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a b. (a -> b) -> a -> b
$
    do { -- First we emit a new constraint that will capture the
         -- given CallStack.

         let new_loc :: CtLoc
new_loc = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc (HsIPName -> CtOrigin
IPOccOrigin (FastString -> HsIPName
HsIPName FastString
ip_name))
                            -- We change the origin to IPOccOrigin so
                            -- this rule does not fire again.
                            -- See Note [Overview of implicit CallStacks]
                            -- in GHC.Tc.Types.Evidence

       ; new_ev <- WantedCtEvidence -> CtEvidence
WantedCtEvidence -> CtEvidence
CtWanted (WantedCtEvidence -> CtEvidence)
-> TcS WantedCtEvidence -> TcS CtEvidence
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> CoHoleSet -> Type -> TcS WantedCtEvidence
newWantedEvVarNC CtLoc
new_loc CoHoleSet
rws Type
pred

         -- Then we solve the wanted by pushing the call-site
         -- onto the newly emitted CallStack
       ; let ev_cs = FastString -> RealSrcSpan -> EvExpr -> EvCallStack
EvCsPushCall FastString
fun_fs (CtLoc -> RealSrcSpan
ctLocSpan CtLoc
loc) (HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
new_ev)
       ; solveCallStack ev ev_cs

       ; continueWith (DictCt { di_ev = new_ev, di_cls = cls
                              , di_tys = tys, di_pend_sc = doNotExpand }) }
         -- doNotExpand: No superclasses for class CallStack
         -- See invariants in CDictCan.cc_pend_sc

  | Bool
otherwise
  = TcS (StopOrContinue DictCt) -> SolverStage DictCt
TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt)
-> TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a b. (a -> b) -> a -> b
$
    do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; let fuel | Class -> Bool
classHasSCs Class
cls = DynFlags -> ScDepth
wantedsFuel DynFlags
dflags
                  | Bool
otherwise       = ScDepth
doNotExpand
                  -- See Invariants in `CCDictCan.cc_pend_sc`
       ; continueWith (DictCt { di_ev = ev, di_cls = cls
                              , di_tys = tys, di_pend_sc = fuel }) }

  where
    loc :: CtLoc
loc  = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
    orig :: CtOrigin
orig = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
    pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev

{- *********************************************************************
*                                                                      *
*           Implicit parameters and call stacks
*                                                                      *
********************************************************************* -}

solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
-- Also called from GHC.Tc.Solver when defaulting call stacks
solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
solveCallStack CtEvidence
ev EvCallStack
ev_cs
  -- We're given ev_cs :: CallStack, but the evidence term should be a
  -- dictionary, so we have to coerce ev_cs to a dictionary for
  -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
  = do { inner_stk <- Type -> EvCallStack -> TcS EvExpr
evCallStack Type
pred EvCallStack
ev_cs
       ; let ev_tm = EvExpr -> EvTerm
EvExpr (Type -> EvExpr -> EvExpr
evWrapIPE Type
pred EvExpr
inner_stk)
       ; setDictIfWanted ev EvCanonical ev_tm }
         -- EvCanonical: see Note [CallStack and ExceptionContext hack]
  where
    pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev

-- Dictionary for CallStack implicit parameters
evCallStack :: TcPredType -> EvCallStack -> TcS EvExpr
-- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
evCallStack :: Type -> EvCallStack -> TcS EvExpr
evCallStack Type
_ EvCallStack
EvCsEmpty
  = EvVar -> EvExpr
EvVar -> EvExpr
forall b. EvVar -> Expr b
Var (EvVar -> EvExpr) -> TcS EvVar -> TcS EvExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> TcS EvVar
forall (m :: * -> *). MonadThings m => Name -> m EvVar
lookupId Name
emptyCallStackName
evCallStack Type
pred (EvCsPushCall FastString
fs RealSrcSpan
loc EvExpr
tm)
  = do { df <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; m  <- getModule
       ; srcLocDataCon <- lookupDataCon srcLocDataConName
       ; let platform = DynFlags -> Platform
targetPlatform DynFlags
df
             mkSrcLoc RealSrcSpan
l = DataCon -> [EvExpr] -> EvExpr
mkCoreConWrapApps DataCon
srcLocDataCon ([EvExpr] -> EvExpr) -> TcS [EvExpr] -> TcS EvExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                          [TcS EvExpr] -> TcS [EvExpr]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [ FastString -> TcS EvExpr
forall (m :: * -> *). MonadThings m => FastString -> m EvExpr
mkStringExprFS (Unit -> FastString
forall u. IsUnitId u => u -> FastString
unitFS (Unit -> FastString) -> Unit -> FastString
forall a b. (a -> b) -> a -> b
$ Module -> Unit
forall unit. GenModule unit -> unit
moduleUnit Module
m)
                                   , FastString -> TcS EvExpr
forall (m :: * -> *). MonadThings m => FastString -> m EvExpr
mkStringExprFS (ModuleName -> FastString
moduleNameFS (ModuleName -> FastString) -> ModuleName -> FastString
forall a b. (a -> b) -> a -> b
$ Module -> ModuleName
forall unit. GenModule unit -> ModuleName
moduleName Module
m)
                                   , FastString -> TcS EvExpr
forall (m :: * -> *). MonadThings m => FastString -> m EvExpr
mkStringExprFS (RealSrcSpan -> FastString
srcSpanFile RealSrcSpan
l)
                                   , EvExpr -> TcS EvExpr
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvExpr -> TcS EvExpr) -> EvExpr -> TcS EvExpr
forall a b. (a -> b) -> a -> b
$ Platform -> ScDepth -> EvExpr
mkIntExprInt Platform
platform (RealSrcSpan -> ScDepth
srcSpanStartLine RealSrcSpan
l)
                                   , EvExpr -> TcS EvExpr
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvExpr -> TcS EvExpr) -> EvExpr -> TcS EvExpr
forall a b. (a -> b) -> a -> b
$ Platform -> ScDepth -> EvExpr
mkIntExprInt Platform
platform (RealSrcSpan -> ScDepth
srcSpanStartCol RealSrcSpan
l)
                                   , EvExpr -> TcS EvExpr
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvExpr -> TcS EvExpr) -> EvExpr -> TcS EvExpr
forall a b. (a -> b) -> a -> b
$ Platform -> ScDepth -> EvExpr
mkIntExprInt Platform
platform (RealSrcSpan -> ScDepth
srcSpanEndLine RealSrcSpan
l)
                                   , EvExpr -> TcS EvExpr
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (EvExpr -> TcS EvExpr) -> EvExpr -> TcS EvExpr
forall a b. (a -> b) -> a -> b
$ Platform -> ScDepth -> EvExpr
mkIntExprInt Platform
platform (RealSrcSpan -> ScDepth
srcSpanEndCol RealSrcSpan
l)
                                   ]

       ; push_cs_id <- lookupId pushCallStackName
       ; name_expr  <- mkStringExprFS fs
       ; loc_expr   <- mkSrcLoc loc
               -- At this point tm :: IP sym CallStack
               -- but we need the actual CallStack to pass to pushCS,
               -- so we use evUwrapIP to strip the dictionary wrapper
               -- See Note [Overview of implicit CallStacks]
       ; let outer_stk = Type -> EvExpr -> EvExpr
evUnwrapIPE Type
pred EvExpr
tm
       ; return (mkCoreApps (Var push_cs_id)
                    [mkCoreTup [name_expr, loc_expr], outer_stk]) }

{- Note [Solving CallStack constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See Note [Overview of implicit CallStacks] in GHc.Tc.Types.Evidence.

Suppose f :: HasCallStack => blah.  Then

* Each call to 'f' gives rise to
    [W] s1 :: IP "callStack" CallStack    -- CtOrigin = OccurrenceOf f
  with a CtOrigin that says "OccurrenceOf f".
  Remember that HasCallStack is just shorthand for
    IP "callStack" CallStack
  See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence

* We canonicalise such constraints, in GHC.Tc.Solver.Dict.canDictNC, by
  pushing the call-site info on the stack, and changing the CtOrigin
  to record that has been done.
   Bind:  s1 = pushCallStack <site-info> s2
   [W] s2 :: IP "callStack" CallStack   -- CtOrigin = IPOccOrigin

* Then, and only then, we can solve the constraint from an enclosing
  Given.

So we must be careful /not/ to solve 's1' from the Givens.  We guarantee
this by canonicalising before looking up in the inert set.

Note [CallStack and ExceptionContext hack]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It isn't really right that we treat CallStack and ExceptionContext dictionaries
as canonical, in the sense of Note [Coherence and specialisation: overview].
They definitely are not!

But if we use EvNonCanonical here we get lots of
    nospec (error @Int) dict  string
(since `error` takes a HasCallStack dict), and that isn't bottoming  (at least not
without extra work)  So, hackily, we just say that HasCallStack and ExceptionContext
are canonical, even though they aren't really.

Note [Shadowing of implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we add a new /given/ implicit parameter to the inert set, it /replaces/
any existing givens for the same implicit parameter.  This makes a difference
in two places:

* In `GHC.Tc.Solver.InertSet.solveOneFromTheOther`, be careful when we have
   (?x :: ty) in the inert set and an identical (?x :: ty) as the work item.

* In `updInertDicts`, in this module, when adding [G] (?x :: ty), remove any
  existing [G] (?x :: ty'), regardless of ty'.

There are wrinkles:

* Wrinkle (SIP1): we must be careful of superclasses (#14218).  Consider
     f,g :: (?x::Int, C a) => a -> a
     f v = let ?x = 4 in g v

  The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
  We must /not/ solve this from the Given (?x::Int, C a), because of
  the intervening binding for (?x::Int).  #14218.

  We deal with this by arranging that when we add [G] (?x::ty) we /delete/
  * from the inert_cans, and
  * from the inert_solved_dicts
  any existing [G] (?x::ty) /and/ any [G] D tys, where (D tys) has a superclass
  with (?x::ty).  See Note [Local implicit parameters] in GHC.Core.Predicate.

  An very important special case is constraint tuples like [G] (% ?x::ty, Eq a %).

  But it could also happen for `class xx => D xx where ...` and the constraint
  D (?x :: int); again see Note [Local implicit parameters].  This corner
  (constraint-kinded variables instantiated with implicit parameter constraints)
  is not well explored.

  You might worry about whether deleting an /entire/ constraint just because
  a distant superclass has an implicit parameter might make another Wanted for
  that constraint un-solvable.  Indeed so. But for constraint tuples it doesn't
  matter -- their entire payload is their superclasses.  And the other case is
  the ill-explored corner above.

  The code that accounts for (SIP1) is in updInertDicts; in particular the call to
  GHC.Core.Predicate.mentionsIP.

* Wrinkle (SIP2): we must apply this update semantics for `inert_solved_dicts`
  as well as `inert_cans` (#23761).

  You might think that wouldn't be necessary, because an element of
  `inert_solved_dicts` is never an implicit parameter (see
  Note [Solved dictionaries] in GHC.Tc.Solver.InertSet).
  While that is true, dictionaries in `inert_solved_dicts` may still have
  implicit parameters as a /superclass/! For example:

    class c => C c where ...
    f :: C (?x::Int) => blah

  Now (C (?x::Int)) has a superclass (?x::Int). This may look exotic, but it
  happens particularly for constraint tuples, like `(% ?x::Int, Eq a %)`.

* Wrinkle (SIP3)
  - Note that for the inert dictionaries, `inert_cans`, we must /only/ delete
    existing /Givens/!  Deleting an existing Wanted led to #26451; we just never
    solved it!

  - In contrast, the solved dictionaries, `inert_solved_dicts`, are really like
    Givens; they may be "inherited" from outer scopes, so we must delete any
    solved dictionaries for this implicit parameter for /both/ Givens /and/
    Wanteds.

    Otherwise the new Given doesn't properly shadow those inherited solved
    dictionaries. Test T23761 showed this up.

Example 1:

Suppose we have (typecheck/should_compile/ImplicitParamFDs)
  flub :: (?x :: Int) => (Int, Integer)
  flub = (?x, let ?x = 5 in ?x)
When we are checking the last ?x occurrence, we guess its type to be a fresh
unification variable alpha and emit an (IP "x" alpha) constraint. But the given
(?x :: Int) has been translated to an IP "x" Int constraint, which has a
functional dependency from the name to the type. So if that (?x::Int) is still
in the inert set, we'd get a fundep interaction that tells us that alpha ~ Int,
and we get a type error. This is bad.  The "replacement" semantics stops this
happening.

Example 2:

f :: (?x :: Char) => Char
f = let ?x = 'a' in ?x

The "let ?x = ..." generates an implication constraint of the form:

?x :: Char => ?x :: Char

Furthermore, the signature for `f` also generates an implication
constraint, so we end up with the following nested implication:

?x :: Char => (?x :: Char => ?x :: Char)

Note that the wanted (?x :: Char) constraint may be solved in two incompatible
ways: either by using the parameter from the signature, or by using the local
definition.  Our intention is that the local definition should "shadow" the
parameter of the signature.  The "replacement" semantics for implicit parameters
does this.

Example 3:

Similarly, consider
   f :: (?x::a) => Bool -> a

   g v = let ?x::Int = 3
         in (f v, let ?x::Bool = True in f v)

This should probably be well typed, with
   g :: Bool -> (Int, Bool)

So the inner binding for ?x::Bool *overrides* the outer one.

See ticket #17104 for a rather tricky example of this overriding
behaviour.

All this works for the normal cases but it has an odd side effect in
some pathological programs like this:

    -- This is accepted, the second parameter shadows
    f1 :: (?x :: Int, ?x :: Char) => Char
    f1 = ?x

    -- This is rejected, the second parameter shadows
    f2 :: (?x :: Int, ?x :: Char) => Int
    f2 = ?x

Both of these are actually wrong:  when we try to use either one,
we'll get two incompatible wanted constraints (?x :: Int, ?x :: Char),
which would lead to an error.

I can think of two ways to fix this:

  1. Simply disallow multiple constraints for the same implicit
    parameter---this is never useful, and it can be detected completely
    syntactically.

  2. Move the shadowing machinery to the location where we nest
     implications, and add some code here that will produce an
     error if we get multiple givens for the same implicit parameter.
-}


{- ******************************************************************************
*                                                                               *
                   solveEqualityDict
*                                                                               *
****************************************************************************** -}

{- Note [Solving equality classes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (~), which behaves as if it was defined like this:
  class a ~# b => a ~ b
  instance a ~# b => a ~ b
There are two more similar "equality classes" like this.  The full list is
  * (~)         eqTyCon
  * (~~)        heqTyCon
  * Coercible   coercibleTyCon
(See Note [The equality types story] in GHC.Builtin.Types.Prim.)

(EQC1) For a Given (boxed) equality like (t1 ~ t2), we /replace/ the constraint
  with its superclass (which, remember, is equally powerful) rather than /adding/
  it.  Thus, we turn  [G] d : t1 ~ t2  into
         [G] g : t1 ~# t2
         g := sc_sel d       -- Extend the evidence bindings

  We achieve this by
   (a) not expanding superclasses for equality classes at all;
       see the `isEqualityClass` test in `mk_strict_superclasses`
   (b) special logic to solve (t1 ~ t2) in the Given case of `solveEqualityDict`.

  Using replacement rather than adding can make a huge difference.
  Consider T17836, which has a constraint like
      forall b,c. a ~ (b,c) =>
        forall d,e. c ~ (d,e) =>
          ...etc...
  If we just /add/ the superclasses of [G] g1:a ~ (b,c), we'll put
  [G] g1:(a~(b,c)) in the inert set and emit [G] g2:a ~# (b,c).  That will
  kick out g1, and it'll be re-inserted as [G] g1':(b,c)~(b,c) which does
  no good to anyone.  When the implication is deeply nested, this has
  quadratic cost, and no benefit.  Just replace!

  (This can have a /big/ effect: test T17836 involves deeply-nested GADT
  pattern matching. Its compile-time allocation decreased by 40% when
  I added the "replace" rather than "add" semantics.)

(EQC2) Faced with [W] t1 ~ t2, it's always OK to reduce it to [W] t1 ~# t2,
  without worrying about Note [Instance and Given overlap].  Why?  Because
  if we had [G] s1 ~ s2, then we'd get the superclass [G] s1 ~# s2, and
  so the reduction of the [W] constraint does not risk losing any solutions.

  On the other hand, it can be fatal to /fail/ to reduce such equalities
  on the grounds of Note [Instance and Given overlap], because many good
  things flow from [W] t1 ~# t2.

Conclusion: we have a special solver pipeline for equality-class constraints,
`solveEqualityDict`.  It aggressively decomposes the boxed equality constraint
into an unboxed coercion, both for Givens and Wanteds, and /replaces/ the
boxed equality constraint with the unboxed one, so that the inert set never
contains the boxed one.

Note [Solving tuple constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
I tried treating tuple constraints, such as (% Eq a, Show a %), rather like
equality-class constraints (see Note [Solving equality classes]). That is, by
eagerly decomposing tuple-constraints into their component (Eq a) and (Show a).

But discarding the tuple Given (which "replacing" does) means that we may
have to reconstruct it for a recursive call.  For example
    f :: (% Eq a, Show a %) => blah
    f x = ....(f x')....
If we decomposed eagerly we'd get
    f = \(d : (% Eq a, Show a %)).
         let de = fst d
             ds = snd d
         in ....(f (% de, ds %))...
and the optimiser may not be clever enough to transform (f (% de, ds %)) into
(f d). See #10359 and its test case, and #23398.  (This issue is less pressing for
equality classes because they have to be unpacked strictly, so CSE-ing away
the reconstruction works fine.

So at the moment we don't decompose tuple constraints eagerly; instead we mostly
just treat them like other constraints.
* Given tuples are decomposed via their superclasses, in `canDictCt`.  So
    [G] (% Eq a, Show a %)
  has superclasses
    [G] Eq a,  [G] Show a

* Wanted tuples are decomposed via a built-in "instance". See
  `GHC.Tc.Instance.Class.matchCTuple`

There is a bit of special treatment: search for isCTupleClass.
-}

solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void
-- See Note [Solving equality classes]
-- Precondition: (isEqualityClass cls) True, so cls is (~), (~~), or Coercible
solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void
solveEqualityDict CtEvidence
ev Class
cls [Type]
tys
  | CtGiven (GivenCt { ctev_evar :: GivenCtEvidence -> EvVar
ctev_evar = EvVar
ev_id }) <- CtEvidence
ev
  , [EvVar
sel_id] <- Class -> [EvVar]
classSCSelIds Class
cls  -- Equality classes have just one superclass
  = TcS (StopOrContinue Void) -> SolverStage Void
TcS (StopOrContinue Void) -> SolverStage Void
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue Void) -> SolverStage Void)
-> TcS (StopOrContinue Void) -> SolverStage Void
forall a b. (a -> b) -> a -> b
$
    do { let loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
             sc_pred :: Type
sc_pred = EvVar -> [Type] -> Type
classMethodInstTy EvVar
sel_id [Type]
tys
             ev_expr :: EvTerm
ev_expr = EvExpr -> EvTerm
EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ EvVar -> EvExpr
forall b. EvVar -> Expr b
Var EvVar
sel_id EvExpr -> [Type] -> EvExpr
forall b. Expr b -> [Type] -> Expr b
`mkTyApps` [Type]
tys EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` EvVar -> EvExpr
evId EvVar
ev_id
       -- See (EQC1) in Note [Solving equality classes]
       -- This call to newGivenEv makes the evidence binding for the (unboxed) coercion
       ; given_ev <- CtLoc -> (Type, EvTerm) -> TcS GivenCtEvidence
newGivenEv CtLoc
loc (Type
sc_pred, EvTerm
ev_expr)
       ; startAgainWith (mkNonCanonical $ CtGiven given_ev) }

  | CtWanted (WantedCt { ctev_dest :: WantedCtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest }) <- CtEvidence
ev
  = TcS (StopOrContinue Void) -> SolverStage Void
TcS (StopOrContinue Void) -> SolverStage Void
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue Void) -> SolverStage Void)
-> TcS (StopOrContinue Void) -> SolverStage Void
forall a b. (a -> b) -> a -> b
$
    do { let (Role
role, Type
t1, Type
t2) = Class -> [Type] -> (Role, Type, Type)
matchEqualityInst Class
cls [Type]
tys
         -- Unify t1~t2, putting anything that can't be solved
         -- immediately into the work list
       ; CPH { cph_co = co } <- CtEvidence
-> Role -> (UnifyEnv -> TcM Coercion) -> TcS CoercionPlusHoles
wrapUnifierAndEmit CtEvidence
ev Role
role ((UnifyEnv -> TcM Coercion) -> TcS CoercionPlusHoles)
-> (UnifyEnv -> TcM Coercion) -> TcS CoercionPlusHoles
forall a b. (a -> b) -> a -> b
$ \UnifyEnv
uenv ->
                                UnifyEnv -> Type -> Type -> TcM Coercion
uType UnifyEnv
uenv Type
t1 Type
t2
         -- Set  d :: (t1~t2) = Eq# co
       ; setWantedDict dest EvCanonical $
         evDictApp cls tys [Coercion co]
       ; stopWith ev "Solved wanted lifted equality" }

  | Bool
otherwise
  = String -> SDoc -> SolverStage Void
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"solveEqualityDict" (Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls)

{- ******************************************************************************
*                                                                               *
                   interactDict
*                                                                               *
*********************************************************************************

Note [Shortcut solving]
~~~~~~~~~~~~~~~~~~~~~~~
When we interact a [W] constraint with a [G] constraint that solves it, there is
a possibility that we could produce better code if instead we solved from a
top-level instance declaration (See #12791, #5835). For example:

    class M a b where m :: a -> b

    type C a b = (Num a, M a b)

    f :: C Int b => b -> Int -> Int
    f _ x = x + 1

The body of `f` requires a [W] `Num Int` instance. We could solve this
constraint from the givens because we have `C Int b` and that provides us a
solution for `Num Int`. This would let us produce core like the following
(with -O2):

    f :: forall b. C Int b => b -> Int -> Int
    f = \ (@ b) ($d(%,%) :: C Int b) _ (eta1 :: Int) ->
        + @ Int
          (GHC.Classes.$p1(%,%) @ (Num Int) @ (M Int b) $d(%,%))
          eta1
          A.f1

This is bad! We could do /much/ better if we solved [W] `Num Int` directly
from the instance that we have in scope:

    f :: forall b. C Int b => b -> Int -> Int
    f = \ (@ b) _ _ (x :: Int) ->
        case x of { GHC.Types.I# x1 -> GHC.Types.I# (GHC.Prim.+# x1 1#) }

** NB: It is important to emphasize that all this is purely an optimization:
** exactly the same programs should typecheck with or without this procedure.

Consider
       f :: Ord [a] => ...
       f x = ..Need Eq [a]...
We could use the Eq [a] superclass of the Ord [a], or we could use the top-level
instance `Eq a => Eq [a]`.   But if we did the latter we'd be stuck with an
insoluble constraint (Eq a).

-----------------------------------
So the ShortCutSolving plan is this:
   If we could solve a constraint from a local Given,
       try first to /completely/ solve the constraint
       using only top-level instances,
       /without/ using any local Givens.
   - If that succeeds, use it
   - If not, use the local Given
-----------------------------------

An example that succeeds:

    class Eq a => C a b | b -> a where
      m :: b -> a

    f :: C [Int] b => b -> Bool
    f x = m x == []

We solve for `Eq [Int]`, which requires `Eq Int`, which we also have. This
produces the following core:

    f :: forall b. C [Int] b => b -> Bool
    f = \ (@ b) ($dC :: C [Int] b) (x :: b) ->
        GHC.Classes.$fEq[]_$s$c==
          (m @ [Int] @ b $dC x) (GHC.Types.[] @ Int)

An example that fails:

    class Eq a => C a b | b -> a where
      m :: b -> a

    f :: C [a] b => b -> Bool
    f x = m x == []

Which, because solving `Eq [a]` demands `Eq a` which we cannot solve. so short-cut
solving fails and we use the superclass of C:

    f :: forall a b. C [a] b => b -> Bool
    f = \ (@ a) (@ b) ($dC :: C [a] b) (eta :: b) ->
        ==
          @ [a]
          (A.$p1C @ [a] @ b $dC)
          (m @ [a] @ b $dC eta)
          (GHC.Types.[] @ a)

The moving parts are relatively simple:

* To attempt to solve the constraint completely, we just recursively
  call the constraint solver. See the use of `tryShortCutTcS` in
  `tcShortCutSolver`.

* When this attempted recursive solving, in `tryShortCutTcS`, we
  - start with an empty inert set: no Givens and no Wanteds
  - set a special mode  `TcSShortCut`, which signals that we are trying to solve
    using only top-level instances.

* When in TcSShortCut mode, since there are no Givens we can short-circuit;
  these are all just optimisations:
      - `tryInertDicts`
      - `GHC.Tc.Solver.Monad.lookupInertDict`
      - `noMatchableGivenDicts`
      - `matchLocalInst`
      - `GHC.Tc.Solver.Solve.runTcPluginsWanted`

* In `GHC.Tc.Solver.Instance.Class.matchInstEnv`: when short-cut solving,
  don't pick overlappable top-level instances

Some wrinkles:

(SCS1) Note [Shortcut solving: incoherence]

(SCS2) The short-cut solver just uses the solver recursively, so we get its
  full power:

    * We need to be able to handle recursive super classes. The
      solved_dicts state  ensures that we remember what we have already
      tried to solve to avoid looping.

    * As #15164 showed, it can be important to exploit sharing between
      goals. E.g. To solve G we may need G1 and G2. To solve G1 we may need H;
      and to solve G2 we may need H. If we don't spot this sharing we may
      solve H twice; and if this pattern repeats we may get exponentially bad
      behaviour.

    * Suppose we have (#13943)
          class Take (n :: Nat) where ...
          instance {-# OVERLAPPING #-}                    Take 0 where ..
          instance {-# OVERLAPPABLE #-} (Take (n - 1)) => Take n where ..

      And we have [W] Take 3.  That only matches one instance so we get
      [W] Take (3-1).  Then we should reduce the (3-1) to 2, and continue.

(SCS3) When doing short-cut solving we can (and should) inherit the `solved_dicts`
    of the caller (#15164).  You might worry about having a solved-dict that uses
    a Given -- but that too will have been subject to short-cut solving so it's fine.

Note [Shortcut solving: incoherence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This optimization relies on coherence of dictionaries to be correct. When we
cannot assume coherence because of IncoherentInstances then this optimization
can change the behavior of the user's code.

The following four modules produce a program whose output would change depending
on whether we apply this optimization when IncoherentInstances is in effect:

=========
    {-# LANGUAGE MultiParamTypeClasses #-}
    module A where

    class A a where
      int :: a -> Int

    class A a => C a b where
      m :: b -> a -> a

=========
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    module B where

    import A

    instance A a where
      int _ = 1

    instance C a [b] where
      m _ = id

=========
    {-# LANGUAGE FlexibleContexts      #-}
    {-# LANGUAGE FlexibleInstances     #-}
    {-# LANGUAGE IncoherentInstances   #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    module C where

    import A

    instance A Int where
      int _ = 2

    instance C Int [Int] where
      m _ = id

    intC :: C Int a => a -> Int -> Int
    intC _ x = int x

=========
    module Main where

    import A
    import B
    import C

    main :: IO ()
    main = print (intC [] (0::Int))

The output of `main` if we avoid the optimization under the effect of
IncoherentInstances is `1`. If we were to do the optimization, the output of
`main` would be `2`.
-}

tryInertDicts :: DictCt -> SolverStage ()
tryInertDicts :: DictCt -> SolverStage ()
tryInertDicts DictCt
dict_ct
  = TcS (StopOrContinue ()) -> SolverStage ()
TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ do { inerts <- TcS InertCans
getInertCans
               ; try_inert_dicts inerts dict_ct }

try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ())
try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ())
try_inert_dicts InertCans
inerts dict_w :: DictCt
dict_w@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev_w, di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
  | Just DictCt
dict_i <- InertCans -> Class -> [Type] -> Maybe DictCt
lookupInertDict InertCans
inerts Class
cls [Type]
tys
  , let ev_i :: CtEvidence
ev_i  = DictCt -> CtEvidence
dictCtEvidence DictCt
dict_i
        loc_i :: CtLoc
loc_i = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_i
        loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
  = -- There is a matching dictionary in the inert set
    do { -- For a Wanted, first to try to solve it /completely/ from top level instances
         -- See Note [Shortcut solving]
       ; short_cut_worked <- Bool -> DictCt -> TcS Bool
tryShortCutSolver (CtEvidence -> Bool
isGiven CtEvidence
ev_i) DictCt
dict_w

       ; if | short_cut_worked
            -> stopWith ev_w "shortCutSolver worked(1)"

            -- Next see if we are in "loopy-superclass" land.  If so,
            -- we don't want to replace the (Given) inert with the
            -- (Wanted) work-item, or vice versa; we want to hang on
            -- to both, and try to solve the work-item via an instance.
            -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
            | prohibitedSuperClassSolve loc_i loc_w
            -> continueWith ()

            | otherwise -- We can either solve the inert from the work-item or vice-versa.
            -> case solveOneFromTheOther (CDictCan dict_i) (CDictCan dict_w) of
                 InteractResult
KeepInert -> do { String -> SDoc -> TcS ()
traceTcS String
"lookupInertDict:KeepInert" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_w)
                                 ; CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setDictIfWanted CtEvidence
ev_w CanonicalEvidence
EvCanonical (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_i)
                                 ; StopOrContinue () -> TcS (StopOrContinue ())
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (StopOrContinue () -> TcS (StopOrContinue ()))
-> StopOrContinue () -> TcS (StopOrContinue ())
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc -> StopOrContinue ()
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev_w (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Dict equal" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_w) }
                 InteractResult
KeepWork  -> do { String -> SDoc -> TcS ()
traceTcS String
"lookupInertDict:KeepWork" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_w)
                                 ; CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setDictIfWanted CtEvidence
ev_i CanonicalEvidence
EvCanonical (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_w)
                                 ; (InertCans -> InertCans) -> TcS ()
updInertCans ((DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
updDicts ((DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans)
-> (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$ DictCt -> DictMap DictCt -> DictMap DictCt
forall a. DictCt -> DictMap a -> DictMap a
delDict DictCt
dict_w)
                                 ; () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () } }

  | Bool
otherwise
  = do { String -> SDoc -> TcS ()
traceTcS String
"tryInertDicts:no" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_w SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
       ; () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () }

-- See Note [Shortcut solving]
tryShortCutSolver :: Bool       -- True <=> try the short-cut solver; False <=> don't
                  -> DictCt     -- Work item
                  -> TcS Bool   -- True <=> success
-- We are about to solve a [W] constraint from a [G] constraint. We take
-- a moment to see if we can get a better solution using an instance.
-- Note that we only do this for the sake of performance. Exactly the same
-- programs should typecheck regardless of whether we take this step or
-- not. See Note [Shortcut solving]
tryShortCutSolver :: Bool -> DictCt -> TcS Bool
tryShortCutSolver Bool
try_short_cut dict_w :: DictCt
dict_w@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev_w })
  | Bool -> Bool
not Bool
try_short_cut
  = Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  | Bool
otherwise
  = do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
       ; if | CtWanted (WantedCt { ctev_pred = pred_w }) <- ev_w

            , not (couldBeIPLike pred_w)   -- Not for implicit parameters (#18627)

            , not (xopt LangExt.IncoherentInstances dflags)
              -- If IncoherentInstances is on then we cannot rely on coherence of proofs
              -- in order to justify this optimization: The proof provided by the
              -- [G] constraint's superclass may be different from the top-level proof.
              -- See Note [Shortcut solving: incoherence]

            , gopt Opt_SolveConstantDicts dflags
              -- Enabled by the -fsolve-constant-dicts flag

            -> tryShortCutTcS $  -- tryTcS tries to completely solve some contraints
               do { residual <- solveSimpleWanteds (unitBag (CDictCan dict_w))
                  ; return (isEmptyWC residual) }

            | otherwise
            -> return False }


{- *******************************************************************
*                                                                    *
         Top-level reaction for class constraints (CDictCan)
*                                                                    *
**********************************************************************-}

tryInstances :: DictCt -> SolverStage ()
tryInstances :: DictCt -> SolverStage ()
tryInstances DictCt
dict_ct
  = TcS (StopOrContinue ()) -> SolverStage ()
TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ do { inerts <- TcS InertSet
getInertSet
               ; try_instances inerts dict_ct }

try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ())
-- Try to use type-class instance declarations to simplify the constraint

-- Case for Givens
-- Never use instances for Given constraints
try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ())
try_instances InertSet
_ (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtGiven {} })
  = -- See Note [No Given/Given fundeps]
    () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith ()

-- Case for Wanteds
try_instances InertSet
inerts work_item :: DictCt
work_item@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = ev :: CtEvidence
ev@(CtWanted WantedCtEvidence
wev), di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
xis })
  | Just CtEvidence
solved_ev <- InertSet -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict InertSet
inerts Class
cls [Type]
xis   -- Cached
  = do { CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setDictIfWanted CtEvidence
ev CanonicalEvidence
EvCanonical (CtEvidence -> EvTerm
ctEvTerm CtEvidence
solved_ev)
       ; CtEvidence -> String -> TcS (StopOrContinue ())
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Dict/Top (cached)" }

  | Bool
otherwise  -- Wanted, but not cached
   = do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
        ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
        ; case lkup_res of
               OneInst { cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }
                  -> do { let is_local_given :: Bool
is_local_given = case InstanceWhat
what of { InstanceWhat
LocalInstance -> Bool
True; InstanceWhat
_ -> Bool
False }
                        ; take_shortcut <- Bool -> DictCt -> TcS Bool
tryShortCutSolver Bool
is_local_given DictCt
work_item
                        ; if take_shortcut
                          then stopWith ev "shortCutSolver worked(2)"
                          else do { insertSafeOverlapFailureTcS what work_item
                                  ; updSolvedDicts what work_item
                                  ; chooseInstance wev lkup_res
                                  ; stopWith ev "Dict/Top (solved wanted)" } }
               ClsInstResult
_  -> -- NoInstance or NotSure: we didn't solve it
                     () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () }
   where
     dict_loc :: CtLoc
dict_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev

chooseInstance :: WantedCtEvidence -> ClsInstResult -> TcS ()
chooseInstance :: WantedCtEvidence -> ClsInstResult -> TcS ()
chooseInstance work_item :: WantedCtEvidence
work_item@(WantedCt { ctev_dest :: WantedCtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest, ctev_rewriters :: WantedCtEvidence -> CoHoleSet
ctev_rewriters = CoHoleSet
rws
                                   , ctev_loc :: WantedCtEvidence -> CtLoc
ctev_loc = CtLoc
loc, ctev_pred :: WantedCtEvidence -> Type
ctev_pred = Type
pred })
               (OneInst { cir_new_theta :: ClsInstResult -> [Type]
cir_new_theta   = [Type]
theta
                        , cir_what :: ClsInstResult -> InstanceWhat
cir_what        = InstanceWhat
what
                        , cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev       = [EvExpr] -> EvTerm
mk_ev
                        , cir_canonical :: ClsInstResult -> CanonicalEvidence
cir_canonical   = CanonicalEvidence
canonical })
  = do { String -> SDoc -> TcS ()
traceTcS String
"doTopReact/found instance for" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ WantedCtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedCtEvidence
work_item
       ; deeper_loc <- CtLoc -> InstanceWhat -> Type -> TcS CtLoc
checkInstanceOK CtLoc
loc InstanceWhat
what Type
pred
       ; checkReductionDepth deeper_loc pred
       ; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar)
                    (ppr work_item)
       ; evc_vars <- mapM (newWanted deeper_loc rws) theta
       ; setWantedDict dest canonical (mk_ev (map getEvExpr evc_vars))
       ; emitWorkNC (map CtWanted $ freshGoals evc_vars) }

chooseInstance WantedCtEvidence
work_item ClsInstResult
lookup_res
  = String -> SDoc -> TcS ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"chooseInstance" (WantedCtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedCtEvidence
work_item SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
lookup_res)

checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
-- Check that it's OK to use this instance:
--    (a) the use is well staged in the Template Haskell sense
-- Returns the CtLoc to used for sub-goals
-- Probably also want to call checkReductionDepth
checkInstanceOK :: CtLoc -> InstanceWhat -> Type -> TcS CtLoc
checkInstanceOK CtLoc
loc InstanceWhat
what Type
pred
  = do { CtLoc -> InstanceWhat -> Type -> TcS ()
checkWellLevelledDFun CtLoc
loc InstanceWhat
what Type
pred
       ; CtLoc -> TcS CtLoc
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return CtLoc
deeper_loc }
  where
     deeper_loc :: CtLoc
deeper_loc = CtLoc -> CtLoc
zap_origin (CtLoc -> CtLoc
bumpCtLocDepth CtLoc
loc)
     origin :: CtOrigin
origin     = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc

     zap_origin :: CtLoc -> CtLoc
zap_origin CtLoc
loc  -- After applying an instance we can set ScOrigin to
                     -- NotNakedSc, so that prohibitedSuperClassSolve never fires
                     -- See Note [Solving superclass constraints] in
                     -- GHC.Tc.TyCl.Instance, (sc1).
       | ScOrigin ClsInstOrQC
what NakedScFlag
_ <- CtOrigin
origin
       = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc (ClsInstOrQC -> NakedScFlag -> CtOrigin
ScOrigin ClsInstOrQC
what NakedScFlag
NotNakedSc)
       | Bool
otherwise
       = CtLoc
loc

matchClassInst :: DynFlags -> InertSet
               -> Class -> [Type]
               -> CtLoc -> TcS ClsInstResult
matchClassInst :: DynFlags
-> InertSet -> Class -> [Type] -> CtLoc -> TcS ClsInstResult
matchClassInst DynFlags
dflags InertSet
inerts Class
clas [Type]
tys CtLoc
loc
-- First check whether there is an in-scope Given that could
-- match this constraint.  In that case, do not use any instance
-- whether top level, or local quantified constraints.
-- See Note [Instance and Given overlap] and see
-- (IL0) in Note [Rules for instance lookup] in GHC.Core.InstEnv
  | Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances DynFlags
dflags)
  , Bool -> Bool
not (Class -> Bool
isCTupleClass Class
clas)
        -- It is always safe to unpack constraint tuples
        -- And if we don't do so, we may never solve it at all
        -- See Note [Solving tuple constraints]
  , Bool -> Bool
not (InertSet -> CtLoc -> Class -> [Type] -> Bool
noMatchableGivenDicts InertSet
inerts CtLoc
loc Class
clas [Type]
tys)
  = do { String -> SDoc -> TcS ()
traceTcS String
"Delaying instance application" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
           [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Work item:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Class -> [Type] -> SDoc
pprClassPred Class
clas [Type]
tys ]
       ; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NotSure }

  | Bool
otherwise
  = do { String -> SDoc -> TcS ()
traceTcS String
"matchClassInst" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pred =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'{'
       ; local_res <- Type -> CtLoc -> TcS ClsInstResult
matchLocalInst Type
pred CtLoc
loc
       ; case local_res of
           OneInst {} ->  -- See Note [Local instances and incoherence]
                do { String -> SDoc -> TcS ()
traceTcS String
"} matchClassInst local match" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
local_res
                   ; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
local_res }

           ClsInstResult
NotSure -> -- In the NotSure case for local instances
                      -- we don't want to try global instances
                do { String -> SDoc -> TcS ()
traceTcS String
"} matchClassInst local not sure" SDoc
forall doc. IsOutput doc => doc
empty
                   ; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
local_res }

           ClsInstResult
NoInstance  -- No local instances, so try global ones
              -> do { global_res <- DynFlags -> Class -> [Type] -> CtLoc -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Class
clas [Type]
tys CtLoc
loc
                    ; warn_custom_warn_instance global_res loc
                          -- See Note [Implementation of deprecated instances]
                    ; traceTcS "} matchClassInst global result" $ ppr global_res
                    ; return global_res } }
  where
    pred :: Type
pred = Class -> [Type] -> Type
mkClassPred Class
clas [Type]
tys

-- | Returns True iff there are no Given constraints that might,
-- potentially, match the given class constraint. This is used when checking to see if a
-- Given might overlap with an instance. See Note [Instance and Given overlap]
-- in GHC.Tc.Solver.Dict
noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool
noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [Type] -> Bool
noMatchableGivenDicts inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans }) CtLoc
loc_w Class
clas [Type]
tys
  = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (DictCt -> Bool) -> Bag DictCt -> Bool
forall a. (a -> Bool) -> Bag a -> Bool
anyBag DictCt -> Bool
matchable_given (Bag DictCt -> Bool) -> Bag DictCt -> Bool
forall a b. (a -> b) -> a -> b
$
    DictMap DictCt -> Class -> Bag DictCt
forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> DictMap DictCt
inert_dicts InertCans
inert_cans) Class
clas
  where
    pred_w :: Type
pred_w = Class -> [Type] -> Type
mkClassPred Class
clas [Type]
tys

    matchable_given :: DictCt -> Bool
    matchable_given :: DictCt -> Bool
matchable_given (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev })
      | CtGiven (GivenCt { ctev_loc :: GivenCtEvidence -> CtLoc
ctev_loc = CtLoc
loc_g, ctev_pred :: GivenCtEvidence -> Type
ctev_pred = Type
pred_g }) <- CtEvidence
ev
      = Maybe Subst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$ InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inerts Type
pred_g CtLoc
loc_g Type
pred_w CtLoc
loc_w

      | Bool
otherwise
      = Bool
False

{- Note [Implementation of deprecated instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This note describes the implementation of the deprecated instances GHC proposal
  https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0575-deprecated-instances.rst

In the parser, we parse deprecations/warnings attached to instances:

  instance {-# DEPRECATED "msg" #-} Show X
  deriving instance {-# WARNING "msg2" #-} Eq Y

(Note that non-standalone deriving instance declarations do not support this mechanism.)
(Note that the DEPRECATED and WARNING pragmas can be used here interchangeably.)

We store the resulting warning message in the extension field of `ClsInstDecl`
(respectively, `DerivDecl`; See Note [Trees That Grow]).

In `GHC.Tc.TyCl.Instance.tcClsInstDecl` (respectively, `GHC.Tc.Deriv.Utils.newDerivClsInst`),
we pass on that information to `ClsInst` (and eventually store it in `IfaceClsInst` too).

Next, if we solve a constraint using such an instance, in
`GHC.Tc.Instance.Class.matchInstEnv`, we pass it further into the
`Ghc.Tc.Types.Origin.InstanceWhat`.

Finally, if the instance solving function `GHC.Tc.Solver.Monad.matchGlobalInst` returns
a `Ghc.Tc.Instance.Class.ClsInstResult` with `Ghc.Tc.Types.Origin.InstanceWhat` containing
a warning, when called from either `matchClassInst` or `shortCutSolver`, we call
`warn_custom_warn_instance` that ultimately emits the warning if needed.

Note that we only emit a warning when the instance is used in a different module
than it is defined, which keeps the behaviour in line with the deprecation of
top-level identifiers.
-}

-- | Emits the custom warning for a deprecated instance
--
-- See Note [Implementation of deprecated instances]
warn_custom_warn_instance :: ClsInstResult -> CtLoc -> TcS ()
warn_custom_warn_instance :: ClsInstResult -> CtLoc -> TcS ()
warn_custom_warn_instance (OneInst{ cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }) CtLoc
ct_loc
  | TopLevInstance{ iw_dfun_id :: InstanceWhat -> EvVar
iw_dfun_id = EvVar
dfun, iw_warn :: InstanceWhat -> Maybe (WarningTxt GhcRn)
iw_warn = Just WarningTxt GhcRn
warn } <- InstanceWhat
what = do
      let mod :: Module
mod = HasDebugCallStack => Name -> Module
Name -> Module
nameModule (Name -> Module) -> Name -> Module
forall a b. (a -> b) -> a -> b
$ EvVar -> Name
forall a. NamedThing a => a -> Name
getName EvVar
dfun
      this_mod <- TcS Module
forall (m :: * -> *). HasModule m => m Module
getModule
      when (this_mod /= mod)
          -- We don't emit warnings for usages inside of the same module
          -- to prevent it being triggered for instance child declarations
        $ ctLocWarnTcS ct_loc
          $ TcRnPragmaWarning
              { pragma_warning_info = PragmaWarningInstance dfun (ctl_origin ct_loc)
              , pragma_warning_msg  = warn }
warn_custom_warn_instance ClsInstResult
_ CtLoc
_ = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

{- Note [Instance and Given overlap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Example, from the OutsideIn(X) paper:
       instance P x => Q [x]
       instance (x ~ y) => R y [x]

       wob :: forall a b. (Q [b], R b a) => a -> Int

       g :: forall a. Q [a] => [a] -> Int
       g x = wob x

From 'g' we get the implication constraint:
            forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its top-level axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the top-level we get  (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].

The partial solution is that:
  In matchClassInst (and thus in topReact), we return a matching
  instance only when there is no Given in the inerts which is
  unifiable to this particular dictionary.

  We treat any meta-tyvar as "unifiable" for this purpose,
  *including* untouchable ones.  But not skolems like 'a' in
  the implication constraint above.

The end effect is that, much as we do for overlapping instances, we
delay choosing a class instance if there is a possibility of another
instance OR a given to match our constraint later on. This fixes
tickets #4981 and #5002.

Other notes:

* The check is done *first*, so that it also covers classes
  with built-in instance solving, such as
     - constraint tuples
     - natural numbers
     - Typeable

* See also Note [What might equal later?] in GHC.Tc.Utils.Unify

* The given-overlap problem is arguably not easy to appear in practice
  due to our aggressive prioritization of equality solving over other
  constraints, but it is possible. I've added a test case in
  typecheck/should-compile/GivenOverlapping.hs

* Another "live" example is #10195; another is #10177.

* We ignore the overlap problem if -XIncoherentInstances is in force:
  see #6002 for a worked-out example where this makes a
  difference.

* Moreover notice that our goals here are different than the goals of
  the top-level overlapping checks. There we are interested in
  validating the following principle:

      If we inline a function f at a site where the same global
      instance environment is available as the instance environment at
      the definition site of f then we should get the same behaviour.

  But for the Given Overlap check our goal is just related to completeness of
  constraint solving.

* The solution is only a partial one.  Consider the above example with
       g :: forall a. Q [a] => [a] -> Int
       g x = let v = wob x
             in v
  and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
  general type for 'v'.  When generalising v's type we'll simplify its
  Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
  will use the instance declaration after all. #11948 was a case
  in point.

All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].


Note [Local instances and incoherence]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
   f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
                 => c b -> Bool
   f x = x==x

We get [W] Eq (c b), and we must use the local instance to solve it.

BUT that wanted also unifies with the top-level Eq [a] instance,
and Eq (Maybe a) etc.  We want the local instance to "win", otherwise
we can't solve the wanted at all.  So we mark it as Incohherent.
According to Note [Rules for instance lookup] in GHC.Core.InstEnv, that'll
make it win even if there are other instances that unify.

Moreover this is not a hack!  The evidence for this local instance
will be constructed by GHC at a call site... from the very instances
that unify with it here.  It is not like an incoherent user-written
instance which might have utterly different behaviour.

Consider  f :: Eq a => blah.  If we have [W] Eq a, we certainly
get it from the Eq a context, without worrying that there are
lots of top-level instances that unify with [W] Eq a!  We'll use
those instances to build evidence to pass to f. That's just the
nullary case of what's happening here.
-}

matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
-- Look up the predicate in Given quantified constraints,
-- which are effectively just local instance declarations.
matchLocalInst :: Type -> CtLoc -> TcS ClsInstResult
matchLocalInst Type
body_pred CtLoc
loc
  = do { -- Look in the inert set for a matching Given quantified constraint
         inerts@(IS { inert_cans = ics }) <- TcS InertSet
getInertSet
       ; case match_local_inst inerts (inert_qcis ics) of
            { ([], []) -> do { String -> SDoc -> TcS ()
traceTcS String
"No local instance for" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_pred)
                             ; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance }
            ; ([(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs) ->

    do { -- Find the best match
         -- See Note [Use only the best matching quantified constraint]
         matches <- ((CtEvidence, [DFunInstType]) -> TcS InstDFun)
-> [(CtEvidence, [DFunInstType])] -> TcS [InstDFun]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun [(CtEvidence, [DFunInstType])]
matches
       ; unifs   <- mapM mk_instDFun unifs
       ; case dominatingMatch matches of
          { Just (EvVar
dfun_id, [Type]
tys, [Type]
theta)
            | (InstDFun -> Bool) -> [InstDFun] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (([Type]
theta [Type] -> [Type] -> Bool
`impliedBySCs`) ([Type] -> Bool) -> (InstDFun -> [Type]) -> InstDFun -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstDFun -> [Type]
forall a b c. (a, b, c) -> c
thdOf3) [InstDFun]
unifs
            ->
            do { let result :: ClsInstResult
result = OneInst { cir_new_theta :: [Type]
cir_new_theta   = [Type]
theta
                                      , cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev       = EvVar -> [Type] -> [EvExpr] -> EvTerm
evDFunApp EvVar
dfun_id [Type]
tys
                                      , cir_canonical :: CanonicalEvidence
cir_canonical   = CanonicalEvidence
EvCanonical
                                      , cir_what :: InstanceWhat
cir_what        = InstanceWhat
LocalInstance }
               ; String -> SDoc -> TcS ()
traceTcS String
"Best local instance found:" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
                  [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"body_pred:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_pred
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"result:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
result
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"matches:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
matches
                       , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"unifs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
unifs ]
               ; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
result }

          ; Maybe InstDFun
mb_best ->
            do { String -> SDoc -> TcS ()
traceTcS String
"Multiple local instances; not committing to any"
                  (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"body_pred:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_pred
                         , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"matches:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
matches
                         , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"unifs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
unifs
                         , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"best_match:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Maybe InstDFun -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe InstDFun
mb_best ]
               ; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NotSure }}}}}
  where
    body_pred_tv_set :: TyCoVarSet
body_pred_tv_set = Type -> TyCoVarSet
tyCoVarsOfType Type
body_pred

    mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun
    mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun (CtEvidence
ev, [DFunInstType]
tys) =
      let dfun_id :: EvVar
dfun_id = CtEvidence -> EvVar
ctEvEvId CtEvidence
ev
      in do { (tys, theta) <- EvVar -> [DFunInstType] -> TcS ([Type], [Type])
instDFunType (CtEvidence -> EvVar
ctEvEvId CtEvidence
ev) [DFunInstType]
tys
            ; return (dfun_id, tys, theta) }

    -- Compute matching and unifying local instances
    match_local_inst :: InertSet
                     -> [QCInst]
                     -> ( [(CtEvidence, [DFunInstType])]
                        , [(CtEvidence, [DFunInstType])] )
    match_local_inst :: InertSet
-> [QCInst]
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
match_local_inst InertSet
_inerts []
      = ([], [])
    match_local_inst InertSet
inerts (qci :: QCInst
qci@(QCI { qci_tvs :: QCInst -> [EvVar]
qci_tvs  = [EvVar]
qtvs
                                      , qci_body :: QCInst -> Type
qci_body = Type
qbody
                                      , qci_ev :: QCInst -> CtEvidence
qci_ev   = CtEvidence
qev })
                            : [QCInst]
qcis)
      | CtEvidence -> Bool
isWanted CtEvidence
qev    -- Skip Wanteds
      = InertSet
-> [QCInst]
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
match_local_inst InertSet
inerts [QCInst]
qcis

      | let in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet
qtv_set TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
body_pred_tv_set)
      , Just TvSubstEnv
tv_subst <- TyCoVarSet
-> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
ruleMatchTyKiX TyCoVarSet
qtv_set (InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope)
                                        TvSubstEnv
emptyTvSubstEnv Type
qbody Type
body_pred
      , let match :: (CtEvidence, [DFunInstType])
match = (CtEvidence
qev, (EvVar -> DFunInstType) -> [EvVar] -> [DFunInstType]
forall a b. (a -> b) -> [a] -> [b]
map (TvSubstEnv -> EvVar -> DFunInstType
forall a. VarEnv a -> EvVar -> Maybe a
lookupVarEnv TvSubstEnv
tv_subst) [EvVar]
qtvs)
      = ((CtEvidence, [DFunInstType])
match(CtEvidence, [DFunInstType])
-> [(CtEvidence, [DFunInstType])] -> [(CtEvidence, [DFunInstType])]
forall a. a -> [a] -> [a]
:[(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs)

      | Bool
otherwise
      = Bool
-> SDoc
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCoVarSet -> TyCoVarSet -> Bool
disjointVarSet TyCoVarSet
qtv_set (Type -> TyCoVarSet
tyCoVarsOfType Type
body_pred))
                  (QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr QCInst
qci SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_pred)
            -- ASSERT: unification relies on the
            -- quantified variables being fresh
        ([(CtEvidence, [DFunInstType])]
matches, Maybe (CtEvidence, [DFunInstType])
this_unif Maybe (CtEvidence, [DFunInstType])
-> [(CtEvidence, [DFunInstType])] -> [(CtEvidence, [DFunInstType])]
forall {a}. Maybe a -> [a] -> [a]
`combine` [(CtEvidence, [DFunInstType])]
unifs)
      where
        qloc :: CtLoc
qloc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
qev
        qtv_set :: TyCoVarSet
qtv_set = [EvVar] -> TyCoVarSet
mkVarSet [EvVar]
qtvs
        ([(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs) = InertSet
-> [QCInst]
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
match_local_inst InertSet
inerts [QCInst]
qcis
        this_unif :: Maybe (CtEvidence, [DFunInstType])
this_unif
          | Just Subst
subst <- InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inerts Type
qbody CtLoc
qloc Type
body_pred CtLoc
loc
          = (CtEvidence, [DFunInstType]) -> Maybe (CtEvidence, [DFunInstType])
forall a. a -> Maybe a
Just (CtEvidence
qev, (EvVar -> DFunInstType) -> [EvVar] -> [DFunInstType]
forall a b. (a -> b) -> [a] -> [b]
map  (Subst -> EvVar -> DFunInstType
lookupTyVar Subst
subst) [EvVar]
qtvs)
          | Bool
otherwise
          = Maybe (CtEvidence, [DFunInstType])
forall a. Maybe a
Nothing

        combine :: Maybe a -> [a] -> [a]
combine Maybe a
Nothing  [a]
us = [a]
us
        combine (Just a
u) [a]
us = a
u a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
us

-- | Instance dictionary function and type.
type InstDFun = (DFunId, [TcType], TcThetaType)

-- | Try to find a local quantified instance that dominates all others,
-- i.e. which has a weaker instance context than all the others.
--
-- See Note [Use only the best matching quantified constraint].
dominatingMatch :: [InstDFun] -> Maybe InstDFun
dominatingMatch :: [InstDFun] -> Maybe InstDFun
dominatingMatch [InstDFun]
matches =
  [InstDFun] -> Maybe InstDFun
forall a. [a] -> Maybe a
listToMaybe ([InstDFun] -> Maybe InstDFun) -> [InstDFun] -> Maybe InstDFun
forall a b. (a -> b) -> a -> b
$ ((InstDFun, [InstDFun]) -> Maybe InstDFun)
-> [(InstDFun, [InstDFun])] -> [InstDFun]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((InstDFun -> [InstDFun] -> Maybe InstDFun)
-> (InstDFun, [InstDFun]) -> Maybe InstDFun
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry InstDFun -> [InstDFun] -> Maybe InstDFun
go) ([InstDFun] -> [(InstDFun, [InstDFun])]
forall a. [a] -> [(a, [a])]
holes [InstDFun]
matches)
  -- listToMaybe: arbitrarily pick any one context that is weaker than
  -- all others, e.g. so that we can handle [Eq a, Num a] vs [Num a, Eq a]
  -- (see test case T22223).

  where
    go :: InstDFun -> [InstDFun] -> Maybe InstDFun
    go :: InstDFun -> [InstDFun] -> Maybe InstDFun
go InstDFun
this [] = InstDFun -> Maybe InstDFun
forall a. a -> Maybe a
Just InstDFun
this
    go this :: InstDFun
this@(EvVar
_,[Type]
_,[Type]
this_theta) ((EvVar
_,[Type]
_,[Type]
other_theta):[InstDFun]
others)
      | [Type]
this_theta [Type] -> [Type] -> Bool
`impliedBySCs` [Type]
other_theta
      = InstDFun -> [InstDFun] -> Maybe InstDFun
go InstDFun
this [InstDFun]
others
      | Bool
otherwise
      = Maybe InstDFun
forall a. Maybe a
Nothing

-- | Whether a collection of constraints is implied by another collection,
-- according to a simple superclass check.
--
-- See Note [When does a quantified instance dominate another?].
impliedBySCs :: TcThetaType -> TcThetaType -> Bool
impliedBySCs :: [Type] -> [Type] -> Bool
impliedBySCs [Type]
c1 [Type]
c2 = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
in_c2 [Type]
c1
  where
    in_c2 :: TcPredType -> Bool
    in_c2 :: Type -> Bool
in_c2 Type
pred = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Type
pred HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType`) [Type]
c2_expanded

    c2_expanded :: [TcPredType]  -- Includes all superclasses
    c2_expanded :: [Type]
c2_expanded = [ Type
q | Type
p <- [Type]
c2, Type
q <- Type
p Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type -> [Type]
transSuperClasses Type
p ]


{- Note [When does a quantified instance dominate another?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When matching local quantified instances, it's useful to be able to pick
the one with the weakest precondition, e.g. if one has both

  [G] d1: forall a b. ( Eq a, Num b, C a b  ) => D a b
  [G] d2: forall a  .                C a Int  => D a Int
  [W] {w}: D a Int

Then it makes sense to use d2 to solve w, as doing so we end up with a strictly
weaker proof obligation of `C a Int`, compared to `(Eq a, Num Int, C a Int)`
were we to use d1.

In theory, to compute whether one context implies another, we would need to
recursively invoke the constraint solver. This is expensive, so we instead do
a simple check using superclasses, implemented in impliedBySCs.

Examples:

 - [Eq a] is implied by [Ord a]
 - [Ord a] is not implied by [Eq a],
 - any context is implied by itself,
 - the empty context is implied by any context.

Note [Use only the best matching quantified constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#20582) the ambiguity check for
  (forall a. Ord (m a), forall a. Semigroup a => Eq (m a)) => m Int

Because of eager expansion of given superclasses, we get
  [G] d1: forall a. Ord (m a)
  [G] d2: forall a. Eq (m a)
  [G] d3: forall a. Semigroup a => Eq (m a)

  [W] {w1}: forall a. Ord (m a)
  [W] {w2}: forall a. Semigroup a => Eq (m a)

The first wanted is solved straightforwardly. But the second wanted
matches *two* local instances: d2 and d3. Our general rule around multiple local
instances is that we refuse to commit to any of them. However, that
means that our type fails the ambiguity check. That's bad: the type
is perfectly fine. (This actually came up in the wild, in the streamly
library.)

The solution is to prefer local instances which are easier to prove, meaning
that they have a weaker precondition. In this case, the empty context
of d2 is a weaker constraint than the "Semigroup a" context of d3, so we prefer
using it when proving w2. This allows us to pass the ambiguity check here.

Our criterion for solving a Wanted by matching local quantified instances is
thus as follows:

  - There is a matching local quantified instance that dominates all others
    matches, in the sense of [When does a quantified instance dominate another?].
    Any such match do, we pick it arbitrarily (the T22223 example below says why).
  - This local quantified instance also dominates all the unifiers, as we
    wouldn't want to commit to a single match when we might have multiple,
    genuinely different matches after further unification takes place.

Some other examples:


  #15244:

    f :: (C g, D g) => ....
    class S g => C g where ...
    class S g => D g where ...
    class (forall a. Eq a => Eq (g a)) => S g where ...

  Here, in f's RHS, there are two identical quantified constraints
  available, one via the superclasses of C and one via the superclasses
  of D. Given that each implies the other, we pick one arbitrarily.


  #22216:

    class Eq a
    class Eq a => Ord a
    class (forall b. Eq b => Eq (f b)) => Eq1 f
    class (Eq1 f, forall b. Ord b => Ord (f b)) => Ord1 f

  Suppose we have

    [G] d1: Ord1 f
    [G] d2: Eq a
    [W] {w}: Eq (f a)

  Superclass expansion of d1 gives us:

    [G] d3 : Eq1 f
    [G] d4 : forall b. Ord b => Ord (f b)

  expanding d4 and d5 gives us, respectively:

    [G] d5 : forall b. Eq  b => Eq (f b)
    [G] d6 : forall b. Ord b => Eq (f b)

  Now we have two matching local instances that we could use when solving the
  Wanted. However, it's obviously silly to use d6, given that d5 provides us with
  as much information, with a strictly weaker precondition. So we pick d5 to solve
  w. If we chose d6, we would get [W] Ord a, which in this case we can't solve.


  #22223:

    [G] forall a b. (Eq a, Ord b) => C a b
    [G] forall a b. (Ord b, Eq a) => C a b
    [W] C x y

  Here we should be free to pick either quantified constraint, as they are
  equivalent up to re-ordering of the constraints in the context.
  See also Note [Do not add duplicate quantified instances]
  in GHC.Tc.Solver.Monad.

Test cases:
  typecheck/should_compile/T20582
  quantified-constraints/T15244
  quantified-constraints/T22216{a,b,c,d,e}
  quantified-constraints/T22223

Historical note: a previous solution was to instead pick the local instance
with the least superclass depth (see Note [Replacement vs keeping]),
but that doesn't work for the example from #22216.
-}


{- *********************************************************************
*                                                                      *
*                      Superclasses
*                                                                      *
********************************************************************* -}

{- Note [The superclass story]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to add superclass constraints for two reasons:

* For givens [G], they give us a route to proof.  E.g.
    f :: Ord a => a -> Bool
    f x = x == x
  We get a Wanted (Eq a), which can only be solved from the superclass
  of the Given (Ord a).

* For wanteds [W], they may give useful
  functional dependencies.  E.g.
     class C a b | a -> b where ...
     class C a b => D a b where ...
  Now a [W] constraint (D Int beta) has (C Int beta) as a superclass
  and that might tell us about beta, via C's fundeps.  We can get this
  by generating a [W] (C Int beta) constraint. We won't use the evidence,
  but it may lead to unification.

See Note [Why adding superclasses can help].

For these reasons we want to generate superclass constraints for both
Givens and Wanteds. But:

* (Minor) they are often not needed, so generating them aggressively
  is a waste of time.

* (Major) if we want recursive superclasses, there would be an infinite
  number of them.  Here is a real-life example (#10318);

     class (Frac (Frac a) ~ Frac a,
            Fractional (Frac a),
            IntegralDomain (Frac a))
         => IntegralDomain a where
      type Frac a :: *

  Notice that IntegralDomain has an associated type Frac, and one
  of IntegralDomain's superclasses is another IntegralDomain constraint.

So here's the plan:

1. Eagerly generate superclasses for given (but not wanted)
   constraints; see Note [Eagerly expand given superclasses].
   This is done using mkStrictSuperClasses in canDictCt, when
   we take a non-canonical Given constraint and cannonicalise it.

   However stop if you encounter the same class twice.  That is,
   mkStrictSuperClasses expands eagerly, but has a conservative
   termination condition: see Note [Expanding superclasses] in GHC.Tc.Utils.TcType.

2. Solve the wanteds as usual, but do no further expansion of
   superclasses for canonical CDictCans in solveSimpleGivens or
   solveSimpleWanteds; Note [Danger of adding superclasses during solving]

   However, /do/ continue to eagerly expand superclasses for new /given/
   /non-canonical/ constraints (canDictCt does this).  As #12175
   showed, a type-family application can expand to a class constraint,
   and we want to see its superclasses for just the same reason as
   Note [Eagerly expand given superclasses].

3. If we have any remaining unsolved wanteds
        (see Note [When superclasses help] in GHC.Tc.Types.Constraint)
   try harder: take both the Givens and Wanteds, and expand
   superclasses again.  See the calls to expandSuperClasses in
   GHC.Tc.Solver.simpl_loop and solveWanteds.

   This may succeed in generating (a finite number of) extra Givens,
   and extra Wanteds. Both may help the proof.

3a An important wrinkle: only expand Givens from the current level.
   Two reasons:
      - We only want to expand it once, and that is best done at
        the level it is bound, rather than repeatedly at the leaves
        of the implication tree
      - We may be inside a type where we can't create term-level
        evidence anyway, so we can't superclass-expand, say,
        (a ~ b) to get (a ~# b).  This happened in #15290.

4. Go round to (2) again.  This loop (2,3,4) is implemented
   in GHC.Tc.Solver.simpl_loop.

The cc_pend_sc field in a CDictCan records whether the superclasses of
this constraint have been expanded.  Specifically, in Step 3 we only
expand superclasses for constraints with cc_pend_sc > 0
(i.e. isPendingScDict holds).
See Note [Expanding Recursive Superclasses and ExpansionFuel]

Why do we do this?  Two reasons:

* To avoid repeated work, by repeatedly expanding the superclasses of
  same constraint,

* To terminate the above loop, at least in the -XNoUndecidableSuperClasses
  case.  If there are recursive superclasses we could, in principle,
  expand forever, always encountering new constraints.

When we take a CNonCanonical or CIrredCan, but end up classifying it
as a CDictCan, we set the cc_pend_sc flag to False.

Note [Superclass loops]
~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
  class C a => D a
  class D a => C a

Then, when we expand superclasses, we'll get back to the self-same
predicate, so we have reached a fixpoint in expansion and there is no
point in fruitlessly expanding further.  This case just falls out from
our strategy.  Consider
  f :: C a => a -> Bool
  f x = x==x
Then canDictCt gets the [G] d1: C a constraint, and eager emits superclasses
G] d2: D a, [G] d3: C a (psc).  (The "psc" means it has its cc_pend_sc has pending
expansion fuel.)
When processing d3 we find a match with d1 in the inert set, and we always
keep the inert item (d1) if possible: see Note [Replacement vs keeping] in
GHC.Tc.Solver.InertSet.  So d3 dies a quick, happy death.

Note [Eagerly expand given superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In step (1) of Note [The superclass story], why do we eagerly expand
Given superclasses by one layer?  (By "one layer" we mean expand transitively
until you meet the same class again -- the conservative criterion embodied
in expandSuperClasses.  So a "layer" might be a whole stack of superclasses.)
We do this eagerly for Givens mainly because of some very obscure
cases like this:

   instance Bad a => Eq (T a)

   f :: (Ord (T a)) => blah
   f x = ....needs Eq (T a), Ord (T a)....

Here if we can't satisfy (Eq (T a)) from the givens we'll use the
instance declaration; but then we are stuck with (Bad a).  Sigh.
This is really a case of non-confluent proofs, but to stop our users
complaining we expand one layer in advance.

See Note [Instance and Given overlap].

We also want to do this if we have

   f :: F (T a) => blah

where
   type instance F (T a) = Ord (T a)

So we may need to do a little work on the givens to expose the
class that has the superclasses.  That's why the superclass
expansion for Givens happens in canDictCt.

This same scenario happens with quantified constraints, whose superclasses
are also eagerly expanded. Test case: typecheck/should_compile/T16502b
These are handled in canForAllNC, analogously to canDictCt.

Note [Why adding superclasses can help]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Examples of how adding superclasses can help:

    --- Example 1
        class C a b | a -> b
    Suppose we want to solve
         [G] C a b
         [W] C a beta
    Then adding [W] beta~b will let us solve it.

    -- Example 2 (similar but using a type-equality superclass)
        class (F a ~ b) => C a b
    And try to sllve:
         [G] C a b
         [W] C a beta
    Follow the superclass rules to add
         [G] F a ~ b
         [W] F a ~ beta
    Now we get [W] beta ~ b, and can solve that.

    -- Example (tcfail138)
      class L a b | a -> b
      class (G a, L a b) => C a b

      instance C a b' => G (Maybe a)
      instance C a b  => C (Maybe a) a
      instance L (Maybe a) a

    When solving the superclasses of the (C (Maybe a) a) instance, we get
      [G] C a b, and hence by superclasses, [G] G a, [G] L a b
      [W] G (Maybe a)
    Use the instance decl to get
      [W] C a beta
    Generate its superclass
      [W] L a beta.  Now using fundeps, combine with [G] L a b to get
      [W] beta ~ b
    which is what we want.

Note [Danger of adding superclasses during solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here's a serious, but now out-dated example, from #4497:

   class Num (RealOf t) => Normed t
   type family RealOf x

Assume the generated wanted constraint is:
   [W] RealOf e ~ e
   [W] Normed e

If we were to be adding the superclasses during simplification we'd get:
   [W] RealOf e ~ e
   [W] Normed e
   [W] RealOf e ~ fuv
   [W] Num fuv
==>
   e := fuv, Num fuv, Normed fuv, RealOf fuv ~ fuv

While looks exactly like our original constraint. If we add the
superclass of (Normed fuv) again we'd loop.  By adding superclasses
definitely only once, during canonicalisation, this situation can't
happen.

Note [Nested quantified constraint superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (typecheck/should_compile/T17202)

  class C1 a
  class (forall c. C1 c) => C2 a
  class (forall b. (b ~ F a) => C2 a) => C3 a

Elsewhere in the code, we get a [G] g1 :: C3 a. We expand its superclass
to get [G] g2 :: (forall b. (b ~ F a) => C2 a). This constraint has a
superclass, as well. But we now must be careful: we cannot just add
(forall c. C1 c) as a Given, because we need to remember g2's context.
That new constraint is Given only when forall b. (b ~ F a) is true.

It's tempting to make the new Given be (forall b. (b ~ F a) => forall c. C1 c),
but that's problematic, because it's nested, and ForAllPred is not capable
of representing a nested quantified constraint. (We could change ForAllPred
to allow this, but the solution in this Note is much more local and simpler.)

So, we swizzle it around to get (forall b c. (b ~ F a) => C1 c).

More generally, if we are expanding the superclasses of
  g0 :: forall tvs. theta => cls tys
and find a superclass constraint (itself perhaps a quantified constraint)
  forall sc_tvs. sc_theta => sc_inner_pred
we must have a selector
  sel_id :: forall cls_tvs. cls cls_tvs => forall sc_tvs. sc_theta => sc_inner_pred
and thus build
  g_sc :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred
  g_sc = /\ tvs. /\ sc_tvs. \ theta_ids. \ sc_theta_ids.
         sel_id tys (g0 tvs theta_ids) sc_tvs sc_theta_ids

Actually, we cheat a bit by eta-reducing: note that sc_theta_ids are both the
last bound variables and the last arguments. This avoids the need to produce
the sc_theta_ids at all. So our final construction is

  g_sc = /\ tvs. /\ sc_tvs. \ theta_ids.
         sel_id tys (g0 tvs theta_ids) sc_tvs

(NQCS1) Common case.  If theta_ids[] we get just
     g_sc = /\ tvs. /\sc_tvs. sel_id tys (g0 tvs) sc_tvs
  and can eta-reduce even more to
     g_sc = /\ tvs. sel_id tys (g0 tvs)
  and if tvs=[] we get the straight superclass selection
     g_sc = sel_id tys g0
-}

makeSuperClasses :: [Ct] -> TcS [Ct]
-- Returns strict superclasses, transitively, see Note [The superclass story]
-- The loop-breaking here follows Note [Expanding superclasses] in GHC.Tc.Utils.TcType
-- Specifically, for an incoming (C t) constraint, we return all of (C t)'s
--    superclasses, up to /and including/ the first repetition of C
--
-- Example:  class D a => C a
--           class C [a] => D a
-- makeSuperClasses (C x) will return (D x, C [x])
--
-- NB: the incoming constraint's superclass will consume a unit of fuel
-- Preconditions on `cts`: 1. They are either `CDictCan` or `CQuantCan`
--                         2. Their fuel (stored in cc_pend_sc or qci_pend_sc) is > 0
makeSuperClasses :: [Ct] -> TcS [Ct]
makeSuperClasses [Ct]
cts = (Ct -> TcS [Ct]) -> [Ct] -> TcS [Ct]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM Ct -> TcS [Ct]
go [Ct]
cts
  where
    go :: Ct -> TcS [Ct]
go (CDictCan (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys, di_pend_sc :: DictCt -> ScDepth
di_pend_sc = ScDepth
fuel }))
      = ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPreconditionStrict ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$ -- fuel needs to be more than 0 always
        ScDepth
-> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses ScDepth
fuel CtEvidence
ev [] [] Class
cls [Type]
tys
    go (CQuantCan (QCI { qci_body :: QCInst -> Type
qci_body = Type
body_pred, qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev, qci_pend_sc :: QCInst -> ScDepth
qci_pend_sc = ScDepth
fuel }))
      = Bool -> SDoc -> TcS [Ct] -> TcS [Ct]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type -> Bool
isClassPred Type
body_pred) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
body_pred) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$ -- The cts should all have class pred heads
        ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPreconditionStrict ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$                 -- fuel needs to be more than 0, always
        ScDepth
-> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses ScDepth
fuel CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
      where
        ([EvVar]
tvs, [Type]
theta, Class
cls, [Type]
tys) = Type -> ([EvVar], [Type], Class, [Type])
tcSplitDFunTy (CtEvidence -> Type
ctEvPred CtEvidence
ev)
    go Ct
ct = String -> SDoc -> TcS [Ct]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"makeSuperClasses" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

mkStrictSuperClasses
    :: ExpansionFuel -> CtEvidence
    -> [TyVar] -> ThetaType  -- These two args are non-empty only when taking
                             -- superclasses of a /quantified/ constraint
    -> Class -> [Type] -> TcS [Ct]
-- Return constraints for the strict superclasses of
--   ev :: forall as. theta => cls tys
-- Precondition: fuel > 0
-- Postcondition: fuel for recursive superclass ct is one unit less than cls fuel
mkStrictSuperClasses :: ScDepth
-> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses ScDepth
fuel CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
  = ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_strict_superclasses (ScDepth -> ScDepth
consumeFuel ScDepth
fuel) (Name -> NameSet
unitNameSet (Class -> Name
className Class
cls))
                           CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys

mk_strict_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
                       -> [TyVar] -> ThetaType
                       -> Class -> [Type] -> TcS [Ct]
-- Always return the immediate superclasses of (cls tys);
-- and expand their superclasses, provided none of them are in rec_clss
-- nor are repeated
-- The caller of this function is supposed to perform fuel book keeping
-- Precondition: fuel >= 0
mk_strict_superclasses :: ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_strict_superclasses ScDepth
_ NameSet
_ CtEvidence
_ [EvVar]
_ [Type]
_ Class
cls [Type]
_
  | Class -> Bool
isEqualityClass Class
cls  -- See (EQC1) in Note [Solving equality classes]
  = [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []

mk_strict_superclasses ScDepth
fuel NameSet
rec_clss ev :: CtEvidence
ev@(CtGiven (GivenCt { ctev_evar :: GivenCtEvidence -> EvVar
ctev_evar = EvVar
evar })) [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
  = -- Given case
    do { String -> SDoc -> TcS ()
traceTcS String
"mk_strict" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc))
       ; (EvVar -> TcS [Ct]) -> [EvVar] -> TcS [Ct]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM EvVar -> TcS [Ct]
do_one_given (Class -> [EvVar]
classSCSelIds Class
cls) }
  where
    loc :: CtLoc
loc  = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
    dict_ids :: [EvVar]
dict_ids  = [Type] -> [EvVar]
mkTemplateLocals [Type]
theta
    this_size :: PatersonSize
this_size = Class -> [Type] -> PatersonSize
pSizeClassPred Class
cls [Type]
tys

    do_one_given :: EvVar -> TcS [Ct]
do_one_given EvVar
sel_id
      | HasDebugCallStack => Type -> Bool
Type -> Bool
isUnliftedType Type
sc_pred
         -- NB: class superclasses are never representation-polymorphic,
         -- so isUnliftedType is OK here.
      , Bool -> Bool
not ([EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
      = -- See Note [Equality superclasses in quantified constraints]
        [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      | Bool
otherwise
      = do { given_ev <- CtLoc -> (Type, EvTerm) -> TcS GivenCtEvidence
newGivenEv CtLoc
sc_loc ((Type, EvTerm) -> TcS GivenCtEvidence)
-> (Type, EvTerm) -> TcS GivenCtEvidence
forall a b. (a -> b) -> a -> b
$
                         EvVar -> Type -> (Type, EvTerm)
mk_given_desc EvVar
sel_id Type
sc_pred
           ; assertFuelPrecondition fuel $
             mk_superclasses fuel rec_clss (CtGiven given_ev) tvs theta sc_pred }
      where
        sc_pred :: Type
sc_pred = EvVar -> [Type] -> Type
classMethodInstTy EvVar
sel_id [Type]
tys

      -- See Note [Nested quantified constraint superclasses]
    mk_given_desc :: Id -> PredType -> (PredType, EvTerm)
    mk_given_desc :: EvVar -> Type -> (Type, EvTerm)
mk_given_desc EvVar
sel_id Type
sc_pred
      = (Type
swizzled_pred, EvExpr -> EvTerm
EvExpr EvExpr
swizzled_evterm)
      where
        ([EvVar]
sc_tvs, Type
sc_rho)          = Type -> ([EvVar], Type)
splitForAllTyCoVars Type
sc_pred
        ([Scaled Type]
sc_theta, Type
sc_inner_pred) = Type -> ([Scaled Type], Type)
splitFunTys Type
sc_rho

        all_tvs :: [EvVar]
all_tvs       = [EvVar]
tvs [EvVar] -> [EvVar] -> [EvVar]
forall a. [a] -> [a] -> [a]
`chkAppend` [EvVar]
sc_tvs
        all_theta :: [Type]
all_theta     = [Type]
theta [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` ((Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
sc_theta)
        swizzled_pred :: Type
swizzled_pred = [EvVar] -> [Type] -> Type -> Type
HasDebugCallStack => [EvVar] -> [Type] -> Type -> Type
mkInfSigmaTy [EvVar]
all_tvs [Type]
all_theta Type
sc_inner_pred

        -- evar   :: forall tvs. theta => cls tys
        -- sel_id :: forall cls_tvs. cls cls_tvs
        --                        => forall sc_tvs. sc_theta => sc_inner_pred
        -- swizzled_evterm :: forall tvs sc_tvs. theta => sc_theta => sc_inner_pred
        swizzled_evterm :: EvExpr
swizzled_evterm
          | [EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
tvs, [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta -- See wrinkle (NQCS1)
          = EvVar -> EvExpr
forall b. EvVar -> Expr b
Var EvVar
sel_id EvExpr -> [Type] -> EvExpr
forall b. Expr b -> [Type] -> Expr b
`mkTyApps` [Type]
tys EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` EvVar -> EvExpr
evId EvVar
evar
          | Bool
otherwise
          = [EvVar] -> EvExpr -> EvExpr
forall b. [b] -> Expr b -> Expr b
mkLams [EvVar]
all_tvs (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$ [EvVar] -> EvExpr -> EvExpr
forall b. [b] -> Expr b -> Expr b
mkLams [EvVar]
dict_ids (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$
            EvVar -> EvExpr
forall b. EvVar -> Expr b
Var EvVar
sel_id EvExpr -> [Type] -> EvExpr
forall b. Expr b -> [Type] -> Expr b
`mkTyApps` [Type]
tys
                       EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` (EvVar -> EvExpr
evId EvVar
evar EvExpr -> [EvVar] -> EvExpr
forall b. Expr b -> [EvVar] -> Expr b
`mkVarApps` ([EvVar]
tvs [EvVar] -> [EvVar] -> [EvVar]
forall a. [a] -> [a] -> [a]
++ [EvVar]
dict_ids))
                       EvExpr -> [EvVar] -> EvExpr
forall b. Expr b -> [EvVar] -> Expr b
`mkVarApps` [EvVar]
sc_tvs

    sc_loc :: CtLoc
sc_loc | Class -> Bool
isCTupleClass Class
cls = CtLoc
loc
           | Bool
otherwise         = CtLoc
loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) }
           -- isCTupleClass: we don't want tuples to mess up the size calculations
           -- of Note [Solving superclass constraints]. For tuple predicates, this
           -- matters, because their size can be large, and we don't want to add a
           -- big class to the size of the dictionaries in the chain. When we get
           -- down to a base predicate, we'll include its size. See #10335.
           -- See Note [Solving tuple constraints]

    -- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
    -- for explanation of GivenSCOrigin and Note [Replacement vs keeping] in
    -- GHC.Tc.Solver.InertSet for why we need depths
    mk_sc_origin :: CtOrigin -> CtOrigin
    mk_sc_origin :: CtOrigin -> CtOrigin
mk_sc_origin (GivenSCOrigin SkolemInfoAnon
skol_info ScDepth
sc_depth Bool
already_blocked)
      = SkolemInfoAnon -> ScDepth -> Bool -> CtOrigin
GivenSCOrigin SkolemInfoAnon
skol_info (ScDepth
sc_depth ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ ScDepth
1)
                      (Bool
already_blocked Bool -> Bool -> Bool
|| SkolemInfoAnon -> Bool
newly_blocked SkolemInfoAnon
skol_info)

    mk_sc_origin (GivenOrigin SkolemInfoAnon
skol_info)
      = -- These cases do not already have a superclass constraint: depth starts at 1
        SkolemInfoAnon -> ScDepth -> Bool -> CtOrigin
GivenSCOrigin SkolemInfoAnon
skol_info ScDepth
1 (SkolemInfoAnon -> Bool
newly_blocked SkolemInfoAnon
skol_info)

    mk_sc_origin CtOrigin
other_orig = String -> SDoc -> CtOrigin
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"Given constraint without given origin" (SDoc -> CtOrigin) -> SDoc -> CtOrigin
forall a b. (a -> b) -> a -> b
$
                              EvVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvVar
evar SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtOrigin
other_orig

    newly_blocked :: SkolemInfoAnon -> Bool
newly_blocked (InstSkol ClsInstOrQC
_ PatersonSize
head_size) = Maybe PatersonCondFailure -> Bool
forall a. Maybe a -> Bool
isJust (PatersonSize
this_size PatersonSize -> PatersonSize -> Maybe PatersonCondFailure
`ltPatersonSize` PatersonSize
head_size)
    newly_blocked SkolemInfoAnon
_                      = Bool
False

-- Wanted case
mk_strict_superclasses ScDepth
fuel NameSet
rec_clss
  (CtWanted (WantedCt { ctev_pred :: WantedCtEvidence -> Type
ctev_pred = Type
pty, ctev_loc :: WantedCtEvidence -> CtLoc
ctev_loc = CtLoc
loc0, ctev_rewriters :: WantedCtEvidence -> CoHoleSet
ctev_rewriters = CoHoleSet
rws }))
  [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
  | (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType [Type]
tys
  = [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [] -- Wanteds with no variables yield no superclass constraints.
              -- See Note [Improvement from Ground Wanteds]

  | Bool
otherwise -- Wanted case, just add Wanted superclasses
              -- that can lead to improvement.
  = Bool -> SDoc -> TcS [Ct] -> TcS [Ct]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta) ([EvVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [EvVar]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
theta) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
    (Type -> TcS [Ct]) -> [Type] -> TcS [Ct]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM Type -> TcS [Ct]
do_one (Class -> [Type] -> [Type]
immSuperClasses Class
cls [Type]
tys)
  where
    loc :: CtLoc
loc = CtLoc
loc0 CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
`updateCtLocOrigin` Type -> CtOrigin -> CtOrigin
WantedSuperclassOrigin Type
pty

    do_one :: Type -> TcS [Ct]
do_one Type
sc_pred
      = do { String -> SDoc -> TcS ()
traceTcS String
"mk_strict_superclasses Wanted" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
sc_pred)
           ; sc_ev <- CtLoc -> CoHoleSet -> Type -> TcS WantedCtEvidence
newWantedNC CtLoc
loc CoHoleSet
rws Type
sc_pred
           ; mk_superclasses fuel rec_clss (CtWanted sc_ev) [] [] sc_pred }

{- Note [Improvement from Ground Wanteds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose class C b a => D a b
and consider
  [W] D Int Bool
Is there any point in emitting [W] C Bool Int?  No!  The only point of
emitting superclass constraints for W constraints is to get
improvement, extra unifications that result from functional
dependencies.  See Note [Why adding superclasses can help] above.

But no variables means no improvement; case closed.
-}

mk_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
                -> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
-- Return this constraint, plus its superclasses, if any
-- Precondition: fuel >= 0
mk_superclasses :: ScDepth
-> NameSet -> CtEvidence -> [EvVar] -> [Type] -> Type -> TcS [Ct]
mk_superclasses ScDepth
fuel NameSet
rec_clss CtEvidence
ev [EvVar]
tvs [Type]
theta Type
pred
  | ClassPred Class
cls [Type]
tys <- HasDebugCallStack => Type -> Pred
Type -> Pred
classifyPredType Type
pred
  = ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPrecondition ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
    ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_superclasses_of ScDepth
fuel NameSet
rec_clss CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys

  | Bool
otherwise   -- Superclass is not a class predicate
  = [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev]

mk_superclasses_of :: ExpansionFuel -> NameSet -> CtEvidence
                   -> [TyVar] -> ThetaType -> Class -> [Type]
                   -> TcS [Ct]
-- Always return this class constraint,
-- and expand its superclasses
-- Precondition: fuel >= 0
mk_superclasses_of :: ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_superclasses_of ScDepth
fuel NameSet
rec_clss CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
  | Bool
loop_found = do { String -> SDoc -> TcS ()
traceTcS String
"mk_superclasses_of: loop" (Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
                    ; ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPrecondition ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [ScDepth -> Ct
mk_this_ct ScDepth
fuel] }
                                                  -- cc_pend_sc of returning ct = fuel
  | Bool
otherwise  = do { String -> SDoc -> TcS ()
traceTcS String
"mk_superclasses_of" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
                                                          , Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> Bool
isCTupleClass Class
cls)
                                                          , NameSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr NameSet
rec_clss
                                                          ])
                    ; sc_cts <- ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPrecondition ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
                                ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_strict_superclasses ScDepth
fuel NameSet
rec_clss' CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
                    ; return (mk_this_ct doNotExpand : sc_cts) }
                                      -- doNotExpand: we have expanded this cls's superclasses, so
                                      -- exhaust the associated constraint's fuel,
                                      -- to avoid duplicate work
  where
    cls_nm :: Name
cls_nm     = Class -> Name
className Class
cls
    loop_found :: Bool
loop_found = Bool -> Bool
not (Class -> Bool
isCTupleClass Class
cls) Bool -> Bool -> Bool
&& Name
cls_nm Name -> NameSet -> Bool
`elemNameSet` NameSet
rec_clss
                 -- Tuples never contribute to recursion, and can be nested
    rec_clss' :: NameSet
rec_clss'  = NameSet
rec_clss NameSet -> Name -> NameSet
`extendNameSet` Name
cls_nm

    mk_this_ct :: ExpansionFuel -> Ct
    -- We can't use CNonCanonical here because we need to track the fuel
    mk_this_ct :: ScDepth -> Ct
mk_this_ct ScDepth
fuel | [EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
tvs, [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta
                    = DictCt -> Ct
CDictCan (DictCt { di_ev :: CtEvidence
di_ev = CtEvidence
ev, di_cls :: Class
di_cls = Class
cls
                                       , di_tys :: [Type]
di_tys = [Type]
tys, di_pend_sc :: ScDepth
di_pend_sc = ScDepth
fuel })
                    -- NB: If there is a loop, we cut off, so we have not
                    --     added the superclasses, hence cc_pend_sc = fuel
                    | Bool
otherwise
                    = QCInst -> Ct
CQuantCan (QCI { qci_tvs :: [EvVar]
qci_tvs = [EvVar]
tvs, qci_theta :: [Type]
qci_theta = [Type]
theta
                                     , qci_body :: Type
qci_body = Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys
                                     , qci_ev :: CtEvidence
qci_ev = CtEvidence
ev, qci_pend_sc :: ScDepth
qci_pend_sc = ScDepth
fuel })


{- Note [Equality superclasses in quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#15359, #15593, #15625)
  f :: (forall a. theta => a ~ b) => stuff

It's a bit odd to have a local, quantified constraint for `(a~b)`,
but some people want such a thing (see the tickets). And for
Coercible it is definitely useful
  f :: forall m. (forall p q. Coercible p q => Coercible (m p) (m q)))
                 => stuff

Moreover it's not hard to arrange; we just need to look up /equality/
constraints in the quantified-constraint environment, which we do in
GHC.Tc.Solver.Equality.tryQCsEqCt.

There is a wrinkle though, in the case where 'theta' is empty, so
we have
  f :: (forall a. a~b) => stuff

Now, potentially, the superclass machinery kicks in, in
makeSuperClasses, giving us a a second quantified constraint
       (forall a. a ~# b)
BUT this is an unboxed value!  And nothing has prepared us for
dictionary "functions" that are unboxed.  Actually it does just
about work, but the simplifier ends up with stuff like
   case (/\a. eq_sel d) of df -> ...(df @Int)...
and fails to simplify that any further.

So for now we simply decline to take superclasses in the quantified
case.  Instead we have a special case in GHC.Tc.Solver.Equality.tryQCsEqCt
which looks for primitive equalities specially in the quantified
constraints.

See also Note [Evidence for quantified constraints] in GHC.Core.Predicate.
-}