Note [Inferred contexts from method constraints]
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
- Simplifying the instance context GHC.Tc.Deriv.Infer
Referenced by 1
- GHC.Tc.Deriv.Infer call site