"Hint Rewrite" with unresolved typeclass evar anomaly

[samuelgruetter]

Version

8.6

Operating system

Linux

Description of the problem

Class Decidable (P : Prop) := dec : {P} + {~P}.
Arguments dec _%type_scope {_}.

Notation DecidableEq T := (forall (x y: T), Decidable (x = y)).

Axiom word: nat -> Type.
Axiom weq: forall (sz : nat) (x y : word sz), {x = y} + {x <> y}.

Instance dec_eq_word : forall sz, DecidableEq (word sz) := weq.

Lemma get_put: forall {var: Type} {dec_eq_var: DecidableEq var} (x y: var),
  (x = y) = if dec (x = y) then True else False.
Admitted.

Check (@get_put _ _).

Hint Rewrite (@get_put _ _) : rewrite_state_op_specs.

yields the following error on the last line:

Anomaly: Evar ?X18 was not declared. Please report at
http://coq.inria.fr/bugs/.

[JasonGross]

Also present in 8.7.0. I suspect what's happening is that when Hint Rewrite runs TC resolution to get a term out, it does not thread the evar map properly somewhere, and so when TC resolution partially refines some evars with newly created ones, bad things happen. I wonder if the anomaly comes from Hint Rewrite itself, or if it comes in trying to print the error message....

[SkySkimmer]

Fixed since 8.17