Defaulting plugins are not run at the right time

It seems to me that defaulting plugins are not run at the right point in time, because they are handed a whole implication tree. This means that defaulting plugins only get to see things "after the fact", e.g. after we have already decided on quantification for top-level bindings.

Problem 1: quantification

Let me give an example with a partial type signature for clarity (similar examples can be written without any type signature at all):

{-# LANGUAGE PartialTypeSignatures, NamedWildCards #-}
fun1 :: _a -> Bool
fun1 x = x == x

Here GHC will decide to quantify _a into a skolem, and then the defaulting plugin will see an implication with a[sk]:

  WC {wc_impl =
        Implic {
          TcLevel = 1
          Skolems = a_a599[sk:1]
          Given-eqs = NoGivenEqs
          Status = Unsolved
          Given =
          Wanted =
            WC {wc_simple = [W] $dEq_a59a {0}:: Eq a_a599[sk:1] (CDictCan)
                wc_errors = {_a_a4Xk:a_a599[sk:1]}}
          Binds = EvBindsVar<a59e>
          the inferred type of fun1 :: a_a599[sk:1] -> Bool }}

What if the plugin wanted to default _a in order to solve Eq _a? It has no means of doing so; in fact defaulting plugins will never see any metavariables arising from such a program.

Problem 2: nested implications

There is no way for a plugin to do defaulting inside an implication with Given constraints, as the solveSimpleWanteds run happens outside of the implication when the Givens are no longer available.

A slightly contrived example:

type C :: Type -> Type -> Constraint
class C a b where
  meth :: a -> b -> ()

type D :: Type -> Type
class D b where { }

instance D b => C Int b where { meth _ _ = () }

data Dict ct where
  Dict :: ct => Dict ct

mk_dict :: b -> (b, Dict (D b))
mk_dict = undefined

baz = case mk_dict undefined of
        (b, Dict) -> foo undefined b

Here we will end up with an implication of the form

[G] D beta => [W] C alpha beta

However, if we suggest defaulting alpha := Int, we end up in a solver run WITHOUT the Given [G] D beta, because it comes from an inner implication. Then, when using the instance C Int b, we end up with [W] D beta which we can't solve, because we don't have the Given around anymore. This then causes us to abort the defaulting attempt (due to unsolved residual Wanted constraints).