The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

The behavior isn't surprising to me given what I understand of the 
reduction rules for co-inductive types. [cofix]es are only expanded when 
they are [match]ed on. The definition of [p] includes [match]ing on the 
[cofix] from the definition of [ones], but that matching can be 
simplified to reflexivity, apparently after it plays a crucial role in 
getting [p] to type-check at the type you want. There's no matching 
anywhere in the definition of [p2], so the type checker can never "look 
inside" the definition of [ones] effectively.

While this makes sense working through the reduction rules 
mechanistically, it certainly is surprisingly that normalization can 
prevent a term from being assigned a type that it was assigned before. 
It doesn't look to me like the normal form is _ill-typed_, though, just 
that it can't be assigned the type that the original had. Maybe someone 
involved with the theory and implementation of co-inductive types can 
comment on the deeper consequences of this.

Nicolas Oury wrote:
> (*if you define the type of streams of units:*)
>
> CoInductive Stream : Set :=
> | cons : Stream -> Stream.
>
> CoFixpoint ones : Stream := cons ones.
>
> (*and a function out such that out (cons xs) := cons xs *)
>
> Definition out (xs : Stream) : Stream :=
> match xs with
> | cons ys => cons ys
> end.
>
> Require Import Logic.
>
> (*Then you can prove: forall xs, xs = out xs *)
>
> Lemma out_eq (xs : Stream) : xs = out xs .
> intros xs.
> case_eq xs.
> intros s eq.
> reflexivity.
> Defined.
>
> (* This seems not to be a problem, but we can deduce *)
>
> Definition p : ones = cons ones := out_eq ones.
>
> (* Now, if we want to see how this is proved: *)
>
> Eval compute in p. (* returns refl_equal (cons (cofix ones : Stream := 
> cons ones)) *)
>
> (* but if we feed back the normal form *)
>
> Definition p2 : ones = cons ones :=
> refl_equal (cons (cofix ones : Stream := cons ones)).
>
> (* the type checker yells that ones and cons ones are not convertible *)
>
> -------------------------------
>
> It seems there is a well-typed term whose normal form is not well-typed.
> That's probably not threatening for the safety of the system, because 
> ones and cons ones are extensionaly equal.
> But it's still a bit troubling that type preservation does not hold.
>
> Am I missing something?
> Is it a known problem with coinductive types?