Restore 'return' as an alias for 'pure'

CHANGELOG.md

@@ -774,8 +774,7 @@ Non-backwards compatible changes
   This is needed for level-increasing functors like `IO : Set l → Set (suc l)`.
 
 * `RawApplicative` is now `RawFunctor + pure + _<*>_` and `RawMonad` is now
-  `RawApplicative` + `_>>=_` and so `return` is not used anywhere anymore.
-  This fixes the conflict with `case_return_of` (#356)
+  `RawApplicative` + `_>>=_`.
   This reorganisation means in particular that the functor/applicative of a monad
   are not computed using `_>>=_`. This may break proofs.
 

src/Effect/Applicative.agda

@@ -53,6 +53,10 @@ record RawApplicative (F : Set f → Set g) : Set (suc f ⊔ g) where
   zip : F A → F B → F (A × B)
   zip = zipWith _,_
 
+  -- Haskell-style alternative name for pure
+  return : A → F A
+  return = pure
+
   -- backwards compatibility: unicode variants
   _⊛_ : F (A → B) → F A → F B
   _⊛_ = _<*>_

src/IO/Primitive.agda

@@ -10,20 +10,29 @@
 
 module IO.Primitive where
 
-open import Agda.Builtin.IO
+open import Level using (Level)
+private
+  variable
+    a : Level
+    A B : Set a
 
 ------------------------------------------------------------------------
 -- The IO monad
 
-open import Agda.Builtin.IO public using (IO)
+open import Agda.Builtin.IO public
+  using (IO)
 
 infixl 1 _>>=_
 
 postulate
-  pure : ∀ {a} {A : Set a} → A → IO A
-  _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
+  pure : A → IO A
+  _>>=_  : IO A → (A → IO B) → IO B
 
 {-# COMPILE GHC pure = \_ _ -> return    #-}
 {-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
 {-# COMPILE UHC pure = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
 {-# COMPILE UHC _>>=_  = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
+
+-- Haskell-style alternative syntax
+return : A → IO A
+return = pure