Note [Solved dictionaries]

GHC/Tc/Solver/InertSet.hs:388 compiler 1 ticket

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

Referenced by 6