    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- This module is DEPRECATED. Please use the builtin Maybe instead.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible #-}

    module Foreign.Haskell.Maybe where

    open import Level using (Level; _⊔_)
    open import Data.Maybe.Base as Data using (just; nothing)

    private
      variable
        a : Level
        A : Set a

    ------------------------------------------------------------------------
    -- Definition

    data Maybe (A : Set a) : Set a where
      just    : A → Maybe A
      nothing : Maybe A

    {-# FOREIGN GHC type AgdaMaybe l a = Maybe a #-}
    {-# COMPILE GHC Maybe = data AgdaMaybe (Just | Nothing) #-}

    ------------------------------------------------------------------------
    -- Conversion

    toForeign : Data.Maybe A → Maybe A
    toForeign (just x) = just x
    toForeign nothing = nothing

    fromForeign : Maybe A → Data.Maybe A
    fromForeign (just x) = just x
    fromForeign nothing = nothing

    {-# WARNING_ON_IMPORT
    "Warning: Foreign.Haskell.Maybe was deprecated in v1.4.
    Maybe is now an Agda builtin and does not need library support."
    #-}

    {-# WARNING_ON_USAGE Maybe
    "Warning: Foreign.Haskell.Maybe's Maybe was deprecated in v1.4.
    Maybe is now an Agda builtin and does not need library support."
    #-}

    {-# WARNING_ON_USAGE toForeign
    "Warning: toForeign was deprecated in v1.4.
    Maybe is now an Agda builtin and does not need library support."
    #-}

    {-# WARNING_ON_USAGE fromForeign
    "Warning: fromForeign was deprecated in v1.4.
    Maybe is now an Agda builtin and does not need library support."
    #-}