[Agda] Codata oddity

[Nils Anders Danielsson]

Hi,

The current implementation of codata seems to be a bit problematic.
The following program was suggested by Nicolas Oury:

  data _≡_ {a : Set} (x : a) : a -> Set where
    refl : x ≡ x

  codata Stream : Set where
    cons : Stream -> Stream

  out : Stream -> Stream
  out (cons xs) = cons xs

  out-≡ : (xs : Stream) -> xs ≡ out xs
  out-≡ (cons xs) = refl

  ω : Stream
  ω ~ cons ω

  p : ω ≡ cons ω
  p = out-≡ ω

If we evaluate p we get refl, but if we replace the right-hand side of
p with refl we get a type error, so we do not have preservation of
types.

-- 
/NAD