Why can't coq infer the that 0+n=n in this dependently typed program?

Question

I'm starting to use Coq and I'd like to define some dependently typed programs. Consider the following:

Inductive natlist : nat -> Type :=
  | natnil : natlist 0
  | natcons : forall k, nat -> natlist k -> natlist (S k).

Fixpoint natappend (n:nat) (l1: natlist n) (m:nat) (l2: natlist m) : natlist (n+m) :=
  match l1 with
    | natnil => l2
    | natcons _ x rest => natcons (n+m) x (natappend rest l2)
  end.

So natlist k would be a list of nats of length k. The problem with the definition of concatenation as natappend is the following error:

Error:
In environment
natappend : forall n : nat,
            natlist n ->
            forall m : nat,
            natlist m -> natlist (n + m)
n : nat
l1 : natlist n
m : nat
l2 : natlist m
The term "l2" has type "natlist m"
while it is expected to have type
 "natlist (?n@{n1:=0} + m)".

As you can see it has a problem with the clause:

| natnil => l2

because it claims that the type of l2 is natlist m while the result type must be natlist (n+m) = natlist (0+m).

I know that Coq cannot resolve arbitrary expressions at the type level to avoid non-terminating computations, but I find strange that even this simple case isn't handled.

I'm running CoqIDE on linux, the version is:

The Coq Proof Assistant, version 8.5 (February 2016)
  compiled on Feb 22 2016 18:19:5 with OCaml 4.02.2

I've seen live classes using the MacOSX version with code similar to the above that compiled in the IDE without that error, so I'm a bit puzzled.

Is there some setting that I have to set to enable more type inference and allow the kind of code as above? Alternatively: how can I write dependently typed code that doesn't rely on type inference?

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2016-03-14T15:36:55

The problem is that you had a type error in your second branch. Here is a version that works:

Fixpoint natappend {n m:nat} (l1 : natlist n) (l2 : natlist m) : natlist (n + m) :=
  match l1 with
  | natnil => l2
  | natcons n' x rest => natcons (n' + m) x (natappend rest l2)
  end.

The crucial difference between this version and the original one is the parameter passed to natcons: here, it is n' + m, whereas before it was n + m.

This example illustrates very well a general issue with non-locality of error messages in Coq, in particular when writing dependently typed programs. Even though Coq complained about the first branch, the problem was actually in the second branch. Adding annotations in your match statement, as suggested by @jbapple, can be useful when trying to diagnose what is going wrong.

Why can't coq infer the that 0+n=n in this dependently typed program?

2 Answers