`sauto` causes "Unable to handle arbitrary u+k <= v constraints."

[QinshiWang]

I encounter a strange problem. After a seemingly unrelated change, CoqHammer's sauto tactic does not work anymore in some goals, where it used to work. And it reports

Anomaly "Unable to handle arbitrary u+k <= v constraints."
Please report at http://coq.inria.fr/bugs/.

It seems that a certain proof searching step in sauto produces a universe constraint that Coq does not support. Coq only allows universe constraint in the form of u+k <= v where k is a constant. If this is the case, a possible fix is to locate what proof searching causes this constrain, and then either prevent this from happening or catch the exception and assume the proof searching step has failed.

I have a relatively small example of the issue, but it's based on our project. I can try to make an independent example if it is helpful.

[QinshiWang]

I encountered this issue again recently and was able to figure out a small example.

Require Import Coq.Lists.List.
Require Import Hammer.Plugin.Hammer.
Import ListNotations.

Class ExternSem := {
  extern_state : Type;
  (* sauto works if removing this line. *)
  AbsMet := extern_state -> extern_state -> Prop
}.

Section EXT.

Context {target : ExternSem}.

Definition EXT (a : list (extern_state -> Prop)) (es : extern_state) : Prop :=
  fold_right and True (map (fun (ep : extern_state -> Prop) => (ep es)) a).

End EXT.

Section ExtExtract.

Context {target : ExternSem}.

Fixpoint remove_nth {A} (n : nat) (al : list A) {struct n} : list A :=
  match n, al with
  | O, a :: al => al
  | S n', a :: al' => a :: remove_nth n' al'
  | _, nil => nil
  end.

Lemma test : forall n es,
  EXT (remove_nth n []) es.
Proof.
  (* sauto. *)
  (* Anomaly "Unable to handle arbitrary u+k <= v constraints."
     Please report at http://coq.inria.fr/bugs/. *)
  (* Fail sauto. *)
  (* Even this fails. *)
Abort.

End ExtExtract.

(* sauto works if a target is provided. *)

#[local] Instance target : ExternSem.
Admitted.

Lemma test : forall n es,
  EXT (remove_nth n []) es.
Proof.
  sauto.
Qed.

There is no problem if EXT and test are in the same section.

Require Import Coq.Lists.List.
Require Import Hammer.Plugin.Hammer.
Import ListNotations.

Class ExternSem := {
  extern_state : Type;
  AbsMet := extern_state -> extern_state -> Prop
}.

Section ExtExtract.

Context {target : ExternSem}.

Definition EXT (a : list (extern_state -> Prop)) (es : extern_state) : Prop :=
  fold_right and True (map (fun (ep : extern_state -> Prop) => (ep es)) a).

Fixpoint remove_nth {A} (n : nat) (al : list A) {struct n} : list A :=
  match n, al with
  | O, a :: al => al
  | S n', a :: al' => a :: remove_nth n' al'
  | _, nil => nil
  end.

Lemma test : forall n es,
  EXT (remove_nth n nil) es.
Proof.
  sauto.
Qed.

End ExtExtract.