------------------------------------------------------------------------
-- This approach is incorrect, but perhaps subtly so
------------------------------------------------------------------------

-- Note that in an inductive setting, where all expressions were
-- finite, this semantics (correspondingly modified) would be OK.
-- Hence it may be easy to mistakenly assume that this semantics is
-- also OK; at least I initially did so.

module Deterministic.Incorrect where

open import Data.Colist
open import Coinduction

open import Deterministic.Expr

infix 4 _HasTrace_

data _HasTrace_ : Semantics where
  nop  :  {e   ms} (s :  ( e HasTrace   ms))  nop    e HasTrace     ms
  tick :  {e m ms} (s :  ( e HasTrace  ms))  tick m e HasTrace m  ms

------------------------------------------------------------------------
-- Examples

possible : nops HasTrace []
possible = nop ( possible)

-- Should not be allowed, since nops does not emit any messages:

should-be-impossible :  {m ms}  nops HasTrace (m  ms)
should-be-impossible = nop ( should-be-impossible)

ok : ticks HasTrace scissors
ok = tick ( ok)