fun with coe_fn

Stream: general

[Kenny Lau]

universe u

structure fun_wrapper (A : Type u) : Type u :=
(to_fun : A → A)

instance fun_wrapper.has_one (A : Type*) : has_one (fun_wrapper A) := ⟨⟨id⟩⟩

instance fun_wrapper.has_coe_to_fun (A : Type*) : has_coe_to_fun (fun_wrapper A) :=
⟨_, fun_wrapper.to_fun⟩

theorem foo : ((1 : fun_wrapper ℕ) : unit → empty) = id := rfl

[Kenny Lau]

question: what's the type of id in the statement of foo?

[Kenny Lau]

@Mario Carneiro how does type ascription work?

[Patrick Massot]

Kenny, the new widget interface answers your question about foo

[Patrick Massot]

id is natural number id

[Mario Carneiro]

That is pretty interesting. I haven't run the code yet, but I assume it typechecks, and my guess is the following:

• (1 : fun_wrapper ℕ) has the expected meaning, the wrapper around @id ℕ
• Because this has type fun_wrapper ℕ does not have the type unit -> empty or unify with it, lean inserts a coe_fn into the term
• Now the resulting term coe_fn (@has_one.one (fun_wrapper ℕ) ...) = id is typechecked, finishing up the remaining holes in the term around coe_fn and id.
• Importantly, the type ascription : unit -> empty is now gone, because it has no representation as an expr. We only have a few metavariables left to solve in an otherwise complete expr
• The fun_wrapper.has_coe_to_fun instance is inserted, which means that the result type is ℕ -> ℕ, so the rhs is inferred to be @id ℕ, and we are done.

[Mario Carneiro]

Note the difference with coe : A -> B, where the output has type B, so a type ascription will cause @coe ?A ?B ... to solve the ?B metavariable. In coe_fn there is no metavariable B, it is a delayed unification of the form has_coe_fo_fun.F ?C ?x =?= B, which doesn't help to solve for ?C. I guess lean forgot about this unification constraint when it decided to insert the coe_fn in the term