The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Jason,

On Thu, Oct 13, 2016 at 06:58:19PM +0000, Jason Gross wrote:
> What's the difference between [let '(a, b) := x in y] and [let (a, b) := x 
> in
> y]?  I had in my head that the first was better, but the first results in
> typechecking failures in 8.4 and anomalies in 8.6 
> (https://coq.inria.fr/bugs/
> show_bug.cgi?id=5140), so now I'm curious what the actual differences betwen
> them are.

They follow slightly different paths for type-checking. The
former is directly interpreted as a "match" with one clause
(i.e.  [let 'pattern := t in u] is syntactic sugar for 
[match t with pattern => u end]). The latter is typed-checked
in an ad hoc way and translated to a "match" only afterwards.

A consequence is that the former case takes benefit of the more
general algorithm used in "match", as the following working
example shows:

Require Import Vector.
Import VectorNotations.
Definition hd n (v:t nat (S n)) := let 'a::_ := v in a.

As far as I understand the situation, the bug that you mention is
indirect: typing the former is demanding more from the
unification algorithm and, in #5140, this met a (actually already
fixed) bug in the type class inference algorithm.

As far as the precise example of destructing a single non nested
pair (in type "prod") is concerned, as you do, the extra power of
the "match" compilation algorithm may not be needed. So, the
second form might be as good. However, if ever some unification
of both forms had to be done, I believe that only the former
would be kept, with the latter being reduced to a particular case
of the former with an anonymous constructor (something like
re-interpreting [let (var1, ..., varn) := t in u] as
[let '(_ var1 ... varn) := t in u]).

Best,

Hugo