The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 29/04/2015 11:11, Randy Pollack wrote:
> This "answer" doesn't explain either of the observations I asked about:
>
> > Type inference is as you would expect: Γ |- t : A  /\ A =c B ----> Γ |- (t
> > :c B) : B. The :c can be just regular kernel conversion or call to a VM
> > (bytecode or native). Reduction ignores casts entirely (AFAICT).
>
> Type inference apparently causes eta-expansion of the term t, but
> Matthieu's purported type inference rule doesn't change t.

Type inference does not cause eta-expansion, per se. But type coercion 
does. Your term is somehow ill-typed, since cons has type "Type ->" 
while your cast forces it to have type "Set ->". So the pretyper 
performs an eta-expansion.

Disclaimer: I am no specialist of Coq's type system, and it might well 
be that, according to the typing rules, the term is well-typed, even 
without an eta-expansion. But the pretyper at least seems to think it 
needs to put an eta-expansion there for the term to be well-typed.

> Apparently reduction causes the cast "term constructor" to be dropped,
> at least in some cases, which is not the same as ignoring casts
> entirely.

Casts have no computational meaning, they are just meant as hints (and 
even then, the type checker tends to ignore them unless they ask for a 
specific reduction machinery, so they are basically just hints for the 
pretyper). As a consequence, they can be dropped or ignored or whatever.

> Finally, consider again the goal command
>
>     Goal (cons: forall (A:Set), A -> list A -> list A) = cons.
>
> Coq shows the goal to be
>
>      ((fun A : Set => cons (A:=A)):forall A : Set, A -> list A -> list A) =
>      (fun A : Set => cons (A:=A))
>
> Why is the RHS eta-expanded?

Because of type coercion, again. Since both sides of the equality are 
supposed to have the same type, and since the left-hand side has type 
"Set ->" (because of your explicit cast), the pretyper of Coq decides to 
coerce the right-hand side to this type using an eta-expansion.

Best regards,

Guillaume