Demonstration of the importance of "tight" co-inductive definitions

EffUnguarded.v

Section Eff.
  Variable eff : Type -> Type.

  CoInductive Eff (T : Type) : Type :=
  | ret (_ : T)
  | interact {A : Type} (_ : eff A) (_ : A -> Eff T)
  | delay (_ : Eff T).
  Arguments ret {_} _.
  Arguments interact {_ _} _.
  Arguments delay {_} _.

  Section tight.
    Context {A B : Type} (k : A -> Eff B).

    CoFixpoint bind_tight (f : Eff A) : Eff B :=
      match f with
      | ret x => delay (k x)
      | interact io k' => interact io (fun x => bind_tight (k' x))
      | delay f => delay (bind_tight f)
      end.
  End tight.


  Section loose.

    CoFixpoint bind_loose {A B : Type} (k : A -> Eff B) (f : Eff A) : Eff B :=
      match f with
      | ret x => delay (k x)
      | interact io k' => interact io (fun x => bind_loose k (k' x))
      | delay f => delay (bind_loose k f)
      end.
  End loose.

End Eff.

Arguments bind_tight {_ _ _} _ _.
Arguments bind_loose {_ _ _} _ _.
Arguments interact {_ _ _} _ _.
Arguments ret {_ _} _.
Arguments delay {_ _} _.

Section interp.

  Context {eff eff' : Type -> Type}.

  Variable do : forall {T}, eff T -> Eff eff' T.

  (* Definition fails with the "loose" implementation of `bind` *)
  Fail CoFixpoint interp {T} (c : Eff eff T) : Eff eff' T :=
    match c with
    | ret x => ret x
    | interact e k =>
      bind_loose (fun x => interp (k x)) (do _ e)
    | delay x => delay (interp x)
    end.

  (* Same definition succeeds with the "tight" implementation of `bind` *)
  CoFixpoint interp {T} (c : Eff eff T) : Eff eff' T :=
    match c with
    | ret x => ret x
    | interact e k =>
      bind_tight (fun x => interp (k x)) (do _ e)
    | delay x => delay (interp x)
    end.

End interp.