Type class resolution only works with a name

Stream: general

[Bolton Bailey]

I have another question about variables and synthesis

import computability.encoding
import data.polynomial.basic
import data.polynomial.eval

section

variable {A : Type}
variable [computability.fin_encoding A]
-- variable [encA : computability.fin_encoding A] -- works
-- variable [_instfoobar : computability.fin_encoding A] --doesn't work

def dtime (t : ℕ → ℕ) (f : A -> Prop) : Prop
:= sorry

def polytime (f : A -> Prop) : Prop
:= ∃ (p : polynomial ℕ ), dtime (λ n, p.eval n) f

end

This code throws failed to synthesize type class instance for the dtime call. However, if I replace the line variable [computability.fin_encoding A] with variable [encA : computability.fin_encoding A] everything is fine. This is pretty confusing, since the reference manual says of implicit arguments

The name of the variable can be omitted from a class resolution argument, in which case an internal name is generated.

From this quote I would expect the behavior of these two versions to be the same.

Further exploration shows that an error is thrown even when the name of the fin_encoding instance is inserted manually, as long as the name starts with the characters _inst. What is going on?

[Kevin Buzzard]

docs#computability.fin_encoding

[Kevin Buzzard]

Looks to me like it's a structure but not a class so you shouldn't be using square brackets at all

[Bolton Bailey]

Then why doesn't the compiler complain at all when I name the value?

[Mario Carneiro]

Named and unnamed typeclass variables behave differently, in that unnamed typeclass variables are included if all their dependents (here A) are required for the theorem statement, while named typeclass variables are included only if the variable itself (encA) is used in the theorem statement. You might have stumbled on a non-hygiene situation though with your tricky name _instfoobar, which probably tricks lean into thinking that it's an unnamed instance since unnamed instances have autogenerated names starting with _inst

[Bolton Bailey]

Ok thanks. Just one more question: Is there some technical or philosophical reason why computability.fin_encoding is not a class here? To me, this feels analogous to me to other classes in Lean, like algebra.field. In both cases there are objects and propositions associated with each instance. Also, it feels like it should be possible to use the "chaining" feature of type classes to chain instances of computability.fin_encoding, for example, to implement an encoding for pairs of encodable types.

[Eric Wieser]

If it were a typeclass, it would be saying "there is a canonical encoding of nat", just as field says "there is a canonical field structure on the reals"