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).