New subject: Panic from rewritableTyVarsOfType

3 Feb 2017


      Simon Peyton Jones  writes:
...
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

RE: Panic from rewritableTyVarsOfType

Ben Gamari

Ben Gamari

Simon Peyton Jones

tags

participants (2)