The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Sun, 15 May 2011 09:43:04 -0400
Adam Chlipala 
<adam AT chlipala.net>
 wrote:

> I just want to make sure you're aware that all of these definitions 
> (including the one you're struggling with) also appear in "Certified 
> Programming with Dependent Types."

I've just applied the techniques given in the 'Dependent Data Structures'
chapter and have come across something rather nasty.

This:

Fixpoint index {A : Type} {b : nat} (v : vector A b) : F.finite b -> A :=
  match v with
    | VZ =>
      fun i =>
        match i in (F.finite b') return (match b' with | 0 => A | S _ => unit 
end) with
          | F.FO _   => tt
          | F.FS _ _ => tt
        end
    | VC _ x xs =>
      fun i =>
        match i in (F.finite b') return ((F.finite (pred b') -> A) -> A) with
          | F.FO _    => fun _      => x
          | F.FS _ f' => fun index' => index' f'
        end (index xs)
  end.

... typechecks.

This:

Fixpoint index {A : Type} {b : nat} (v : vector A b) : F.finite b -> A :=
  match v with
    | VZ =>
      (fun i =>
        match i in (F.finite b') return (match b' with | 0 => A | S _ => unit 
end) with
          | F.FO _   => tt
          | F.FS _ _ => tt
        end)
    | VC _ x xs =>
      (fun i =>
        match i in (F.finite b') return ((F.finite (pred b') -> A) -> A) with
          | F.FO _    => fun _      => x
          | F.FS _ f' => fun index' => index' f'
        end) (index xs)
  end.

Gives the following incomprehensible error:

Error:
In environment
index : forall (A : Type) (b : nat), vector A b -> F.finite b -> A
A : Type
b : nat
v : vector A b
i : F.finite ?41
The term
 "match
    i in (F.finite b') return match b' with
                              | 0 => A
                              | S _ => unit
                              end
  with
  | F.FO _ => tt
  | F.FS _ _ => tt
  end" has type "match ?41 with
                 | 0 => A
                 | S _ => unit
                 end" while it is expected to have type 
"A".

I assume this is down to the various heuristics used to infer types?

I'm at a bit of a loss as to how the addition of a pair of parentheses
could do so much damage!