coercion to function needs some hints

Stream: lean4

[Kevin Buzzard]

structure equiv (α : Sort u) (β : Sort v) :=
(to_fun    : α → β)
(inv_fun   : β → α)

infix:25 " ≃ " => equiv

namespace equiv

instance : CoeFun (α ≃ β) (λ _ => α → β) :=
⟨to_fun⟩

def symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun⟩

def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ (e₁ : α → β), e₁.symm ∘ (e₂.symm : γ → β)⟩

end equiv

In Lean 3, one would just have been able to do e₂ ∘ e₁; in Lean 4 we need to give it some more hints. Is this expected behaviour?

[Daniel Selsam]

@Kevin Buzzard The issue is that typeclass synthesis is not allowed to assign metavariables that it did not create. In your example, the β is unknown when the CoeFun is tried. This is a known issue and related to https://github.com/leanprover/lean4/issues/403

[Patrick Massot]

This is a really import issue (and I can totally believe it's very non-trivial). Smooth coercions are really a crucial part of the user experience.

[Daniel Selsam]

Patrick Massot said:

This is a really import issue (and I can totally believe it's very non-trivial). Smooth coercions are really a crucial part of the user experience.

I added the example to the GitHub issue.

[Eric Wieser]

Can unification hints help here in any way?

[Daniel Selsam]

No need. It is easy to allow TC to assign metavariables -- it was a design decision to disallow this in general. So, we might be able to address this issue by just having the elaborator disable this restriction when synthesizing instances for coercions.

[Daniel Selsam]

It is supporting tactics during coercions that would require a substantial refactoring.

[Mario Carneiro]

Daniel Selsam said:

No need. It is easy to allow TC to assign metavariables -- it was a design decision to disallow this in general. So, we might be able to address this issue by just having the elaborator disable this restriction when synthesizing instances for coercions.

What about disabling the restriction when unifying out parameters? (In this case, we want the out parameter (λ _ => α → β) to cause β to be unified.) Focusing on coercions seems unnecessarily specific.

[Daniel Selsam]

Mario Carneiro said:

Daniel Selsam said:

No need. It is easy to allow TC to assign metavariables -- it was a design decision to disallow this in general. So, we might be able to address this issue by just having the elaborator disable this restriction when synthesizing instances for coercions.

What about disabling the restriction when unifying out parameters?

I proposed that here https://github.com/dselsam/mathport/issues/5#issuecomment-771997626 but never followed up with Leo after his response. I don't know what problems it would cause -- my coe-specific comment wasn't really a suggestion, I mainly just meant to clarify the point that the feature in question isn't technically difficult to support but merely a design question.

[Mac]

Mario Carneiro said:

What about disabling the restriction when unifying out parameters? (In this case, we want the out parameter (λ _ => α → β) to cause β to be unified.)

I don't think that would help here. The coercion in this case would not be using CoeFun directly but rather the CoeFun instance of CoeT and CoeT does not have an out param.

[Mac]

Daniel Selsam said:

I proposed that here https://github.com/dselsam/mathport/issues/5#issuecomment-771997626

It is worth noting that issue was about filling universe metavariables whereas this case involves metavariables for normal types. Thus, it would likely require an even more general solution. In fact, it is an even more general case than the example in the first post of https://github.com/leanprover/lean4/issues/403 as it is not using CoeFun directly but rather indirectly through CoeT (at least I think so?).

[Gabriel Ebner]

In case anybody else was also wondering what has changed in Lean 4 so that this no longer works: in Lean 3, coercions to functions are handled specially by the elaborator. If it sees that the expected type is a function type, then it synthesizes (the Lean 3) equivalent of CoeFn (α ≃ β) ?m, which works because ?m is an out param. Then ?m is unified with the expected type normally, and can therefore assign the metavariable in the expected type.

[Gabriel Ebner]

(A similar special case exists for type coercions.)

[Kevin Buzzard]

Can one somehow use the fact that if a type coerces to a function type then one could in practice "guarantee" that it will only coerce to one function type? Or does this not help?

[Gabriel Ebner]

Yes, this is in a way what Lean 3 did and what out param means.

[Mac]

Gabriel Ebner said:

If it sees that the expected type is a function type, then it synthesizes (the Lean 3 equivalent of) CoeFn (α ≃ β) ?m

Are you sure? I thought CoeFun was only used in situations where a given foo was applied (i.e. foo 0 would use CoeFun). However, when a function type is merely expected it uses CoeT (i.e. foo : Nat -> Nat uses CoeT). For example, consider the following:

universes u v

structure Fun (A : Sort u) (B : Sort v) where
  fn : A -> B

def idd {A : Sort u} : Fun A A
  := Fun.mk id

instance {A : Sort u} {B : Sort v} : CoeFun (Fun A B) (fun _ => A -> B)
  := ⟨ Fun.fn ⟩

#check idd 0 -- Works
#check (idd : Nat -> Nat) -- Errors

[Mac]

(There is also the annoying fact that the function coercion results in a unsightly being Fun.fn being introduced into the pretty print.)

[Gabriel Ebner]

I was talking about Lean 3:
https://github.com/leanprover-community/lean/blob/13da8a7ff12ce726551287f39e5883f5dcaa7aff/src/frontends/lean/elaborator.cpp#L699