Type inference on `→` vs `≃`

Stream: general

[Eric Wieser]

Why is lean able to infer types for the expression using f (→) but not g (≃)?

import data.real.basic
import data.equiv.basic

def wrapped (α : Type) := α

variables {α : Type}

def f : α → wrapped α := sorry
def g : α ≃ wrapped α := sorry

variables (n : ℕ) (x : ℝ)

#check (f (n * x) : wrapped ℝ)   -- ok, lean works out that I mean
#check (f (n * x : ℝ) : wrapped ℝ)   -- this, which also works

#check (g (n * x) : wrapped ℝ)   -- fail - why can't lean work out that I mean
#check (g (n * x : ℝ) : wrapped ℝ)  -- this, which doesn't fail

(this makes #4346 fail)

[Adam Topaz]

This works:

#check (g ((n : ℝ) * x) : wrapped ℝ)

[Adam Topaz]

It must be something about how lean decides to coerce a function

[Adam Topaz]

My guess is that it sees n which has type nat and things "okay, g should be a function on nat" and then it doesn't know what to do with the x which is a real number.

[Chris Hughes]

For ≃ the elaborator has to search for a has_coe_to_fun instance for equiv. It has something to do with that, not sure of the precise details.

[Eric Wieser]

Once it finds the docs#has_coe_to_fun instance, shouldn't it discover that g coerces to α → wrapped α, and apply the same rules as f?

[Adam Topaz]

But it sees nfirst.

[Adam Topaz]

So I imagine it thinks g should be a function on nat.

[Eric Wieser]

type inference is outside in, isn't it?

[Adam Topaz]

For example both

#check (g x)
#check (g n)

work

[Adam Topaz]

Yeah, but I think this means that it would look for a coercion of g to a function from nat to wrapped \R.

[Adam Topaz]

But honestly I don't really know the details of how this stuff works. @Mario Carneiro is probably the person to ask.

[Eric Wieser]

But that's not how the API of has_coe_to_fun looks - it's not like has_coe where there's a target type too - has_coe_to_fun.F specifies the type once it has been found for g

[Adam Topaz]

So the error under the g in your example says: term has type wrapped \N but it is expected to have type wrapped \R. So this makes me think that it sees n, and finds the coercion of gto \a \to wrapped \a, but fails because you explicitly told it to have type wrapped \R.

[Adam Topaz]

There is also an error under * because it doesn't know how to handle the coercion from nto \R.

[Eric Wieser]

If you look at the order of the errors in the output log, the * error comes first

[Adam Topaz]

This works:

#check (g (↑n * x) : wrapped ℝ)

[Eric Wieser]

As does reversing the order of the multiply

[Adam Topaz]

Also this:

#check (g $ ↑n * x)

[Eric Wieser]

Thanks for suggesting ↑, that seems unobtrusive enough to solve my problem. Would still like to hear from @Mario Carneiro why things are the way that they are.