The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 16 Nov 2012 12:08:58 +0100,
Arnaud Spiwack 
<aspiwack AT lix.polytechnique.fr>
 a écrit :

> You've hit a tricky specificity of Coq.
> 
> Here is a fixed version of your code:
> 
> Require Import Arith.
> 
> Open Scope nat_scope.
> 
> Definition test : nat :=
>   let f x_y :=
>     let '(x, y) := x_y in
>       x + y + 2
>   in
>     f (3, 4).
> 
> It typechecks as expected. Can you spot the difference. It's subtle.
> 
> 
> 
> Still cannot see it? It's an apostrophe juste after the let.
> 
> 
> Not for the explaining: the let pattern := … in … construct has two
> forms. The historic one, let (x1,…,xn) := e in …, in this form e can
> be any type with a single constructor with n arguments. That's the
> form you used (and doesn't do what you expect). The more recent form,
> is let ' pattern := e in …, in this form you write a pattern with
> constructors, possible nesting, and as long as this pattern is
> irrefutable it typechecks (in particular it participates to type
> inference).

I was not aware of it, is it documented somewhere? Is there any reason
not to merge them?

> 
> 
> On 16 November 2012 11:24, Dominic Mulligan <
> dominic.p.mulligan AT googlemail.com>
>  wrote:
> 
> > Hi,
> >
> > We're writing an extraction tool targeting Coq theories here from a
> > DSL for hardware descriptions, and came across a surprising (to me,
> > at least --- though I don't know Coq that well) type inference
> > failure in the following Coq code:
> >
> > Require Import Arith.
> >
> > Open Scope nat_scope.
> >
> > Definition test : nat :=
> >   let f x_y :=
> >     let (x, y) := x_y in
> >       x + y + 2
> >   in
> >     f (3, 4).
> >
> > Coq (v8.4, October 2012) complains here that it cannot infer the
> > type of x_y in the let-binding.  But why?  I have given Coq
> > everything that it needs to know that x_y is of type (nat * nat)
> > here.  Can anybody explain why inference is failing, and give any
> > sort of heuristic guidance as to when type annotations are
> > necessary (short of putting them everywhere --- I had hoped to try
> > to keep them to a minimum)?
> >
> > Thanks for any help.
> >
> > Dominic
> >
> >