Stream: Coq devs & plugin devs

Topic: non-transitive module subtyping


view this post on Zulip Jason Gross (Feb 28 2023 at 00:04):

It's supposed to be the case that if A <: B and B <: C then A <: C, right?

view this post on Zulip Jason Gross (Feb 28 2023 at 00:10):

(It's currently not the case, and has not been the case at least since Coq 8.4:

Module Type C. Axiom t : Type. Axiom a : @id Type t. End C.
Module Type B <: C. Axiom t : Type. Axiom a : t. End B.
Module Type A <: B. Axiom t : Set. Axiom a : @id Set t. End A.
Module Type A' <: B := A.
Module Type A'' <: B <: C := A.
(* Error: Universe inconsistency. Cannot enforce Set = foo.2 because foo.2 < foo.1
<= foo.2 = Set.
*)

)


Last updated: Mar 28 2024 at 09:01 UTC