The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

> From: frank maltman 
>Â <frank.maltman AT googlemail.com>

> Sent: Monday, May 16, 2011 12:12 AM
> 
> 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!

It might be a little more comprehensible if you write it out with more 
parentheses.

You turn

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

into

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

I hope it's less surprising that (fun x => (E g))
can be rather different from (fun x => E), which is E[g/x]

Brandon