The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hello Frank,

Le 16 mai 2011 à 07:12, frank maltman a écrit :

> 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."
<snip/>

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

This application of (fun i => ...) to (index xs) is ill-typed, the first 
parenthesis
should be around the match. Indeed the error message is not the one you 
expect due to heuristics in the type-checking of pattern-matching.

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