The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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).

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