Equations does not handle implicit constructor coercions in patterns

[tperami]

trafficstars

The regular match pattern elaborator is able to insert constructor coercions in a match pattern when the type of the pattern and the discriminee are known. For example:

Inductive new_bool := old_bool (b : bool).
Coercion old_bool : bool >-> new_bool.

Definition proj_new_bool (nb : new_bool) : bool :=
  match nb with
  | true => true (* Elaborated to | old_bool true => true *)
  | false => false (* Elaborated to | old_bool false => false *)
  end.

However, Equations is not able to do that:

Fail Equations proj_new_bool_fail : new_bool -> bool :=
| true => true;
| false => false.

Equations proj_new_bool_annoying : new_bool -> bool :=
| old_bool true => true;
| old_bool false => false.

How hard would that be to fix?

[mattam82]

It should not be hard to implement as equations patterns are a subset of typeable terms. Probably we're just not passing the right typing constraint here.