module bug-in-record where

open import Data.Maybe     using (Maybe; just; nothing)
open import Data.List      using (List; []; [_]; _++_)
open import Data.Nat       using (ℕ)

-- this record definition does not work
record MyMonadPlus m : Set₁ where
   field mzero : {a : Set} → m a → List a
         mplus : {a : Set} → m a → m a → List a
--Emacs error: and the 10th line is the above line
--/home/j/dev/apps/haskell/agda/learn/bug-in-record.agda:10,36-39
--Set != Set₁
--when checking that the expression m a has type Set₁

-- if the above record definition is changed to the below, it works
--record MyMonadPlus (m : Set → Set) : Set₁ where
--   field mzero : {a : Set} → m a → List a
--         mplus : {a : Set} → m a → m a → List a

mymaybemzero : {a : Set} → Maybe a → List a
mymaybemzero nothing = []
mymaybemzero (just x) = [ x ]

mymaybemplus : {a : Set} → Maybe a → Maybe a → List a
mymaybemplus x y = (mymaybemzero x) ++ (mymaybemzero y)

mymaybeMonadPlus : MyMonadPlus Maybe
mymaybeMonadPlus = record { mzero = mymaybemzero
                           ; mplus = mymaybemplus }

open MyMonadPlus mymaybeMonadPlus

testmplus : Maybe ℕ → Maybe ℕ → List ℕ
testmplus x y = mplus x y