Odd type class failure

Stream: lean4

[Tomas Skrivan]

I have encountered this odd type class synthesis failure. I do not even know how to describe it, but it is an odd mix of reducible definition and a class in the assumption of another class

structure Foo where
  α : Type u

class Bar' (X : Type) (S : Foo)           extends Add X where
class Bar  (X : Type) (S : Foo) [Add S.α] extends Add X where

abbrev foo  : Foo := ⟨Nat⟩
def    foo' : Foo := ⟨Nat⟩
instance : Add foo'.α := instAddNat

example (X) [Bar' X foo]  : Add X := by infer_instance  -- works
example (X) [Bar  X foo'] : Add X := by infer_instance  -- works
example (X) [Bar  X foo]  : Add X := by infer_instance  -- fails
example (X) [Bar  X foo]  : Add X := Bar.toAdd foo      -- works

Anyone has any idea why is example (X) [Bar X foo] : Add X := by infer_instance failing to synthesize an instance?

[Sebastian Reichelt]

Looks like Lean doesn't see the two occurrences of ⟨Nat⟩ as the same. It works if you change foo like this.

def    foo' : Foo := ⟨Nat⟩
abbrev foo  : Foo := foo'

The error is still strange IMHO.

[Sebastian Reichelt]

Oh, it works if S is an outParam:

structure Foo where
  α : Type u

class Bar' (X : Type) (S : outParam Foo)                      extends Add X where
class Bar  (X : Type) (S : outParam Foo) [outParam (Add S.α)] extends Add X where

abbrev foo  : Foo := ⟨Nat⟩
def    foo' : Foo := ⟨Nat⟩
instance : Add foo'.α := instAddNat

example (X) [Bar' X foo]  : Add X := by infer_instance  -- works
example (X) [Bar  X foo'] : Add X := by infer_instance  -- works
example (X) [Bar  X foo]  : Add X := by infer_instance  -- works
example (X) [Bar  X foo]  : Add X := Bar.toAdd          -- works

[Tomas Skrivan]

Sebastian Reichelt said:

Looks like Lean doesn't see the two occurrences of ⟨Nat⟩ as the same. It works if you change foo like this.

def    foo' : Foo := ⟨Nat⟩
abbrev foo  : Foo := foo'

The error is still strange IMHO.

Sure, but that way foo.1 is not Nat but foo'.1 and defeats the whole purpose why foo is abbrev.

[Tomas Skrivan]

Oh, it works if S is an outParam

Interesting, what is going on there?

[Tomas Skrivan]

Another solution is to add: instance {X a} [Add a] [Bar X ⟨a⟩] : Add X := Bar.toAdd ⟨a⟩

[Sebastian Reichelt]

I hope someone more knowledgeable will chime in, but roughly speaking if you have an instance of Bar X foo in your context and want to synthesize Add X, Lean needs to infer the argument foo. Making the parameter an outParam causes it to always be inferred.
One important piece of the puzzle may be this: [Bar X foo] with Bar X foo extending Add X doesn't act like having [Add X] in your context. Instead, the instance of Add X is found by type class search, so first of all Bar X foo needs to be found in that particular call to infer_instance.

[Mac]

Tomas Skrivan said:

Oh, it works if S is an outParam

Interesting, what is going on there?

Without outParam on [Add S.α], it is a normal parameter of the the typeclass. That is, Bar is polymorphic in Add (S.α).