Note [Inferred contexts from method constraints]

GHC/Tc/Deriv/Infer.hs:573 compiler

Consider the `deriving Alt` part of this example (from the passing part of
T20815a):

  class Alt f where
    some :: forall a. Applicative f => f a -> f [a]

  newtype T f a = T (f a) deriving Alt

We will produce this derived instance declaration:

  instance (Alt f, ???) => Alt (T f) where
    some :: forall a. Applicative (T f) => T f a -> T f [a]
    some @a (d1 :: Applicative (T f))
      = coerce @(f a -> f [a])
               @(T f a -> T f [a])
               (d2 :: Coercible (f a -> f [a]) (T f a -> T f [a]))
               (some @f (d3 :: Alt f) @a (d4 :: Applicative f))

(Dictionary abstractions and applications are added here even though they are
not usually visible, or even emitted in the code generated by `deriving`.)

The task of `inferConstraints` is to determine the `???` such that it will be
sufficient to solve the constraints arising from that definition of `some`. We
can write out what the type checker sees as follows:

  forall f
    [G] Alt f                -- Given
    [G] ???                  -- Given
  =>
    forall a.
      [G] Applicative (T f)  -- Also given (as d1)
    =>
      [W] Coercible (f a -> f [a]) (T f a -> T f [a])  -- Wanted (as d2)
      [W] Alt f                                        -- Wanted (as d3)
      [W] Applicative f                                -- Wanted (as d4)

`d3` is trivially provided by the given `Alt f`. The simplest way to ensure that
`d4` and `d2` can be solved is to:

* Generate this "target constraint" (in `inferConstraintsCoerceBased`):

  forall a. Applicative (T f)
    => ( Coercible (f a -> f [a]) (T f a -> T f [a])
       , Applicative f
       )

* Simplify the target constraint (in `simplifyInstanceContexts`, which in turn
  calls `simplifyDeriv`). This solves the `Coercible` constraint outright, but
  cannot solve the `Applicative f` constraint.
  See Note [Simplifying the instance context]

* The leftover, unsolved constraint (here `Applicative f`) becomes the `???` in
  the derived instance decl.

The target constraint for GND is created in `inferConstraintsCoerceBased`.

In general, the point here is that the inferred context for a derived instance
must include, for each class method with constraints, a quantified constraint
mapping the provided context for the derived method to both:
  - the `Coercible` corresponding to the monotypes of the base and derived
    methods, and
  - the needed context for the base method.


************************************************************************
*                                                                      *
         Finding the fixed point of deriving equations
*                                                                      *
************************************************************************

References 1

Referenced by 1