ring_aut coerce to function

Stream: general

[Kenny Lau]

import data.equiv.ring
#check λ (α : Type*) [ring α] (g : ring_aut α) (x : α), g x
/-
function expected at
  g
term has type
  α ≃+* α
-/

[Kenny Lau]

what's the canonical workaround?

[Chris Hughes]

g.to_equiv

[Kevin Buzzard]

For some reason they decided that a coercion to a function was not a good idea?

[Kenny Lau]

well that wouldn't be structually equivalent

[Kevin Buzzard]

Why not?

[Kenny Lau]

I've found that this works:

(@has_coe_to_fun.coe (α ≃+* α) _ g : α → α) x

[Kenny Lau]

Kevin Buzzard said:

Why not?

because it doesn't use has_coe_to_fun.coe

[Kevin Buzzard]

Oh so there _is_ a coercion to fun?

[Kenny Lau]

yeah

[Kevin Buzzard]

So just coercing g to \a -> \a directly doesn't work?

[Kevin Buzzard]

Is this something to do with coe_t or has_lift or whatever? I've never understood the details of that stuff

[Kevin Buzzard]

Can you fix it with \u= ?

[Kenny Lau]

I don't think I can.

[Reid Barton]

No, there isn't a coercion to fun. (I don't know why not.) An instance for a defeq type is not an instance for the original type.

[Kenny Lau]

There is a coercion to fun though. It's called ring_equiv.has_coe_to_fun

[Reid Barton]

Okay, but it's not an instance for ring_aut.

[Chris Hughes]

Should we make ring_aut reducible? That method worked okay for perm

[Kenny Lau]

oh, that's the reason

[Kenny Lau]

so g.to_equiv is the canonical way?

[Chris Hughes]

I think there isn't a canonical way right now. But making ring_aut reducible fixes it.

[Chris Hughes]

#2563

[Kevin Buzzard]

Thanks