WErrorOverride.agda

module WErrorOverride where

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}

infixl 1 _>>=_

postulate
  return : {A : Set} → A → IO A
  _>>=_  : {A : Set} {B : Set} → IO A → (A → IO B) → IO B

{-# COMPILED return (\_ -> return)    #-}
{-# COMPILED _>>=_  (\_ _ -> (>>=)) #-}

------------------------------------------------------------------------

-- An error should be raised if one tries to do something like this:

data PartialBool : Set where
  true : PartialBool

{-# COMPILED_DATA PartialBool Bool True #-}

-- However one can override such behaviour by passing the flag
-- --ghc-flag=-Wwarn to Agda upon compilation.

main = return true