Simon Peyton Jones
Ben, Richard
rewritableTyVarsOfType is used when deciding whether to split a [WD] constraint into [W] and [D]. For example, if we are adding [WD] C a and there is an inert [WD] a ~ Int then we want to split the [WD] into [W] C a [D] C a so that the [D] one can be rewritten and perhaps yield improvement etc.
There is no point in rewriting coercions or cases in t, because they won't help (C t) to reduce. That's why rewriteableTyVarsOfType differs from tyVarsOfType. And indeed the arg of a class C should be a monotype.
Ahh, I see.
So rewriteableTyVarsOfType doesn't expect foralls, hence the panic. But it's seeing a forall in an /equality/ constraint.
FIRST ISSUE: I'm a bit surprised about that (smacks of impredicative polymorphism) so the first thing to check is that this is really supposed to happen in this program. Richard should be able to help.
Indeed this test is meant to fail, just not with a panic. I suspect this means that my solver logic isn't catching requests for polytypes as early as it needs to.
SECOND ISSUE: But regardless, I now realise that shouldSplitWD only needs to split a [WD] equality if the LHS matches. If we have [WD] a ~ ty -- work item [D] a ~ ty2 -- inert then we want to split the [WD] so we can get [D] ty ~ ty2. But otherwise there is no point.
Richard do you agree?
I'll try that out.
Meanwhile to get you rolling, you can replace rewritableTyVars with tyCoVarsOfType and it'll all work, just a bit less efficiently.
Thanks Simon! Indeed that allows things to proceed and in the process, confirms that there is a bug in my solver logic. Cheers, - Ben