Stream: Coq users

Topic: Record with class instances?


view this post on Zulip 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?

view this post on Zulip Jakob Botsch Nielsen (Oct 23 2020 at 14:28):

For that I think you need to make Bar a Class instead of Record

view this post on Zulip 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?

view this post on Zulip Li-yao (Oct 23 2020 at 14:32):

In a record it makes a coercion.

view this post on Zulip 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 :>

view this post on Zulip Shea Levy (Oct 23 2020 at 14:39):

I see!

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 23 2020 at 14:40):

(without the :> unless you also want it to be a coercion)

view this post on Zulip Paolo Giarrusso (Oct 23 2020 at 20:25):

Is there a way to use an instance without the coercion?

view this post on Zulip Paolo Giarrusso (Oct 23 2020 at 20:26):

S/use/get the effects of existing instance without getting the coercion/

view this post on Zulip Paolo Giarrusso (Oct 23 2020 at 20:26):

Is :>> anyhow related?

view this post on Zulip Paolo Giarrusso (Oct 23 2020 at 20:27):

(I’ve observed :> create coercions in Classes)

view this post on Zulip Gaëtan Gilbert (Oct 23 2020 at 20:48):

I don't understand the question, Existing Instance doesn't make it a coercion

view this post on Zulip Gaëtan Gilbert (Oct 23 2020 at 20:48):

:> means coercion for Record and instance for Class

view this post on Zulip Gaëtan Gilbert (Oct 23 2020 at 20:49):

see https://github.com/coq/coq/pull/13106 for :>>

view this post on Zulip Paolo Giarrusso (Oct 23 2020 at 23:15):

IME, :> for class means “coercion and instance”.

view this post on Zulip Paolo Giarrusso (Oct 23 2020 at 23:19):

But I’ll try again.

view this post on Zulip 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: Feb 08 2023 at 23:03 UTC