The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 14 sept. 08 à 21:03, Robin Green a écrit :

> When the code fragment below is given to Coq (trunk version), the  
> first
> generated obligation is not provable (because it is false). Is this is
> a bug in the obligation generating code?

Nope. To check that, you can always try [Admit Obligations]. It will  
fail if any of the obligations is ill-typed (which is a good indicator  
of whether or not the VCs are wrong).

> More generally, how often should the obligation generator be  
> expected to
> generate provable obligations (assuming the overall goal is provable)?

Always, it shouldn't lose any logical information from the term. What  
happens in your case is a rather amusing interplay of type inference  
and coercions. At some point, we get to typecheck
[h : Prop, t : list Prop |- fold_left ?A ?B or t h : { x : Prop  
| ... }]. There, we know that the result of the fold must be of type [? 
A], hence we unify it with the constraint. That forces [or] to be of  
type [forall { x : Prop | ... } (x0 : Prop), { x : Prop | ... }], so  
we eta-expand [or] and you get the corresponding obligation. You can  
add an (A:=Prop) annotation to [fold_left] to avoid this problem. The  
thing is that the early unification of the result type should not have  
happened. It is an "optimisation" I've been playing with for some time  
that is only used in Program's typechecker. Among the interesting  
examples it allows to typecheck is this:

Definition rel := { A : Type & relation A }.
Definition rel_true : rel := existT _ False (λ _ _, False).
                                             ^^^^^^^^^^^^^
Error: The type of this term is a product while it is expected to be
 "?177 nat".

I think it's useful when you build any kind of dependent sum and you  
have a typing constraint.
It is insufficient to give the typing constraint with the current  
algorithm because the application
is typed without any and it is only at the end that we coerce its type  
to the one given by the context.
Clearly, when you typecheck (existT ?P False (λ _ _, False)) without  
any constraint, it's impossible
to find a most general ?P. I'll try to find a safe application area  
for this trick or disable it. Maybe some
type inference experts have a better idea though :)

-- Matthieu