{-# OPTIONS --cubical-compatible #-}
module Class.Monad.Instances where

open import Class.Prelude
open import Class.Functor.Core
open import Class.Applicative
open import Class.Monad.Core
open import Class.Monad.Id

instance
  Monad-TC : Monad TC
  Monad-TC = record {R}
    where import Reflection as R renaming (pure to return)

  Monad-List : Monad List
  Monad-List = λ where
    .return → _∷ []
    ._>>=_  → flip concatMap

  Monad-Maybe : Monad Maybe
  Monad-Maybe = λ where
    .return → just
    ._>>=_  → Maybe._>>=_
   where import Data.Maybe as Maybe

  MonadLaws-Maybe : MonadLaws Maybe
  MonadLaws-Maybe = λ where
    .>>=-identityˡ → refl
    .>>=-identityʳ → λ where
      (just _) → refl
      nothing  → refl
    .>>=-assoc → λ where
      (just _) → refl
      nothing  → refl