Unnamed instance arguments not considered for instance resolution

[omelkonian]

In contrast to "don't care" instance arguments of the form {{ _ : P }}, unnamed instance arguments of the form {{ P }} are not considered as candidates in this case:

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

record Def (A : Set) : Set where
  field def : A
open Def ⦃...⦄

_ = ⦃ _ : Def Nat ⦄ → def ≡ 0 -- this works
_ = ⦃ Def Nat ⦄ → def ≡ 0 -- this fails

Is this intended? If so, the docs should be updated under 'Find candidates'.

AGDA: 2.6.1.3

[jespercockx]

Interesting. Knowing the implementation I can see why this happens: a dependent function type (even one with an argument named _) brings a new variable into scope, while a non-dependent function type does not. So in the latter case there is no variable in the context for instance search to find.

agda/src/full/Agda/TypeChecking/Rules/Term.hs

Lines 115 to 129 in 007a26f

	A.Fun i (Arg info t) b -> do
	a <- setArgInfo info . defaultDom <$> checkPiDomain (info :| []) t
	b <- isType_ b
	s <- inferFunSort (getSort a) (getSort b)
	let t' = El s $ Pi a $ NoAbs underscore b
	--noFunctionsIntoSize t'
	return t'
	A.Pi _ tel e -> do
	(t0, t') <- checkPiTelescope (List1.toList tel) $ \ tel -> do
	t0 <- instantiateFull =<< isType_ e
	tel <- instantiateFull tel
	return (t0, telePi tel t0)
	checkTelePiSort t'
	--noFunctionsIntoSize t'
	return t'

It wouldn't be hard to change this, but it would mean that suddenly {{ A }} -> B can denote a dependent function space. So we would lose the ability to express that a function with an instance argument is definitely totally non-dependent.

I don't see why the ability to express this is particularly useful so I would be happy with changing it, but perhaps there are use cases of the current behaviour that I don't think of at the moment.

[MatthewDaggitt]

Heads up that I've also come across this recently in agda/agda-stdlib#1538. e.g.
https://github.com/agda/agda-stdlib/blob/2c2490faea53e1e15fbf2b5ec8081bd564716717/src/Data/Nat/DivMod.agda#L74-L83

It's quite noisy to have to write ⦃ _ : NonZero ⦄ absolutely everywhere, and would be nicer to have a cleaner syntax for this

[gallais]

I don't see why the ability to express this is particularly useful

We have many non-dependent specialised versions of more general higher order
combinators in the standard library because the non-dependent version leads
to better reconstruction of the implicit arguments via unification.

I don't think it's that big of a deal that you need to name an argument for
it to be available in the codomain. If the worry is consistency then I'd
advocate going in the other direction and enforcing that _ consistently
means "throw away" in a binding position i.e. making {{_ : ...}} mean {{...}}.

[omelkonian]

If the worry is consistency then I'd
advocate going in the other direction and enforcing that _ consistently
means "throw away" in a binding position i.e. making {{_ : ...}} mean {{...}}.

IMO it would be annoying to have to find a meaningful name for these instance arguments, although 99% of the time you are not actually using it to the right of the arrow (that's why they are instance arguments anyway!). It's funny that dependencies involving implicit arguments is syntactically explicit, while ones that involve instance arguments are implicit :P.

Would it be possible to statically compute a dependency graph from the type on the right and somehow decide whether the instance argument on the left should be considered for resolution or not? If not, then I guess the current state of affairs is acceptable if documented properly: you just have to put an underscore to make it a dependent function which should not be needed that often anyway.

[jespercockx]

IMO it would be annoying to have to find a meaningful name for these instance arguments, although 99% of the time you are not actually using it to the right of the arrow (that's why they are instance arguments anyway!). It's funny that dependencies involving implicit arguments is syntactically explicit, while ones that involve instance arguments are implicit :P.

There is a difference between using an instance argument in the type and using it in the body of the function. For the latter, both versions of instance arguments are considered by instance search. So it is only if you want the type of the function to depend on the instance argument, that you need to write {{_ : A}} instead of {{A}}. I'm not sure, but it feels to me that this would not actually be needed that often in practice.

[MatthewDaggitt]

So it is only if you want the type of the function to depend on the instance argument, that you need to write {{_ : A}} instead of {{A}}. I'm not sure, but it feels to me that this would not actually be needed that often in practice.

I think it might be used more than you think! See https://github.com/agda/agda-stdlib/blob/2c2490faea53e1e15fbf2b5ec8081bd564716717/src/Data/Nat/DivMod.agda#L74-L83 for an example where I'm proposing to have a lot of types which depend on the instance argument.

[UlfNorell]

I think the status quo is the most sensible. Not having to write {{_ : A}} would of course be convenient, but at the price of introducing an ad hoc exception to the type language.

The fact that the _ is available for instance search is quite natural; instance search uses unnamed variables all the time. I think the only confusion is that there isn't a mechanism by which naming a variable _ excludes it from instance search.

[andreasabel]

At first sight it is surprising that {{P}} -> A should be different from {{_ : P}} -> A, but we can verbalize the first as non-dependent functions space and the second as potentially dependent function space where I do not mention the name of the argument because I can live without giving it a name.

[MatthewDaggitt]

Okay, so it sounds like the consensus is that the distinction is useful. The next question is how can we stop the user from shooting themselves in the foot with this feature. I've spent at least 20 frustrating minutes trying to work out why the following:

0/n≡0 : ∀ n {{NonZero n}} → 0 / n ≡ 0
0/n≡0 (suc n-1) = refl

gives me a "No instance available" error message and I'm sure I'm not the only one. Documenting it would obviously help, but is there some way we could display a more informative error message. Maybe if instance resolution fails, Agda could retry instance resolution with the non-dependent instance arguments now in scope, and then raise an informative error message suggesting that they be made dependent if it then succeeds?

[MatthewDaggitt]

Actually on second thoughts, you wouldn't even need to retry instance resolution. You could simply detect the presence of non-dependent instance arguments and add a possible fix: change {{NonZero n}} to {{_ : NonZero n}} line to the error message?

[jespercockx]

How specific would you want this warning to be? Would it be fine if it mentioned all the unnamed instance arguments that are currently "in scope" or would you only want those that would actually make the instance resolve?

[MatthewDaggitt]

I mean in an ideal world the latter, but I think the former would do the job fine 👍 Upon failure warn the user "Perhaps you meant to name one of the instance arguments X,Y,Z? Unnamed instance arguments are not considered in instance resolution in types." I think that would have been more than enough for me to have worked out what the problem was.