Zulip Chat Archive

Stream: general

Topic: has_coe of function


view this post on Zulip Sean Leather (Aug 08 2018 at 14:45):

Are there any problems with a coercion of a function?

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

where embedding is a structure.

view this post on Zulip Mario Carneiro (Aug 08 2018 at 14:49):

does it work?

view this post on Zulip Mario Carneiro (Aug 08 2018 at 14:50):

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

view this post on Zulip Sean Leather (Aug 08 2018 at 14:51):

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

view this post on Zulip Mario Carneiro (Aug 08 2018 at 14:52):

If B1 and B2 are metavariables, it will have trouble

view this post on Zulip Mario Carneiro (Aug 08 2018 at 14:53):

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

view this post on Zulip Sean Leather (Aug 08 2018 at 14:54):

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

view this post on Zulip Gabriel Ebner (Aug 08 2018 at 15:23):

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

view this post on Zulip Simon Hudon (Aug 08 2018 at 20:20):

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

view this post on Zulip Joe Hendrix (Aug 08 2018 at 22:23):

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.

view this post on Zulip Joe Hendrix (Aug 08 2018 at 22:27):

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

view this post on Zulip Sebastian Ullrich (Aug 09 2018 at 03:37):

@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

view this post on Zulip Joe Hendrix (Aug 09 2018 at 05:47):

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.


Last updated: May 06 2021 at 22:13 UTC