Instance search does not play nicely with monad transformers defined by composition

[jespercockx]

trafficstars

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.

[jespercockx]

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

[MatthewDaggitt]

Blocked by #939

[gallais]

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.?

[Taneb]

Effect.Monad.Reader.Transformer is my instinct

[gallais]

What about Data.Maybe.Effectful? Data.Maybe.Effectful.Transformer too?

[gallais]

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 :(

[gallais]

I now have a test case in #1841 Next step is to actually rely on instance search to fill in the proofs.