Equations uses shadowed variable computing wrong result

[jakobbotsch]

From Equations Require Import Equations.
Set Equations Transparent.

Inductive term :=
| tBox
| tConstruct (ind : nat) (c : nat)
| tConst (kn : nat).

Equations eta_exp_discr (t : term) : Prop :=
eta_exp_discr (tConstruct ind c) := False;
eta_exp_discr (tConst kn) := False;
eta_exp_discr _ := True.

Inductive eta_exp_view : term -> Type :=
| eta_exp_view_Construct ind c : eta_exp_view (tConstruct ind c)
| eta_exp_view_Const kn : eta_exp_view (tConst kn)
| eta_exp_view_other t : eta_exp_discr t -> eta_exp_view t.

Equations eta_exp_viewc (t : term) : eta_exp_view t :=
eta_exp_viewc (tConstruct ind c) := eta_exp_view_Construct ind c;
eta_exp_viewc (tConst kn) := eta_exp_view_Const kn;
eta_exp_viewc t := eta_exp_view_other t _.

Definition decompose_app (t : term) : term * nat := (t, 0).

Definition inspect {A} (a : A) : { x : A | x = a } :=
  exist _ a eq_refl.

Equations eta_expand (t : term) : nat :=
eta_expand t with inspect (decompose_app t) := {
  | exist _ (t, n) _ with eta_exp_viewc t := {
    | eta_exp_view_Construct ind c := 0;
    | eta_exp_view_Const n := n;
    | eta_exp_view_other t' discr := 0
    }
  }.

Compute eta_expand (tConst 5). (* gives 0 instead of 5 *)

In this clause:

    | eta_exp_view_Const n := n;

Equations seems to instead use the n from this clause:

  | exist _ (t, n) _ with eta_exp_viewc t := {

Therefore, the computation computes to 0 instead of 5. This can also manifest as a typing error instead.

[jakobbotsch]

Much simpler example:

From Equations Require Import Equations.

Equations eta_expand : nat :=
eta_expand with 0 :=
  | n with 5 :=
    | n := n.

Compute eta_expand.

[mattam82]

Ah yes, it's missing a name clash test or a proper shadowing discipline here.

[MevenBertrand]

I got a similar issue (in version 1.3+8.14) with an example boiling down to:

From Equations Require Import Equations.

Equations test
  (n : nat) : nat :=
  test 1 := 17 ;
  test n with true := {
    | true => n
    | false => 17
  }.

Compute (test 2).

Here test 2 return 0 while it should return 2, I guess because the n got somehow shadowed.

[mattam82]

Your example is slightly different @MevenBertrand , the ones of @jakobbotsch are fixed (with an explicit error from Equations). In your case the definition should go through but there is indeed a misinterpretation.