Shea Levy (Oct 23 2020 at 14:25): Shea Levy (Oct 23 2020 at 14:25):If I have some class Foo and some record like
Record Bar := { carrier; carrier_foo :> Foo carrier }.
I'd expect that whenever bar : Bar is in scope that instances for Foo bar.(carrier) would be automatically resolved, but this doesn't happen. Have I misunderstood what :> means?
Jakob Botsch Nielsen (Oct 23 2020 at 14:28):For that I think you need to make Bar a Class instead of Record
Shea Levy (Oct 23 2020 at 14:31):Ah, that worked! Does :> mean anything in a record? And will it screw things up to have a Class with no parameters that I don't ever intend to be resolved by typeclass lookup?
Li-yao (Oct 23 2020 at 14:32):In a record it makes a coercion.
Jakob Botsch Nielsen (Oct 23 2020 at 14:32):Right, for example:
Record foo := { x :> nat }.
Check (fun (x : foo) => x : nat).
works only becuase of :>
Shea Levy (Oct 23 2020 at 14:39):I see!
Gaëtan Gilbert (Oct 23 2020 at 14:40):in this case it may make more sense to do Record Bar := { carrier; carrier_foo : Foo carrier }. Existing Instance carrier_foo.
Gaëtan Gilbert (Oct 23 2020 at 14:40):(without the :> unless you also want it to be a coercion)
Paolo Giarrusso (Oct 23 2020 at 20:25):Is there a way to use an instance without the coercion?
Paolo Giarrusso (Oct 23 2020 at 20:26):S/use/get the effects of existing instance without getting the coercion/
Paolo Giarrusso (Oct 23 2020 at 20:26):Is :>> anyhow related?
Paolo Giarrusso (Oct 23 2020 at 20:27):(I’ve observed :> create coercions in Classes)
Gaëtan Gilbert (Oct 23 2020 at 20:48):I don't understand the question, Existing Instance doesn't make it a coercion
Gaëtan Gilbert (Oct 23 2020 at 20:48)::> means coercion for Record and instance for Class
Gaëtan Gilbert (Oct 23 2020 at 20:49):see https://github.com/coq/coq/pull/13106 for :>>
Paolo Giarrusso (Oct 23 2020 at 23:15):IME, :> for class means “coercion and instance”.
Paolo Giarrusso (Oct 23 2020 at 23:19):But I’ll try again.
Paolo Giarrusso (Oct 23 2020 at 23:27):Okay, a basic experiment agrees with you. I remember this thought came from some concrete experiment, but it might have been a mistake indeed.
Last updated: Oct 03 2023 at 20:01 UTC