Closed UlfNorell closed 3 weeks ago
Bisection blames 403ee426.
This is PR (CC @plt-amy)
@plt-amy do you have some time to take a look at this?
What's interesting is that it works if you give the type argument to the (unused) Bool instance:
Bool-hasPreorder = HasPreorder Bool _ ∋ record {BoolOrder}
The only difference in this case is that we add the instance to the discrimination tree with the Bool directly:
added value Bool-hasPreorder to discrimination tree with case
case 0 of
HasPreorder² → case 0 of
Bool⁰ → done {Bool-hasPreorder}
instead of first adding it as
added value Bool-hasPreorder to discrimination tree with case
case 0 of
HasPreorder² → done {Bool-hasPreorder}
and only adding the refined version once the meta is solved. I haven't been able to figure out yet why this makes a difference.
Sure, I'll take a look.
@UlfNorell My immediate guess was right: this is a result of my rather silly attempts to avoid repeatedly waking up instances. The intent was to block on the metas that caused the discrimination tree to go off and find multiple instances:
instance candidates from signature for goal:
HasPreorder Nat __≈__52
{Nat-hasPreorder, Bool-hasPreorder} length: 2
blocker:
__≈__52
mutual block:
{}
As you can tell from the amount of Bool
s, this isn't exactly stellar code; turns out many things are sensitive to the order that instance constraints are solved in (like termination checking). Computing the type of a with
isn't one of the situations I accounted for. Fixes I can see:
checkCandidates
on average), so I'd be okay with getting rid of it. (i.e. delete InstanceArguments.hs lines 212-269)wakeupConstraints_
somewhere between inferring the type of the with
-scrutinee and computing the abstraction; the postpone-on-overlap doesn't fire when under wakeupConstraints_
. I don't know enough about the LHS checker to know where this would go, but I could have a poke.Thanks @plt-amy! I'm not sure if it's relevant, but I did some waking of instance constraints for with-abstraction in #6868.
The following works in agda-2.6.4.3 but fails on master.