Note [Solved dictionaries]
When we apply a top-level instance declaration, we add the "solved"
dictionary to the inert_solved_dicts. In general, we use it to avoid
creating a new EvVar when we have a new goal that we have solved in
the past.
But in particular, we can use it to create *recursive* dictionaries.
The simplest, degenerate case is
instance C [a] => C [a] where ...
If we have
[W] d1 :: C [x]
then we can apply the instance to get
d1 = $dfCList d
[W] d2 :: C [x]
Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
d1 = $dfCList d
d2 = d1
See Note [Example of recursive dictionaries]
VERY IMPORTANT INVARIANT:
(Solved Dictionary Invariant)
Every member of the inert_solved_dicts is the result
of applying an instance declaration that "takes a step"
An instance "takes a step" if it has the form
dfunDList d1 d2 = MkD (...) (...) (...)
That is, the dfun is lazy in its arguments, and guarantees to
immediately return a dictionary constructor. NB: all dictionary
data constructors are lazy in their arguments.
This property is crucial to ensure that all dictionaries are
non-bottom, which in turn ensures that the whole "recursive
dictionary" idea works at all, even if we get something like
rec { d = dfunDList d dx }
See Note [Recursive superclasses] in GHC.Tc.TyCl.Instance.
Reason:
- All instances, except two exceptions listed below, "take a step"
in the above sense
- Exception 1: local quantified constraints have no such guarantee;
indeed, adding a "solved dictionary" when applying a quantified
constraint led to the ability to define unsafeCoerce
in #17267.
- Exception 2: the magic built-in instance for (~) has no
such guarantee. It behaves as if we had
class (a ~# b) => (a ~ b) where {}
instance (a ~# b) => (a ~ b) where {}
The "dfun" for the instance is strict in the coercion.
Anyway there's no point in recording a "solved dict" for
(t1 ~ t2); it's not going to allow a recursive dictionary
to be constructed. Ditto (~~) and Coercible.
THEREFORE we only add a "solved dictionary"
- when applying an instance declaration
- subject to Exceptions 1 and 2 above
In implementation terms
- GHC.Tc.Solver.Monad.addSolvedDict adds a new solved dictionary,
conditional on the kind of instance
- It is only called when applying an instance decl,
in GHC.Tc.Solver.Dict.tryInstances
- ClsInst.InstanceWhat says what kind of instance was
used to solve the constraint. In particular
* LocalInstance identifies quantified constraints
* BuiltinEqInstance identifies the strange built-in
instances for equality.
- ClsInst.instanceReturnsDictCon says which kind of
instance guarantees to return a dictionary constructor
Other notes about solved dictionaries
* See also Note [Do not add superclasses of solved dictionaries]
* The inert_solved_dicts field is not rewritten by equalities,
so it may get out of date.
* The inert_solved_dicts are all Wanteds, never givens
* We only cache dictionaries from top-level instances, not from
local quantified constraints. Reason: if we cached the latter
we'd need to purge the cache when bringing new quantified
constraints into scope, because quantified constraints "shadow"
top-level instances. References 3
- Do not add superclasses of solved dictionaries GHC.Tc.Solver.InertSet
- Example of recursive dictionaries GHC.Tc.Solver.InertSet
- Recursive superclasses GHC.Tc.TyCl.Instance
Referenced by 6
- GHC.Tc.Types.Origin call site ×2
- GHC.Tc.Instance.Class call site
- Shadowing of implicit parameters GHC.Tc.Solver.Dict
- GHC.Tc.Solver.InertSet call site
- GHC.Tc.Solver.Monad call site