Typeclass search with implicit arguments

Stream: lean4

[Christian Merten]

Consider the following MWE (cc @Jiang Jiedong):

def Bar (R : Type) : Type := R

class Foo {R : Type} (f : R → R) : Prop where
  foo {a : R} (h : f a = f a) : True

def baz (R : Type) : Bar R → R := id

instance boo (R : Type) : Foo (baz R) where
  foo _ := trivial

example (R : Type) (a : Bar R) (ha : baz R a = baz R a) : True :=
  /- it fails after commenting the next line out -/
  haveI : Foo (baz R) := inferInstance
  Foo.foo ha

Enabling pp.all true yields that in the last line, @Foo R (baz R) is searched for, but boo has type @Foo (Bar R) (baz R). This makes sense, as the type of R is probably inferred from the equality ha which lives in R. But adding the line haveI : Foo (baz R) := inferInstance makes it work and trace.Meta.synthInstance reveals that it now in the last line checks this local instance and some unification (?) applies and yields the result.

Is there any mechanism to make this work without the haveI (and without explitly passing more arguments to Foo.foo)?

[Edward van de Meent]

make Bar into an abbrev

[Edward van de Meent]

if this is considered a "cheat" solution, could you try and provide a mwe using

structure Bar (R : Type) : Type where
  r:R

Because i'm not sure what you're trying to do, and i believe right now there is no point where the Coe instance you defined gets used.

[Edward van de Meent]

right now, your mwe uses defeq only

[Christian Merten]

Oh yes, the Coe is irrelevant, that is a miscopy from a previous iteration (edited above).

[Kevin Buzzard]

Does something like set_option synthPendingDepth 2 fix it? I'm on mobile and going by memory so that might not be exactly right, but autocompletion should find what I really mean. Meta.synthPendingDepth maybe?

[Kyle Miller]

Christian Merten said:

Is there any mechanism to make this work

Yes:

instance boo {R : Type} : @Foo R (baz R) where
  foo _ := trivial

It's sort of random whether Foo (baz R) elaborates to @Foo R (baz R) or @Foo (Bar R) (baz R), so it seems better to be explicit.

(It's not really random, but it's not immediately obvious which it would be.)

[Christian Merten]

Kevin Buzzard said:

Does something like set_option synthPendingDepth 2 fix it? I'm on mobile and going by memory so that might not be exactly right, but autocompletion should find what I really mean. Meta.synthPendingDepth maybe?

Do you mean maxSynthPendingDepth? If yes, this does not fix it.

[Christian Merten]

Edward van de Meent said:

if this is considered a "cheat" solution, could you try and provide a mwe using

structure Bar (R : Type) : Type where
  r:R

Because i'm not sure what you're trying to do, and i believe right now there is no point where the Coe instance you defined gets used.

This came up while debugging #17403 (see in particular https://github.com/leanprover-community/mathlib4/pull/17403#issuecomment-2418322525).

[Christian Merten]

Kyle Miller said:

Christian Merten said:

Is there any mechanism to make this work

Yes:

instance boo {R : Type} : @Foo R (baz R) where
  foo _ := trivial

It's sort of random whether Foo (baz R) elaborates to @Foo R (baz R) or @Foo (Bar R) (baz R), so it seems better to be explicit.

(It's not really random, but it's not immediately obvious which it would be.)

Yes, this works. Still there seems to be a difference between the local instance variable as introduced in the haveI line and the global boo one, although (without your explicit type suggestion in boo) they both have type @Foo (Bar R) (baz R). Are local instance variables tried more liberally in instance search than global ones?

[Matthew Ballard]

Making Lean unify R → R and Bar R → R when Bar is a type synonym seems like a recipe for a bad time.

[Christian Merten]

Matthew Ballard said:

Making Lean unify R → R and Bar R → R when Bar is a type synonym seems like a recipe for a bad time.

If I understand things correctly, this is what we are doing when using CommRingCat.of and the related FunLike instances.

[Kyle Miller]

Christian Merten said:

Are local instance variables tried more liberally in instance search than global ones?

Yes they are. They're tried first, and they're tried with defeq, without making use of a discrimination tree.