<$>, <&>, $>, void, and =<< are not class methods

lib/Haskell/Prim/Functor.agda

@@ -13,39 +13,38 @@ open import Haskell.Prim.Tuple
 
 -- ** base
 record Functor (f : Set → Set) : Set₁ where
-  infixl 1 _<&>_
-  infixl 4 _<$>_ _<$_ _$>_
+  infixl 4 _<$_
   field
     fmap : (a → b) → f a → f b
-    _<$>_ : (a → b) → f a → f b
-    _<&>_ : f a → (a → b) → f b
     _<$_ : (@0 {{ b }} → a) → f b → f a
-    _$>_ : f a → (@0 {{ a }} → b) → f b
-    void : f a → f ⊤
 -- ** defaults
 record DefaultFunctor (f : Set → Set) : Set₁ where
   field fmap : (a → b) → f a → f b
 
-  infixl 1 _<&>_
-  infixl 4 _<$>_ _<$_ _$>_
-
-  _<$>_ : (a → b) → f a → f b
-  _<$>_ = fmap
-
-  _<&>_ : f a → (a → b) → f b
-  m <&> f = fmap f m
+  infixl 4 _<$_
 
   _<$_ : (@0 {{ b }} → a) → f b → f a
   x <$ m = fmap (λ b → x {{b}}) m
 
-  _$>_ : f a → (@0 {{ a }} → b) → f b
-  m $> x = x <$ m
-
-  void : f a → f ⊤
-  void = tt <$_
 -- ** export
 open Functor ⦃...⦄ public
 {-# COMPILE AGDA2HS Functor existing-class #-}
+
+_<$>_ : {{Functor f}} → (a → b) → f a → f b
+_<$>_ = fmap
+
+_<&>_ : {{Functor f}} → f a → (a → b) → f b
+m <&> f = fmap f m
+
+_$>_ : {{Functor f}} → f a → (@0 {{ a }} → b) → f b
+m $> x = x <$ m
+
+void : {{Functor f}} → f a → f ⊤
+void = tt <$_
+
+infixl 1 _<&>_
+infixl 4 _<$>_ _$>_
+
 -- ** instances
 private
   mkFunctor : DefaultFunctor t → Functor t

lib/Haskell/Prim/Monad.agda

@@ -25,7 +25,6 @@ module Do where
       overlap ⦃ super ⦄ : Applicative m
       return : a → m a
       _>>_ : m a → (@0 {{ a }} → m b) → m b
-      _=<<_ : (a → m b) → m a → m b
   -- ** defaults
   record DefaultMonad (m : Set → Set) : Set₁ where
     field
@@ -37,8 +36,6 @@ module Do where
     _>>_ : m a → (@0 {{ a }} → m b) → m b
     m >> m₁ = m >>= λ x → m₁ {{x}}
 
-    _=<<_ : (a → m b) → m a → m b
-    _=<<_ = flip _>>=_
   -- ** export
   open Monad ⦃...⦄ public
   {-# COMPILE AGDA2HS Monad existing-class #-}
@@ -57,6 +54,9 @@ module Dont where
 
 open Do public
 
+_=<<_ : {{Monad m}} → (a → m b) → m a → m b
+_=<<_ = flip _>>=_
+
 mapM₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → (a → m b) → t a → m ⊤
 mapM₋ f = foldr (λ x k → f x >> k) (pure tt)