The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

An essential difference Hugo forgot to mention is that let (...) = ... 
in works with any inductive type with only one constructor (and not just 
with pair).

--
JH

On 10/17/2016 12:44 PM, Hugo Herbelin wrote:
> 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