The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Still not working.

#11435 comes up with "issubtype Type@{i+1} Type@{j+1}" which I want to
fail when i and j have no constraints between them.  The bug causes
them to pass because "constr:(Type@{i+1}:Type@{j+1})" fails to
typecheck when it should.

But, it's close:

Ltac issubtype A B :=
  first [let _:=constr:(B:A) in fail 1 B "can be ∈" A
        |lazymatch constr:((fun x=>x):(A->B)) with
         | fun x => x => idtac
         | _ => fail 1 "A coercion exists from " A "to" B
         end
        |fail 1 A "and" B "are constrained to be unrelated"
        ].

(*Get i and j as unrelated universes:*)
Example test@{i j}(A:Type@{i})(B : Type@{j}) : True. 
Proof.
  Fail issubtype A B.
  Fail issubtype B Type@{j}.
  Fail issubtype A Type@{j}.
  Fail issubtype B Type@{i}.
  Fail issubtype Type@{i} Type@{j}.
  Fail issubtype Type@{j} Type@{i}.
  issubtype Type@{i} Type@{max(i,j)}.
  issubtype Type@{i} Type@{max(i,j+1)}.
  issubtype Type@{i} Type@{max(i+1,j)}.
  issubtype Type@{i} Type@{i+1}.
  issubtype Set Type@{Set+1}.
  issubtype A A.
  issubtype Prop Set.
  issubtype SProp Set.
  Fail issubtype Set Prop.
  issubtype SProp Prop.
  Fail issubtype Prop SProp.