Instance resolution failure in Agda 2.6.4

[conal]

Instance resolution failure in Agda 2.6.4

[andreasabel]

Ok, thanks @conal, then we do not take further action here.

[jespercockx]

I think the problem here is that Agda's automatic insertion of implicit arguments is making the instance search go awry. In particular, if you make the x argument to q explicit then the example passes:

record Foo (X : Set) : Set₁ where
  field 
    Q : X → Set
    q : (x : X) → Q x

open Foo ⦃ … ⦄

module Test (A : Set) ⦃ FooA : Foo A ⦄ (B : Set) ⦃ FooB : Foo B ⦄ where

  works : (y : B) → Q y
  works = q

So the problem is that instance search does not get the task of searching for an instance inst where the type of q {{inst}} is {x : B} → Q {{inst}} x (which it could solve) but instead it it has to search for an instance inst where q {{inst}} {y} has type Q {{inst}} y. In the latter case there is no trace of the type A which it could use to choose the instance of type Foo B over the one of type Foo A.

Possible workarounds could be:

• Making the argument {x : X} explicit.
• Wrapping the type of q in a box that prevents Agda from eagerly inserting the implicit argument.
• Making Q into an additional parameter of the type class (so instance search can use Q to choose the instance rather than just X.

Would any of these options be acceptable to you? The goal of this change was to make instance search more predictable and performant, but this will inevitably lead to some cases like this where Agda has a harder time choosing the correct instance.

[jkopanski]

• Wrapping the type of q in a box that prevents Agda from eagerly inserting the implicit argument.

Would you be so kind and show what this would look like? I don't really understand this.

[conal]

Thank you for the tips, @jespercockx! Of your workaround suggestions, the first and third would be terribly awkward in practice, and the second I don’t understand.

[jespercockx]

What I meant with the second point is to define a type like

data Box (A : Set) : Set where
  [_] : A -> Box A

and change the type of q from {x : X} → Q x to Box ({x : X} → Q x). But that's probably going to be pretty awkward to work with too.

If none of the workarounds here are acceptable, I'm not sure what would be the best solution here. There are just too many different use cases for instance search, and every time we make a change that makes things better (more predictable, more efficient) for one use case this inevitably makes things worse for another use case elsewhere.

(One other workaround which you probably won't like is to use tactic arguments with a custom tactic instead of instance arguments. Here is an example of a little tactic that I wrote that relies on instance search but removes the uniqueness constraint: https://github.com/jespercockx/scope/blob/master/src/Utils/Tactics.agda#L31-L55, perhaps a similar tactic could be adapted to your use case.)

[conal]

Thanks again, @jespercockx! I think @jkopanski has found a strategy that we can live with. Theorems are still pretty (my top priority), and proofs are only mildly more verbose.