-    go_arg _               _             = False

-

-Suppose we have f :: forall p q. (Ord p, Eq q) => p -> q -> q, and a pragma

-

-  {-# SPECIALISE forall x. f @[a] @[Int] x [3,4] #-}

-

-In `dsSpec` the `SpecPragE` will look something like this:

-

-  SpecPragE { spe_fn_id = f

-            , spe_bndrs = @a (d:Ord a) (x:[a])

-            , spe_call  = let d2:Ord [a] = $dfOrdList d

-                              d3:Eq [Int] = $dfEqList $dfEqInt

-                          in f @[a] @[Int] d2 d3 x [3,4] }

-We want to get

-

-    RULE  forall a (d2:Ord a) (d3:Eq [Int]) (x:[a]).

-             f @[a] @[Int] d2 d3 x [3,4] = $sf d2 x

-

-    $sf :: forall a. Ord [a] => a -> Int

-    $sf = /\a. \d2 x.

-             let d3 = $dfEqList $dfEqInt

-             in <f-rhs> @[a] @[Int] d2 d3 x [3,4]

-

-Notice that

-

-(SP1) If the expression in the SPECIALISE pragma had a type signature, such as

-     SPECIALISE f :: Eq b => Int -> b -> b

-  then the desugared expression may have type abstractions and applications

-  "in the way", like this:

-     (/\b. (\d:Eq b). let d1 = $dfOrdInt in f @Int @b d1 d) @b (d2:Eq b)

-  The lambdas come from the type signature, which is then re-instantiated,

-  hence the applications of those lambdas.

-

-  We use the simple optimiser to simplify this to

-     let { d = d2; d1 = $dfOrdInt } in f @Int @b d1 d

-

-  Important: do no inlining in this "simple optimiser" phase:

-  use `simpleOptExprNoInline`. E.g. we don't want to turn it into

-     f @Int @b $dfOrdInt d2

-  because the latter is harder to match.

-

-  Similarly if we have

-     let { d1=d; d2=d } in f d1 d2

-  we don't want to inline d1/d2 to get this

-     f d d

-

-(SP2) $sf does not simply quantify over (d:Ord a). Instead, to figure out what

-  it should quantify over, and to include the 'd3' binding in the body of $sf,

-  we use the function `prepareSpecLHS`. It takes the simplified LHS `core_call`,

-  and uses the dictionary bindings to figure out the RULE LHS and RHS.

-

-  This is described in Note [prepareSpecLHS].

-

-Note [prepareSpecLHS]

-~~~~~~~~~~~~~~~~~~~~~

-To compute the appropriate RULE LHS and RHS for a new-form specialise pragma,

-as described in Note [Desugaring new-form SPECIALISE pragmas], we use a function

-called prepareSpecLHS.

-It takes as input a list of (type and evidence) binders, and a Core expression.

-For example, suppose its input is of the following form:

-

-  spe_bndrs = @a (d:Ord a)

-  spe_call =

-    let

-      -- call these bindings the call_binds

-      d1 :: Num Int

-      d1 = $dfNumInt

-      d2 :: Ord [a]

-      d2 = $dfOrdList d

-      d3 :: Eq a

-      d3 = $p1Ord d3

-      d4 :: Ord (F a)

-      d4 = d |> co1

-      d5 :: Ord (G a)

-      d5 = d4 |> co2

-    in

-      f @[a] @Int d1 d2 d3 d5

-

-The goal of prepareSpecLHS is then to generate the following two things:

-

-  - A specialisation, of the form:

-

-      $sf <spec_args> =

-        let <spec_binds>

-        in <f-rhs> @[a] @Int d1 d2 d3 d5

-

-  - A rule, of the form:

-

-      RULE forall a d1 d2 d3 d5. f @[a] @Int d1 d2 d3 d5 =

-        let <rule_binds>

-        in $sf <spec_args>

-

-That is, we must compute 'spec_args', 'rule_binds' and 'spec_binds'. A first

-approach might be:

-

-  - take spec_args = spe_bndrs,

-  - spec_binds = call_binds.

-

-If we did so, the RULE would look like:

-

-  RULE forall a d1 d2 d3 d5. f @[a] @Int d1 d2 d3 d5 =

-    let d = <???>

-    in $sf @a d

-

-The problem is: how do we recover 'd' from 'd1', 'd2', 'd3', 'd5'? Essentially,

-we need to run call_binds in reverse. In this example, we had:

-

-  d1 :: Num Int

-  d1 = $dfNumInt

-  d2 :: Ord [a]

-  d2 = $dfOrdList d

-  d3 :: Eq a

-  d3 = $p1Ord d3

-  d4 :: Ord (F a)

-  d4 = d |> co1

-  d5 :: Ord (G a)

-  d5 = d4 |> co2

-

-Let's try to recover (d: Ord a) from 'd1', 'd2', 'd4', 'd5':

-

-  - d1 is a constant binding, so it doesn't help us.

-  - d2 uses a top-level instance, which we can't run in reverse; we can't

-    obtain Ord a from Ord [a].

-  - d3 uses a superclass selector which prevents us from making progress.

-  - d5 is defined using d4, and both involve a cast.

-    In theory we could define d = d5 |> sym (co1 ; co2), but this gets

-    pretty complicated.

-

-This demonstrates the following:

-

-  1. The bindings can't necessarily be "run in reverse".

-  2. Even if the bindings theoretically can be "run in reverse", it is not

-     straightforward to do so.

-

-Now, we could strive to make the let-bindings reversible. We already do this

-to some extent for quantified constraints, as explained in

-Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig,

-using the TcSSpecPrag solver mode described in Note [TcSSpecPrag] in GHC.Tc.Solver.Monad.

-However, given (2), we don't bother ensuring that e.g. we don't use top-level

-class instances like in d2 above. Instead, we handle these bindings in

-prepareSpecLHS as follows:

-

-  (a) Go through the bindings in order.

-

-    (1) Bindings like

-          d1 = $dfNumInt

-        depend only on constants and move to the specialised function body.

-        That is crucial -- it makes those specialised methods available in the

-        specialised body. These are the `spec_const_binds`.

-

-        Note that these binds /can/ depend on locally-quantified /type/ variables.

-        For example, if we have

-          instance Monad (ST s) where ...

-        then the dictionary for (Monad (ST s)) is effectively a constant dictionary.

-        This is important to get specialisation for such types. Example in test T8331.

-

-    (2) Other bindings, like

-          d2:Ord [a] = $dfOrdList d

-          d3 = d

-        depend on a locally-quantifed evidence variable `d`.

-        Surprisingly, /we want to drop these bindings entirely!/

-        This is because, as explained above, it is too difficult to run these

-        in reverse. Instead, we drop them, and re-compute which dictionaries

-        we will quantify over.

-

-    (3) Finally, inside those dictionary bindings we should find the call of the

-        function itself

-            f @[a] @[Int] d2 d3 x [3,4]

-        'prepareSpecLHS' takes the call apart and returns its arguments.

-

-  (b) Now, (a)(2) means that the RULE does not quantify over 'd' any more; it

-      quantifies over 'd1' 'd2' 'd3' 'd5'. So we recompute the `rule_bndrs`

-      from scratch.

-

-      Moreover, the specialised function also no longer quantifies over 'd',

-      it quantifies over 'd2' 'd3' 'd5'. This set of binders is computed by

-      taking the RULE binders and subtracting off the binders from

-      the `spec_const_binds`.

-

-[Shortcoming] This whole approach does have one downside, compared to running

-the let-bindings in reverse: it doesn't allow us to common-up dictionaries.

-Consider for example:

-

-  g :: forall a b. ( Eq a, Ord b ) => a -> b -> Bool

-  {-# SPECIALISE g :: forall c. Ord c => c -> c -> Bool #-}

-

-The input to prepareSpecLHS will be (more or less):

-

-  spe_bndrs: @c (d:Ord c)

-  spe_call =

-    let

-      d1 :: Eq c

-      d1 = $p1Ord d

-      d2 :: Ord c

-      d2 = d

-    in

-      g @c @c d1 d2

-

-The approach described in (2) will thus lead us to generate:

-

-  RULE g @c @c d1 d2 = $sg @c d1 d2

-  $sg @c d1 d2 = <g-rhs> @c @c d1 d2

-

-when we would rather avoid passing both dictionaries, and instead generate:

-

-  RULE g @c @c d1 d2 = let { d = d2 } in $sg @c d

-  $sg @c d = let { d1 = $p1Ord d; d2 = d } in <g-rhs> @c @c d1 d2

-

-For now, we accept this infelicity.

-

-Note [Desugaring new-form SPECIALISE pragmas] -- Take 2

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-But that would do no specialisation! What we want is this:

-                    dx1 = d7  -- Renaming

-                    d6 = dx1

-     - `rev_binds`: the enclosing let-bindings (actually reversed)

-    We carefully arrange that the dictionary arguments of the actual

-    call, `rule_lhs_args` are all distinct dictionary variables,

-    not expressions. How? We use `simpleOptExprNoInline` to avoid

-    inlining the let-bindings.

-

-(S3) grabSpecBinds: transform `rev_binds` into `spec_binds`: the

-   bindings we will wrap around the call in the RHS of `$sf`

-

-(S4) Find `spec_bndrs`, the subset of `rule_bndrs` that we actually

-   need to pass to `$sf`, simply by filtering out those that are

-   bound by `spec_binds`.  In the example

-      spec_bndrs = d1,d4

-

-

-     Working inner

-* Grab any bindings we can that will "shadow" the forall'd

-  rule-bndrs, giving specialised bindings for them.

-  * We keep a set of known_bndrs starting with {d1,..,dn}

-  * We keep a binding iff no free var is

-      (a) in orig_bndrs (i.e. not totally free)

-      (b) not in known_bndrs

-  * If we keep it, add its binder to known_bndrs; if not, don't

-

-To maximise what we can "grab", start by extracting /renamings/ of the

-forall'd rule_bndrs, and bringing them to the top.  A renaming is

-    rule_bndr = d

-If we see this:

-  * Bring d=rule_bndr to the top

-  * Add d to the set of variables to look for on the right.

-    e.g.    rule_bndrs = d1, d2

-            Bindings   { d7=d9; d1=d7 }

-        Bring to the top  { d7=d1; d9=d7 }

-

-  = do { mb_call_info <- decomposeCall poly_id ds_call

-  = do { -- Simplify the (desugared) call; see wrinkle (SP1)

-         -- in Note [Desugaring new-form SPECIALISE pragmas]

-       ; dflags  <- getDynFlags

-    (2) Solve these constraints, but in special TcSSpecPrag mode which ensures

-        each original Wanted is either fully solved or left untouched.

-        See Note [Fully solving constraints for specialisation].

-Note [Fully solving constraints for specialisation]

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-As far as specialisation is concerned, it is actively harmful to simplify

-constraints without /fully/ solving them.

-

-Example:

-

-  f :: ∀ a t. (Eq a, ∀x. Eq x => Eq (t x)). t a -> Char

-  {-# SPECIALISE f @Int #-}

-

-  Typechecking 'f' will result in [W] Eq Int, [W] ∀x. Eq x => Eq (t x).

-  We absolutely MUST leave the quantified constraint alone, because we want to

-  quantify over it. If we were to try to simplify it, we would emit an

-  implication and would thereafter never be able to quantify over the original

-  quantified constraint.

-

-  However, 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 @[] #-}.

-

-The conclusion is this:

-

-  when solving the constraints that arise from a specialise pragma, following

-  the recipe described in Note [Handling new-form SPECIALISE pragmas], all

-  Wanted quantified constraints should either be:

-    - fully solved (no free evidence variables), or

-    - left untouched.

-

-To achieve this, we run the solver in a special "all-or-nothing" solving mode,

-described in Note [TcSSpecPrag] in GHC.Tc.Solver.Monad.

-

-Note that a similar problem arises in other situations in which the solver takes

-an irreversible step, such as using a top-level class instance. This is currently

-less important, as the desugarer can handle these cases. To explain, consider:

-

-    g :: ∀ a. Eq a => a -> Bool

-    {-# SPECIALISE g @[e] #-}

-

-  Typechecking 'g' will result in [W] Eq [e]. Were we to simplify this to

-  [W] Eq e, we would have difficulty generating a RULE for the specialisation:

-

-    $sg :: Eq e => [e] -> Bool

-

-    RULE ∀ e (d :: Eq [e]). g @[e] d = $sg @e (??? :: Eq e)

-      -- Can't fill in ??? because we can't run instances in reverse.

-

-    RULE ∀ e (d :: Eq e). g @[e] ($fEqList @e d) = $sg @e d

-      -- Bad RULE matching template: matches on the structure of a dictionary

-

-  Moreover, there is no real benefit to any of this, because the specialiser

-  can't do anything useful from the knowledge that a dictionary for 'Eq [e]' is

-  constructed from a dictionary for 'Eq e' using the 'Eq' instance for lists.

-

-Here, it would make sense to also use the "solve completely" mechanism in the

-typechecker to avoid producing evidence terms that we can't "run in reverse".

-However, the current implementation tackles this issue in the desugarer, as is

-explained in Note [prepareSpecLHS] in GHC.HsToCore.Binds.

-So, for the time being at least, in TcSSpecPrag mode, we don't attempt to "fully solve"

-constraints when we use a top-level instance. This might change in the future,

-were we to decide to attempt to address [Shortcoming] in Note [prepareSpecLHS]

-in GHC.HsToCore.Binds.

-

-         -- (2) Solve the resulting wanteds in TcSSpecPrag mode.

-** exactly the same programs should typecheck with or without this

-** procedure.

-

-Solving fully

-~~~~~~~~~~~~~

-There is a reason why the solver does not simply try to solve such

-constraints with top-level instances. If the solver finds a relevant

-instance declaration in scope, that instance may require a context

-that can't be solved for. A good example of this is:

-

-    f :: Ord [a] => ...

-    f x = ..Need Eq [a]...

-

-If we have instance `Eq a => Eq [a]` in scope and we tried to use it, we would

-be left with the obligation to solve the constraint Eq a, which we cannot. So we

-must be conservative in our attempt to use an instance declaration to solve the

-[W] constraint we're interested in.

-

-Our rule is that we try to solve all of the instance's subgoals

-recursively all at once. Precisely: We only attempt to solve

-constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci

-are themselves class constraints of the form `C1', ... Cm' => C' t1'

-... tn'` and we only succeed if the entire tree of constraints is

-solvable from instances.

-Which, because solving `Eq [a]` demands `Eq a` which we cannot solve, produces:

-Note [Shortcut solving: type families]

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-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).  Really we should now rewrite to reduce the (3-1) to 2, and

-so on -- but that is reproducing yet more of the solver.  Sigh.  For now,

-we just give up (remember all this is just an optimisation).

-

-But we must not just naively try to lookup (Take (3-1)) in the

-InstEnv, or it'll (wrongly) appear not to match (Take 0) and get a

-unique match on the (Take n) instance.  That leads immediately to an

-infinite loop.  Hence the check that 'preds' have no type families

-(isTyFamFree).

-Note [Shortcut try_solve_from_instance]

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-The workhorse of the short-cut solver is

-    try_solve_from_instance :: (EvBindMap, DictMap CtEvidence)

-                            -> CtEvidence       -- Solve this

-                            -> MaybeT TcS (EvBindMap, DictMap CtEvidence)

-Note that:

-

-* The CtEvidence is the goal to be solved

-

-* The MaybeT manages early failure if we find a subgoal that

-  cannot be solved from instances.

-

-* The (EvBindMap, DictMap CtEvidence) is an accumulating purely-functional

-  state that allows try_solve_from_instance to augment the evidence

-  bindings and inert_solved_dicts as it goes.

-

-  If it succeeds, we commit all these bindings and solved dicts to the

-  main TcS InertSet.  If not, we abandon it all entirely.

-

-Passing along the solved_dicts important for two reasons:

-

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

-      Like TcSVanilla, but the idea is that the returned InertSet will

-      later be resumed, so we do not want to restore type-equality cycles

-      See also Note [Type equality cycles] in GHC.Tc.Solver.Equality

-* TcSSpecPrag: Solve constraints fully or not at all. This is described in

-  Note [TcSSpecPrag].

-

-  This mode is currently used in one place only: when solving constraints

-  arising from specialise pragmas.

-  See Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig.

--- | Run the 'TcS' monad in 'TcSSpecPrag' mode, which either fully solves

--- individual Wanted quantified constraints or leaves them alone.

---

-

-{- Note [TcSSpecPrag]

-~~~~~~~~~~~~~~~~~~~~~

-The TcSSpecPrag mode is a specialized constraint solving mode that guarantees

-that Wanted quantified constraints are either:

-  - Fully solved with no free evidence variables, or

-  - Left completely untouched (no simplification at all)

-

-Examples:

-

-  * [W] forall x. Eq x => Eq (f x).

-

-    In TcSSpecPrag mode, we **do not** process this quantified constraint by

-    creating a new implication constraint; we leave it alone instead.

-

-  * [W] Eq (Maybe Int).

-

-    This constraint is solved fully, using two top-level Eq instances.

-

-  * [W] forall x. Eq x => Eq [x].

-

-    This constraint is solved fully as well, using the Eq instance for lists.

-

-This functionality is crucially used by the specialiser, for which taking an

-irreversible constraint solving steps is actively harmful, as described in

-Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig.

-

-Note that currently we **do not** refrain from using top-level instances,

-even though we also can't run them in reverse; this isn't a problem for the

-specialiser (which is currently the sole consumer of this functionality).

-

-The implementation is as follows: in TcSSpecPrag mode, when we are about to

-solve a Wanted quantified constraint by emitting an implication, we call the

-special function `solveCompletelyIfRequired`. This function recursively calls

-the solver but in TcSVanilla mode (i.e. full-blown solving, with no restrictions).

-If this recursive call manages to solve all the remaining constraints fully,

-then we proceed with that outcome (i.e. we continue with that inert set, etc).

-Otherwise, we discard everything that happened in the recursive call, and

-continue with the original quantified constraint unchanged.

-

-In the future, we could consider re-using this functionality for the short-cut

-solver (see Note [Shortcut solving] in GHC.Tc.Solver.Dict), but we would have to

-be wary of the performance implications.

--}

-

-nestImplicTcS ref inner_tclvl (TcS thing_inside)

-                 -- All other InertSet fields are inherited

-       ; let nest_env = env { tcs_ev_binds = ref

-       ; ev_binds <- TcM.getTcEvBindsMap ref

-         then do { addInertForAll qci

-         else do { setWantedEvTerm dest EvCanonical $

-is delightfully easy.   Just build an implication constraint

-We can take a more straightforward parth when there is a matching Given, e.g.

-  [W] dg :: forall c d. (Eq c, Ord d) => C x c d

-In this case, it's better to directly solve the Wanted from the Given, instead

-of building an implication. This is more than a simple optimisation; see

-Note [Solving Wanted QCs from Given QCs].

-The tricky point is about termination: see #19690.  We want to maintain

-the invariant (QC-INV):

-  (QC-INV) Every quantified constraint returns a non-bottom dictionary

-just as every top-level instance declaration guarantees to return a non-bottom

-dictionary.  But as #19690 shows, it is possible to get a bottom dicionary

-by superclass selection if we aren't careful.  The situation is very similar

-to that described in Note [Recursive superclasses] in GHC.Tc.TyCl.Instance;

-and we use the same solution:

-* Give the Givens a CtOrigin of (GivenOrigin (InstSkol IsQC head_size))

-* Give the Wanted a CtOrigin of (ScOrigin IsQC NakedSc)

-Both of these things are done in solveForAll.  Now the mechanism described

-in Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance takes over.