The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/28/2013 09:33 AM, Jonas Oberhauser wrote:
> exact (fix l k := fix r n := match k as k, n as n return P k n with
>                              | 0, 0 => base
>                              | _, S n => stepr k n (r n)
>                              | S k, _ => stepl k n (l k)
>                              end).
>
> However, r has type forall n, P k n - and not forall n, P 0 n; even 
> though at that point in the match we know that k is 0.

To understand what is going on here, I suggest Section 8.2, "The One 
Rule of Dependent Pattern Matching in Coq," in CPDT 
<http://adam.chlipala.net/cpdt/>.  In particular, you seem to be 
assuming that [match] will refine the types of arbitrary variables 
(e.g., [r]) based on which patterns match, but it never does so.

You're mentioning [k] in some cases, and [k] itself is not refined with 
a known equality to a new value (e.g., [S] of something).  In other 
words, in the second pattern rule, the mentions of [k] and [r] are both 
referring to "the old [k]," while the [match] typing rule wants the 
overall expression to have a type in terms of "the refined [k]."

Your approach to fixing the problem seems reasonable to me.  CPDT 
introduces other design patterns for getting dependent [match]es to 
refine types in useful ways.

P.S.: It is always redundant to write [x as x] as you do above for your 
[match] discriminees.