+* The `spec_bndrs`, which are lambda-bound in the specialised function `$sf`,

+    (2) Solve these constraints.  When doing so, switch on `tcsmFullySolveQCIs`;

+        see wrinkle (NFS1) below.

+(NFS1) Consider

+    f :: forall f a. (Ix a, forall x. Eq x => Eq (f x)) => a -> f a

+    {-# SPECIALISE f :: forall f. (forall x. Eq x => Eq (f x)) => Int -> f Int #-}

+  This SPECIALISE is treated like an expression with a type signature, so

+  we instantiate the constraints, simplify them and re-generalise.  From the

+  instantiation we get  [W] d :: (forall x. Eq a => Eq (f x))

+  and we want to generalise over that.  We do not want to attempt to solve it

+  and then get stuck, and emit an error message.  If we can't solve it, it is

+  much, much better to leave it alone.

+

+  We still need to simplify quantified constraints that can be /fully solved/

+  from instances, otherwise we would never be able to specialise them

+  away. Example: {-# SPECIALISE f @[] @a #-}.  So:

+

+  * The constraint solver has a mode flag `tcsmFullySolveQCIs` that says

+    "fully solve quantified constraint, or leave them alone

+  * When simplifying constraints in a SPECIALISE pragma, we switch on this

+    flag the `SpecPragE` case of `tcSpecPrag`.

+

+  You might worry about the wasted work from failed attempts to fully-solve, but

+  it is seldom repeated (because the constraint solver seldom iterates much).

+

+                               -- tcsmFullySolveQCIs: see (NFS1)a

+       ; (residual_wc, _) <- runTcS $

+                             do { _ <- solveSimpleGivens given_cts

+                                ; solveSimpleWanteds (listToBag (map mkNonCanonical wanteds)) }

+                 bagToList (wc_simple residual_wc)) }

+               ; return $ if isEmptyWC residual then Just (tvs, subst) else Nothing }

+                  ; return (isEmptyWC residual) }

+import GHC.Types.SrcLoc

+import GHC.Rename.Env

+import Data.Maybe( catMaybes )

+    = text "TcSMode" <> (braces $ cat $ punctuate comma $ catMaybes $

+                         [ pp_one pm "PmCheck", pp_one ea "EarlyAbort"

+                         , pp_one so "SkipOverlappable", pp_one fs "FullySolveQCIs" ])

+      -- We get something like TcSMode{EarlyAbort,FullySolveQCIs},

+      -- mentioning just the flags that are on

+    where

+      pp_one True s  = Just (text s)

+      pp_one False _ = Nothing

+       ; (unifs1, wc1) <- reportUnifications $  -- See Note [Superclass iteration]

+                          solveSimpleWanteds simples

+       ; let wc' = wc1 { wc_impl = wc_impl wc1 `unionBags` implics' }

+solveSimpleWanteds :: Cts -> TcS WantedConstraints

+-- Returns unsolved constraints, mostly just flat ones (Cts),

+-- but also any unsolved implications arising from forall-constraints

+       ; (n,simples',implics') <- go (solverIterations dflags) 1 emptyBag simples

+

+       ; let unsolved_wc = emptyWC { wc_simple = simples', wc_impl = implics' }

+                  , text "residual =" <+> ppr unsolved_wc ]

+

+       ; return unsolved_wc }

+    go :: IntWithInf       -- Limit

+       -> Int              -- Iteration number

+       -> Bag Implication  -- Accumulating parameter: unsolved implications

+       -> Cts              -- Try to solve these

+       -> TcS (Int, Cts, Bag Implication)

+    go limit n implics wanted

+                         simples limit

+                         (emptyWC { wc_simple = wanted, wc_impl = implics })

+

+      | isEmptyBag wanted

+      = return (n, wanted, implics)

+

+             (wanted1, implics1) <- solve_one wanted

+           ; let implics2 = implics `unionBags` implics1

+             -- NB: runTcPluginsWanted has a fast path for

+             --     empty wanted1, which is the common case

+           ; (rerun_plugin, wanted2) <- runTcPluginsWanted wanted1

+                     ; go limit (n+1) implics2 wanted2 }   -- Loop

+             else return (n, wanted2, implics2) }          -- Done

+    solve_one :: Cts -> TcS (Cts, Bag Implication)

+    -- Try solving these constraints

+    -- Affects the unification state (of course) but not the inert set

+    -- The result is not necessarily zonked

+    solve_one simples

+      = nestTcS $

+        do { solveSimples simples

+           ; simples' <- getUnsolvedInerts

+               -- Now try to solve any Wanted quantified

+               -- constraints (i.e. QCInsts) in `simples1`

+           ; solveWantedQCIs simples' }

+

+  to solve it (using tryInertQCs).  In particular, solve a Wanted QCI

+  from an identical Given.  This is more than a simple optimisation:

+  see Note [Solving Wanted QCs from Given QCs]

+  If not, just stash it in `inert_qcis :: [QCInst]`. (If it's a Given

+  we can use it to solve other constraints; if a Wanted we will solve

+  it later using `solveWantedQCIs`.)

+* In the main `solveSimpleWanteds` (specifically `solve_one`):

+  - We attempt to solve the `wc_simple` constraints with `solveSimples`

+    Unsolved quantified constraints just accumulate in the `inert_qcis` field

+    of the `InertSet`.

+  - Then we use `solveWantedQCIs` to solve any quantified constraints. That

+    often turns the `QCInst` into an `Implication`; but not invariably (WFA4)

+Wrinkles:

+(WFA4) When `tcsmFullySolveQCIs` is on, we adopt an all-or-nothing strategy:

+   either solve the forall-constraint /fully/ or do nothing at all.

+   Why?  See (NFS1) in Note [Handling new-form SPECIALISE pragmas] in GHC.Tc.Gen.Sig

+           -> -- Commit to the (partly or fully solved) implication

+import GHC.Tc.Types.Constraint( Cts, Implication, WantedConstraints )

+solveSimpleWanteds :: Cts -> TcS WantedConstraints

+evTermFVs (EvFun { et_tvs = tvs, et_given = given

+                 , et_binds = tc_ev_binds, et_body = v })

+  = case tc_ev_binds of

+      TcEvBinds {}  -> emptyFV  -- See Note [Free vars of EvFun]

+      EvBinds binds -> addBndrsFV bndrs fvs

+        where

+          fvs = foldr (unionFV . evTermFVs . eb_rhs) (unitFV v) binds

+          bndrs = foldr ((:) . eb_lhs) (tvs ++ given) binds

+* /During/ typechecking, `evTermFVs` is used only by `GHC.Tc.Solver.neededEvVars`

+  * Each EvBindsVar in an et_binds field of an EvFun is /also/ in the

+    ic_binds field of an Implication

+  * So we can track usage via the processing for that implication,

+    (see Note [Tracking redundant constraints] in GHC.Tc.Solver).

+    We can ignore usage from the EvFun altogether.

+

+* /After/ typechecking `evTermFVs` is used by `GHC.Iface.Ext.Ast`, but by

+  then it has been zonked so we can get at the bindings.