The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 07/09/2016 11:23, Soegtrop, Michael wrote:

> Can’t one add a rule which reduces matches in the following situation:
> 
> -          the match has only one pattern
> -          the result term does not depend on any pattern bindings
> -          the type of the result term and the type of the match unify
> (should always be the case – otherwise the match wouldn’t type check)

This is not always the case. In fact, it is almost never the case, since
people are using "match" precisely because the types do not unify.

For instance, you certainly don't want the following well-typed term

Definition foo (H : (bool -> bool) = bool) :=
  match H in (_ = t) return t -> _ with
  | eq_refl => fun f => f false
  end true.

to reduce to the following ill-typed term

Definition foo (H : (bool -> bool) = bool) :=
  true false.

I may be misunderstanding what you propose.

Best regards,

Guillaume