The Coq mailing list

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

On Sat, 6 Feb 2021 11:06:58 +0100
Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

> Hi Jonathan
> Nice trick. I never realized that I was creating new constraints by
> doing this carelessly.
> P

Unfortunately, it doesn't quite work either.  The issue with:

Ltac issubtype A B :=
  first [constr_eq_strict A B
        |let _:=constr:(B:A) in fail 1 B "can be <=" A
        |assert_succeeds (let _:=constr:(A:B) in idtac)
        |fail 1 A "and" B "are constrained to be unrelated"
        ].

is that if A is in Type then A might be a sort or a type.  Unfortunately
there is no way for the tactic to know which it is going to be - and
issubtype's "(B:A)" test only works to filter out bad cases if A is
clearly a sort (when B is at least a type, possibly a sort).

For instance:

Definition test@{i j}(X:Type@{i})(Y:Type@{j}) : True.
Proof.
  issubtype X Type@{j}.  (*does not fail, but I want it to fail*)

Maybe the necessary trick is to first check if issubtype (type of A)
(type of B) - and only if this passes check issubtype A B:

  let tA:=type of A in
  let tB:=type of B in
  issubtype tA tB; isssubtype A B.

Or, actually, I don't think I need that final issubtype A B check as
issubtype tA tB is conclusive...?