Record Subtyping in Coq, questions and references requested

Question

I've been looking for references discussing subtyping in Coq with respect to records, but have come up dry.

I'm specifically wondering what the Record _ : _ := { _ :> * } syntax means, and how it behaves. Especially am confused when a Record has a mix of :> and : judgements, I suppose that all the normal subtyping relationships (including permutation) hold?

Please share any further references (typing rules, practical use of subtyping in Coq, etc) you think would relevant

As a side remark - is there any similair mechanism in Agda, if so are additional references for this point are welcome.

Answer 1

The syntax you are referring to is not that related to the notions of subtyping you usually find in the programming languages literature. This is probably why you are having trouble finding references on the subject. Declaring

Record foo := { bar :> nat; ... }.

Is just an abbreviation for

Record foo := { bar : nat; ... }.
Coercion bar : foo >-> nat.

This coercion declaration causes Coq to wrap any foo around a call to bar if it is used in a context that expects a nat. This coercion is normally invisible, but you can ask Coq to print coercions in all terms for you with the Set Printing All. command. It does not do anything fancy; in particular, it does not allow you to reorder the fields of a record declaration.