constructor does not work for LawfulMonad

Stream: general

[Asei Inoue]

instance : LawfulMonad Option := by
  constructor <;> sorry

instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) := by
  /- tactic 'constructor' failed, no applicable constructor found -/
  constructor

why this error occurs?

[Asei Inoue]

and why the following code does not raise an error...?

instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) := by
  sorry

instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) := by
  constructor <;> sorry -- why this constructor does not fail???