Zulip Chat Archive

Stream: general

Topic: fun with coe_fn


view this post on Zulip Kenny Lau (Aug 03 2020 at 13:34):

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

view this post on Zulip Kenny Lau (Aug 03 2020 at 13:34):

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

view this post on Zulip Kenny Lau (Aug 03 2020 at 13:37):

@Mario Carneiro how does type ascription work?

view this post on Zulip Patrick Massot (Aug 03 2020 at 13:47):

Kenny, the new widget interface answers your question about foo

view this post on Zulip Patrick Massot (Aug 03 2020 at 13:47):

id is natural number id

view this post on Zulip Mario Carneiro (Aug 03 2020 at 14:01):

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.

view this post on Zulip Mario Carneiro (Aug 03 2020 at 14:05):

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


Last updated: May 13 2021 at 22:15 UTC