Breaking subject reduction in Coq, and not breaking it in Agda (any more)

CoTest.agda

-- More information:
-- http://coq-club.inria.narkive.com/3zS9pwcc/coinductive-types-and-type-preservation
-- https://lists.chalmers.se/pipermail/agda/2008/000383.html

module CoTest where

open import Prelude public

{-

CoInductive tick := Tick : tick -> tick.

CoFixpoint loop := Tick loop.

Definition etaeq : loop = loop :=
  match loop with | Tick t => eq_refl (Tick t) end.

Definition BOOM :=
  Eval compute in (etaeq : loop = loop).

-}

record tick : Set where
  constructor Tick
  coinductive
  field
    τ : tick
open tick public

loop : tick
τ loop = loop

etaeq : loop ≡ loop
etaeq = refl

test : (l : tick) → l ≡ l
test l = {!refl {A = Tick (τ l)}!}