Require Import
  abstract_algebra universal_algebra interfaces.monads canonical_names.

Section contents.

  Context (operation: Set) (operation_type: operation OpType unit).

  Let sign := Build_Signature unit operation operation_type.

  Definition M (T: Type): Type := Term sign T ( tt).

  Section equality.

    Context {A: Type} `{Setoid A}.

    Fixpoint geneq {s s'} (x: Term sign A s) (y: Term sign A s'): Prop :=
      match x, y with
      | Var v _, Var w _ => v = w
      | App _ z t t', App _ z' t'' t''' => geneq t t'' geneq t' t'''
      | Op o, Op o' => o o'
      | _, _ => False

    Lemma geneq_sym s (x: Term sign A s): s' (y: Term sign A s'), geneq x y geneq y x.

    Lemma geneq_trans s (x: Term sign A s): s' (y: Term sign A s') s'' (z: Term sign A s''),
      geneq x y geneq y z geneq x z.

    Global Instance Me: Equiv (M A) := geneq.

    Instance: Symmetric Me.

    Instance: Transitive Me.

    Instance: Reflexive Me.

    Global Instance: Setoid (M A).
  End equality.

  Definition gen_bind {A B: Type} (f: A M B): {s}, Term sign A s Term sign B s
    := fix F {s} (t: Term sign A s): Term sign B s :=
      match t with
      | Var v tt => f v
      | App o z x y => App _ _ _ z (F x) (F y)
      | Op o => Op _ _ o

  Implicit Arguments gen_bind [[A] [B] [s]].

  Instance: MonadBind M := λ _ _ z f, gen_bind f z.

  Instance: `{Equiv A} `{Equiv B},
    Proper ((=) ==> ((=) ==> (=)) ==> (=)) (@bind M _ A B).

  Instance: MonadReturn M := λ _ x, Var sign _ x tt.

  Instance: `{Equiv A}, Proper ((=) ==> (=)) (@ret M _ A).

  Instance: Monad M.

End contents.