Overlapping instances cause infinite loop (in previously well-typed program)

[omelkonian]

Overlapping instances cause infinite loop (in previously well-typed program)

[UlfNorell]

From the manual:

Be aware that enabling this flag might lead to an exponential slowdown in instance resolution and possibly (apparent) looping behaviour.

Looks like you found some actually looping behaviour. The problem seems to be that the instance goals are solved in the wrong order: when we try to solve the argument to ¿_¿, we haven't solved the argument to _≤_ yet, so instance search (with --overlapping-instances) falls into a death spiral trying to apply the _×_ instance over and over again.

I'm not sure if this is what you should expect from using --overlapping-instances or if it's an actual bug. @jespercockx ?

It also reproduces on master.

[jespercockx]

The --overlapping-instances makes Agda more eager to start recursively searching for instances before it has determined a unique instance candidate at the top-level. Hence enabling it can make Agda go down an infinite rabbit hole while that rabbit hole could actually be ruled out if we just postpone the instance search a bit. So it is in general not a conservative extension. Perhaps this should be mentioned explicitly in the user manual.

For this particular example I agree that there's no real reason for Agda to loop. My guess would be that the instance search kicks in "too early" before we have propagated the annotated type into the type of the instance meta. In other words, Agda just sees an instance meta of type Dec _X and before it has figured out the actual value of _X it eagerly tries the instance for Dec (A × B).

We used to have a heuristic that prevented these cases, but it was very buggy and unmaintained and we ended up removing it (see #3419). In general it is easy to point at specific examples and point out "Oh it's obvious what I mean, why is Agda so stupid?" but designing a heuristic that works well in all cases has so far turned out to be impossible. (And before you say "why can't we just wait until the full type of the instance meta is resolved?" first take a look at #723 and #2760.)

In general I would discourage the use of --overlapping-instances and instead either redesign your classes/instances so it is not necessary, or (if you must) implement your own resolution with a macro.

[omelkonian]

I understand that the heuristics cannot be principled and there will always be corner cases.

What I am suggesting however pertains to the cases where non-overlapping search succeeds; couldn't the overlap search be redesigned in a conservative way, where first the non-overlapping search is tried and only if it fails do the heuristics kick in?

[jespercockx]

What happens without overlapping instances is that the instance constraint is first postponed and later tried again when we have more information about the goal type. So what you are asking for is that we also postpone instance constraints with overlapping instances, and only try to solve it at the last possible moment (i.e. just before it would get frozen). That would require messing with the order in which constraints are solved, but it seems possible in theory. I believe @UlfNorell once implemented something like that, but I am not sure what happened with it since then.