The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

However, Coq's implementation (if no bugs) should be weakly normalizing,
which is usually enough for consistency.

I thought that for consistency we also need type preservation (along with strong/weak normalization). 

Coq seems to not have type preservation, as shown in the last 2 slides (25 and 26) of 

https://coq.inria.fr/files/coq5-slides-sacchini.pdf

I just reproduced the above described problem using Coq 8.5:

Set Implicit Arguments.

CoInductive Inf :=

S : Inf -> Inf.

CoFixpoint infinity : Inf :=S ( infinity).

(** This innocuous looking function 

    actually causes an unfolding of cofix *)

Definition unfold (x : Inf) : Inf :=

match x with

| S y => S y

end.

Definition unfoldEq (x:Inf) : x = unfold x.

Proof.

  intros.

  destruct x as [x'].

  simpl. exact eq_refl.

Defined.

(** We make a dummy goal to use the "type of" function *)

Goal False.

(** [unfoldEq infinity] is of type [infinity = S infinity] *)

match type of (unfoldEq infinity) with

| ?T => let T' := eval simpl in T in idtac T "," T'

end.

(**

    when we compute on [eqq infinity] as shown above, we

    get [eq_refl] which cannot be of the type

    [infinity = S infinity] because [S infinity] is not definitionally equal to [infinity]. *)

Eval compute in (unfoldEq infinity).

(** This is  a voilation of type preservation*)