has_coe of function

Stream: general

[Sean Leather]

Are there any problems with a coercion of a function?

instance : has_coe (∀ a, β₁ a → β₂ a) (embedding β₁ β₂)

where embedding is a structure.

[Mario Carneiro]

does it work?

[Mario Carneiro]

I don't see any obvious issues that it would cause, although it might not work

[Sean Leather]

In one place, ↑ worked. In another, I had to use : sigma.embedding β₁ β₂.

[Mario Carneiro]

If B1 and B2 are metavariables, it will have trouble

[Mario Carneiro]

I now recall seeing issues like this with the coercion from order_iso to order_embedding

[Sean Leather]

Hmm. If I have to use an annotation, it's not really worth it.

[Gabriel Ebner]

Yeah, function coercions only trigger if there are no metavariables at all. This includes universe metavariables as well.

[Simon Hudon]

It might be worth defining your own up arrow instead (e.g. ⟰)

[Joe Hendrix]

I'm actually working through a similar issue, but where I want coercions to trigger over. type with. a single parameter. I have two types reg : type -> Type and lhs : type -> Type, and \forall tp, has_coe (reg tp) (lhs tp) that I want to trigger even when tp contains metavariables.

[Joe Hendrix]

I wish there was some way to control how defined a term had to be before searching for coercions.

[Sebastian Ullrich]

@jhx Yes, that is the biggest issue of using type class inference for coercions. We definitely want to fix this in the future, but we don't have a convincing alternative design yet https://github.com/leanprover/lean/issues/1402

[Joe Hendrix]

As a workaround, I've introduces a type class has_coe1, and explicitly tell the functions that expect an argument of the given type to use it.

class has_coe1 {α:Sort w} (f : α → Sort u) (g : α → Sort v) := (coe : Π{a : α}, f a → g a)

instance has_coe1_refl (α:Sort w) (f : α → Sort u) : has_coe1 f f := ⟨λa f, f⟩
instance all_reg_is_lhs   : has_coe1 reg lhs := sorry

...

section
parameter {f:type → Type}
parameter [has_coe1 f value]

def sext {w:ℕ} {f} [has_coe1 f value] (x:f (bv w)) (o:ℕ) : value (bv o) := ...

This approach might provide a more general solution to the monad special case mentioned in issue 1402, but still feels fairly special case.