Anomaly when inferring simple typeclass instance.

[arthuraa]

Description of the problem

From Coq Require Import ssreflect.
From stdpp Require Import base gmap.
Goal False.
have: Inhabited (gmap nat nat) by [].
(* Toplevel input, characters 0-37: *)
(* > have: Inhabited (gmap nat nat) by []. *)
(* > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
(* Error: *)
(* Anomaly *)
(* "tclZERO receiving critical error: Anomaly "Not an arity." Please report at http://coq.inria.fr/bugs/." *)
(* Please report at http://coq.inria.fr/bugs/. *)

Strangely, swapping the two import lines makes the anomaly go away (though typeclass inference still fails to find the empty_inhabited instance.)

Coq Version

8.12

[CohenCyril]

Ssreflect have does not perform typeclass inference, you may add a ltac in term refine to compensate. (see below)
I remember @gares had some ideas of how to integrate ssreflct have with typeclass inference more smoothly, meanwhile he already gave me the following trick:

• doc: https://github.com/math-comp/analysis/blob/9e270bd65004afc740da4fd805a7f06b3e0de075/theories/posnum.v#L10-L13
• implem: https://github.com/math-comp/analysis/blob/9e270bd65004afc740da4fd805a7f06b3e0de075/theories/posnum.v#L45-L46

[arthuraa]

@CohenCyril Great to know about the refine trick!

[gares]

I don't understand my trick 🤣
Is have : T := !! _. the thing?

[SkySkimmer]

Anomaly probably from around

coq/plugins/ssr/ssrview.ml

Lines 204 to 209 in 1c919ed

	with e ->
	(* XXX this is another catch all! *)
	let e, info = Exninfo.capture e in
	Ssrprinters.ppdebug (lazy
	Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
	tclZERO ~info e

[gares]

Well spot. But this is about the "external anomaly". There is still the internal one (there are 2 anomalies in the error message)

[SkySkimmer]

Actually the bad tclZERO looks like this one instead

coq/plugins/ltac/rewrite.ml

Lines 2147 to 2150 in 1c919ed

	with e ->
	(* XXX what is the right test here as to whether e can be converted ? *)
	let e, info = Exninfo.capture e in
	Proofview.tclZERO ~info e

[SkySkimmer]

Similar anomaly, no ssr:

From stdpp Require Import base gmap.
Goal Inhabited (gmap nat nat).
  reflexivity.

[SkySkimmer]

Much reduced version:

#[universes(template)]
Inductive R (x:nat) (A:Type) : Type := C : A -> R x A.

#[universes(template)]
Inductive Box (A:Type) : Type := box : A -> Box A.

Goal Box (R 0 Set).
  reflexivity.