Primitives are incorrectly considered convertible to anything by module subtyping

[SkySkimmer]

Require Import PrimInt63.
Open Scope int63_scope.

Module Type T.
  Primitive bar := #int63_sub.
End T.

Module F(X:T).
  Definition foo : X.bar 1 1 = 0 := eq_refl.
End F.

Module M.
  Definition bar := land.
End M.

Module N := F M. (* "bar := land" is subtype of "bar := #int63_sub"? *)

Lemma bad : False.
Proof.
  pose (f := fun x => eqb x 1).
  assert (H:f 1 = f 0) by (f_equal;exact N.foo).
  change (true = false) in H.
  inversion H.
Qed.

Print Assumptions bad.
(* Axioms:
land : int -> int -> int
int : Set
eqb : int -> int -> bool
*)

[mattam82]

Great find, just in time :)

[CohenCyril]

At least Print Assumptions prints something... 😆

[SkySkimmer]

The original example is rejected by coqchk but this slightly modified example is accepted:

Require Import PrimInt63.
Open Scope int63_scope.

Module Type T.
  Primitive bar := #int63_sub.

  Axiom bar_land : bar = land.
End T.

Module F(X:T).
  Definition foo : X.bar 1 1 = 0 := eq_refl.
End F.

Module M.
  Definition bar := land.
  Definition bar_land : bar = land := eq_refl.
End M.

Module N : T := M.

Module A := F N.

Lemma bad : False.
Proof.
  pose (f := fun x => eqb x 1).
  assert (H:f 1 = f 0).
  { f_equal. change 1 with (land 1 1).
    rewrite <-N.bar_land.
    exact A.foo. }
  change (true = false) in H.
  inversion H.
Qed.

[SkySkimmer]

I tried to get the inconsistency with empty Print Assumptions but it seems impossible:

• we can't use literals in the module type because they're only
  convertible to literals so we would need to use them in the
  implementation

• we can't use literals in the functor because "int" isn't registered
  after the module type we could register a separate Primitive int
  but then literals are of that type not X.int

• all primitive operations take some primitive value as argument except array max length
  array max length is expanded to a literal at declaration time

• we need to call a primitive with a literal to get it to evaluate in the functor otherwise we have nothing of interest

[JasonGross]

I tried to get the inconsistency with empty Print Assumptions but it seems impossible:

Belatedly, this one is closed under the global context (in 8.18.0), but does not pass coqchk.

Require Import BinInt PrimInt63.
Require Uint63.
Open Scope int63_scope.

Module Type T.
  Primitive bar := #int63_sub.

  Axiom bar_land : Uint63.to_Z (bar 1 1) = Uint63.to_Z (land 1 1).
End T.

Module F(X:T).
  Definition foo : Uint63.to_Z (X.bar 1 1) = Uint63.to_Z 0 := eq_refl.
  Lemma bad : False.
  Proof.
    pose (f := fun x => Z.eqb x 1).
    assert (H:f 1%Z = f 0%Z).
    { f_equal. change 1%Z with (Uint63.to_Z (land 1 1)).
      rewrite <-X.bar_land.
      exact foo. }
    change (true = false) in H.
    inversion H.
  Defined.
  Definition rbad := Eval cbv in bad.
End F.

Module M.
  Definition bar := land.
  Definition bar_land : Uint63.to_Z (bar 1 1) = Uint63.to_Z (land 1 1) := eq_refl 1%Z.
End M.

Module N <: T := M.

Module A := F N.

Print A.rbad.
Print Assumptions A.rbad.
(* Closed under the global context *)

[SkySkimmer]

It's possible to make coqchk accept it, just do an opaque Module N : T := M.. coqchk defunctorializes so the bad subtyping isn't trusted when applying a functor, but it relies on correct subtyping when opacifying a module.

PS: You can define bad directly without needing to use cbv:

  Definition bad :=
    match
      match
        match
          match
            (* cast so that the parameters cached in the match node don't refer to primitives *)
            match X.bar_land :> (0 = 1)%Z in (_ = a) return (a = 0%Z) with
            | eq_refl => eq_refl
            end in (_ = a) return (a = 1%Z)
          with
          | eq_refl => eq_refl
          end in (_ = a) return match a with
                                | 0%Z => True
                                | _ => False
                                end
        with
        | eq_refl => I
        end return (true = false)
      with
      end in (_ = b) return (b = false -> False)
    with
    | eq_refl =>
        fun H0 : true = false =>
          match
            match H0 in (_ = a) return (if a then True else False) with
            | eq_refl => I
            end return False
          with
          end
    end eq_refl.

(this is just what Print bad on your proof says + the cast as commented, turning it back into a nice-ish tactic sequence or term is left to the reader)

[SkySkimmer]

Thus simplified and coqchk accepted:

Require Import PrimInt63.
Open Scope int63_scope.

Module Type T.
  Primitive bar := #int63_sub.

  Axiom bar_land : eqb (bar 1 1) 1 = true.
End T.

Module F(X:T).
  Lemma bad : False.
  Proof.
    assert (H : false = true) by exact X.bar_land.
    inversion H.
  Defined.
End F.

Module M.
  Definition bar := land.
  Definition bar_land : eqb (bar 1 1) 1 = true := eq_refl true.
End M.

(* coqchk defunctorializes so the bad subtyping doesn't matter when applying a functor,
   but it relies on correct subtyping when opacifying a module *)
Module N : T := M.

Module A := F N.

Check A.bad : False.

Print Assumptions A.bad.
(* Closed under the global context *)