The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Thu, Jun 20, 2024 at 5:12 PM Jason Hu <fdhzs2010 AT hotmail.com> wrote:

Hi all,

I am reading the subtyping rules for Coq: https://coq.inria.fr/doc/V8.18.0/refman/language/cic.html#subtyping-rules

Rule 5 says that Coq only checks equivalence for the input types while only the output types are subject to subtyping. How is the subtyping rule is not contravariant in the input types?

I understand that in System F, this rule is problematic and causes undecidability but I don't think it applies here. In particular, if for the sake of discussion we let U <: T and compare x : U |- T' <: U', this extra information of x : U should affect the result of comparing T' <: U' at all.

It's not that obvious to me, since T' and U' can depend on x.

At any rate, in the non-dependent case, Coq's type-checker seems to simulate contravariance using eta-expansion:

Parameter F: Set -> Prop.

Check (F: Set -> Set).
(*
F : Set -> Set
     : Set -> Set
*)

Check (F: Prop -> Set).
(*
(fun x : Prop => F x) : Prop -> Set
     : Prop -> Set
*)

- Xavier Leroy

How is the rule designed in this way? What consideration am I missing here?

Thanks,

Jason Hu

https://hustmphrrr.github.io/