structure EmptyM (_ : Type u) : Type v

instance : Monad EmptyM where
  pure _ := ⟨⟩
  bind _ _ := ⟨⟩

theorem runMEvil (runM : ∀α m, [Monad m] → m α → α) : False :=
  runM PEmpty EmptyM ⟨⟩ |>.elim

instance : LawfulMonad EmptyM where
  map_const := by intros; trivial
  id_map := by intros; trivial
  seqLeft_eq := by intros; trivial
  seqRight_eq := by intros; trivial
  pure_seq := by intros; trivial
  bind_pure_comp := by intros; trivial
  bind_map := by intros; trivial
  pure_bind := by intros; trivial
  bind_assoc := by intros; trivial

theorem lawfulRunMEvil (runM : ∀α m, [Monad m] → [LawfulMonad m] → m α → α)
    : False :=
  runM PEmpty EmptyM ⟨⟩ |>.elim