{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Prelude.Monad.Fail
-- Copyright   :  (C) 2019 Ryan Scott
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Ryan Scott
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Defines the promoted and singled versions of the 'MonadFail' type class.
--
----------------------------------------------------------------------------

module Data.Singletons.Prelude.Monad.Fail (
  PMonadFail(..), SMonadFail(..),

  -- * Defunctionalization symbols
  FailSym0, FailSym1
  ) where

import Data.Singletons.Prelude.Instances
import Data.Singletons.Prelude.Monad.Internal
import Data.Singletons.Single

$(singletonsOnly [d|
  -- -| When a value is bound in @do@-notation, the pattern on the left
  -- hand side of @<-@ might not match. In this case, this class
  -- provides a function to recover.
  --
  -- A 'Monad' without a 'MonadFail' instance may only be used in conjunction
  -- with pattern that always match, such as newtypes, tuples, data types with
  -- only a single data constructor, and irrefutable patterns (@~pat@).
  --
  -- Instances of 'MonadFail' should satisfy the following law: @fail s@ should
  -- be a left zero for 'Control.Monad.>>=',
  --
  -- @
  -- fail s >>= f  =  fail s
  -- @
  --
  -- If your 'Monad' is also 'Control.Monad.MonadPlus', a popular definition is
  --
  -- @
  -- fail _ = mzero
  -- @
  class Monad m => MonadFail m where
      fail :: String -> m a

  instance MonadFail Maybe where
      fail _ = Nothing

  instance MonadFail [] where
      fail _ = []
  |])