agda-stdlib
agda-stdlib copied to clipboard
Instance search does not play nicely with monad transformers defined by composition
Here is a small example that currently fails:
open import Data.Maybe.Base public using (Maybe; nothing; just)
open import Data.Unit public using (⊤; tt)
open import Reflection.Term public
open import Reflection.TypeChecking.Monad public using (TC; inferType)
open import Category.Monad public using () renaming ( RawMonad to Monad )
open Monad {{...}} public using (return; _>>=_)
open import Data.Maybe.Instances public
open import Reflection.TypeChecking.Monad.Instances public
goalErr : Term → TC ⊤
goalErr goal = inferType goal >>= λ goalType → return _
The relevant part of the error message is the following:
Failed to solve the following constraints:
Resolve instance argument _r_5 : Monad _M_4
Candidates
tcMonad : {ℓ : Agda.Primitive.Level} → Monad TC
maybeMonadT :
{ℓ : Agda.Primitive.Level} {M : ⊤ → ⊤ → Set ℓ → Set ℓ}
⦃ inst : Category.Monad.Indexed.RawIMonad M ⦄ →
Category.Monad.Indexed.RawIMonad
(λ _ _ → M tt tt Function.Base.∘′ Maybe)
(stuck)
As you can see, Agda fails to rule out that TC = M tt tt Function.Base.∘′ Maybe
for some monad M
, which causes instance search to fail. (It does work with --overlapping-instances
but I'd rather avoid using that for performance reasons.) The general lesson here is that instances should target named data or record types, not types defined using some function. Either the instance for maybeMonadT
should be removed, or else MaybeT
should be wrapped in a record type.
For reference, here's the current definition of monadT
for Maybe
:
------------------------------------------------------------------------
-- Maybe monad transformer
monadT : ∀ {f} → RawMonadT {f} (_∘′ Maybe)
monadT M = record
{ return = M.return ∘ just
; _>>=_ = λ m f → m M.>>= maybe f (M.return nothing)
}
where module M = RawMonad M
Blocked by #939
I wonder where we should put these transformers.
In the #1841 overhaul I ended up having submodules ReaderT
& Reader
in
Effect.Monad.Reader
because both define functor
, applicative
, etc.
As a consequence everything is behind a double open
which is probably not the
most convenient.
I wonder whether it'd be better to have them in different modules.
For instance Effect.Monad.Reader.MonadTrans
& Effect.Monad.Reader.Monad
.
The question then being what to do with Data.Maybe.Effectful
. A similar split?
Actually move that content to Effect.Monad.
?
Effect.Monad.Reader.Transformer
is my instinct
What about Data.Maybe.Effectful
? Data.Maybe.Effectful.Transformer
too?
We currently have
record RawIMonadState {I : Set i} (S : I → Set f)
(M : IFun I f) : Set (i ⊔ suc f) where
field
monad : RawIMonad M
get : ∀ {i} → M i i (S i)
put : ∀ {i j} → S j → M i j (Lift f ⊤)
open RawIMonad monad public
modify : ∀ {i j} → (S i → S j) → M i j (Lift f ⊤)
modify f = get >>= put ∘ f
but to use these in mtl style would mean e.g. having
my_program : {{RawMonadState S M}} -> {{RawMonadReader R M}} -> (...)
which means 2 separate, potentially conflicting, instances of RawMonad
.
Should we remove these RawMonad
fields? In which case we can't implement modify
as a
record-definition :(
I now have a test case in #1841 Next step is to actually rely on instance search to fill in the proofs.