Anomaly: "grounding a non evar-free term" only when using Alectryon

[tchajed]

This example results in an anomaly "grounding a non evar-free term" due to the refine tactic only when run through Alectryon. It has something to do with the evar in the decoder's match: 0 => _.

Class Countable T :=
  inj_countable {
      encode: T -> nat;
      decode: nat -> T;
      encode_decode_ok : forall x, decode (encode x) = x;
    }.

Inductive bin_op :=
  | PlusOp.

Global Instance bin_op_countable : Countable bin_op.
Proof.
  refine (inj_countable bin_op
            (fun op => match op with | PlusOp => 0  end)
            (fun n => match n with | 0 => _ | _ => PlusOp end) _).
  destruct x; auto.
Qed.

[cpitclaudel]

Which version of Coq and SerAPI are you on? I'm on 8.10 and not seeing that issue

[tchajed]

This is Coq 8.12.2 and coq-serapi 8.13.0+0.12.0.

[cpitclaudel]

OK, reproduced with 8.12.0+0.12.0. Bug report here: https://github.com/ejgallego/coq-serapi/issues/228

[cpitclaudel]

Fixed upstream.