Lean doesn't try to coerce

Stream: lean4

[Alastair Horn]

Why doesn't Lean try to coerce the new type below to Nat? Is there a way to make it do this? I'm on the latest stable release.

#XY: In my actual code I'm doing this for the membership relation, not addition, but I think the issue is very similar, since it's the heterogeneity which causes the issue.

inductive Example where
| exam : Example

instance: Coe Example Nat := ⟨fun _ => 0⟩

#check 2 + Example.exam

[Moritz Doll]

how should Lean know which coercion you want to have? Imagine you have coercions to Nat and Foo and Foo has also a HAdd instance with Nat.

[Moritz Doll]

the check is fine if you use 2 + (Example.exam : Nat)

[Chris Bailey]

Or #check ((2 + Example.exam) : Nat). IIRC the rule is that anything not marked as an outParam needs to be known before Lean will try to find stuff.

[Chris Bailey]

In this case I think it works with Nat _ Nat because there's a default instance instance [Add α] : HAdd α α α where

[Moritz Doll]

this is interesting, in Chris' version Lean really wants to have a Coe Example Nat instance, even though it is not really stated.

inductive Example where
| exam : Example

inductive Foo where
| foo : Foo

instance : Coe Example Nat := ⟨fun _ => 0⟩
instance : HAdd Nat Foo Nat where
  hAdd := fun a _ => a + 1

instance : HAdd Nat Example Nat where
  hAdd := fun a _ => a + 1

instance : Coe Example Foo := ⟨fun _ => Foo.foo⟩

#eval 2 + (Example.exam : Nat) -- always 2
#eval 2 + (Example.exam : Foo) -- always 3
#eval (2 + Example.exam : Nat) -- 2 if the Coe Example Nat instance exists, 3 otherwise

[Moritz Doll]

and even with high priority on HAdd Nat Example Nat, it really wants to go through the homogeneous addition

[Alastair Horn]

Moritz Doll said:

how should Lean know which coercion you want to have? Imagine you have coercions to Nat and Foo and Foo has also a HAdd instance with Nat.

My question is how do I tell lean that that's the coercion to expect, without adding type information every time?

[Chris Bailey]

Going back to what you said at the beginning about your use case, you might try adding a default instance for your membership instance.

The specific example of HAdd in that isolated context without the expected type is sort of an edge case, but as soon as the expected type is known (as it usually would be in context) the default instance kicks in.