Multiplicity of implicit type arguments in interfaces

Question

I have the following state monad in Idris 2:

record State (s : Type) (a : Type) where
  constructor MkState
  run : s -> (s, a)

and I'm trying to define something similar to an Eq interface:

infix 0 ~~
interface EqM (m : Type -> Type) where
  (~~) : {a : Type} -> m a -> m a -> Type

but when I go to implement it:

implementation EqM (State s) where
  MkState s1 ~~ MkState s2 = ?

I get the following error:

Error: While processing right hand side of EqM implementation at Monads:23:1--24:51. s is not accessible in this context.

Monads:23:1--24:51
 23 | implementation EqM (State s) where
 24 |   MkState s1 ~~ MkState s2 = ?

I'm guessing the state type s is implicitly given a 0 multiplicity. Is there some way around this, maybe writing out the multiplicity explicitly so that I'm able to implement EqM?

Answer 1

I was able to do this by explicitly quantifying over s:

record State (s : Type) (a : Type) where
  constructor MkState
  run : s -> (s, a)
  
infix 0 ~~
interface EqM (m : Type -> Type) where
  (~~) : {a : Type} -> m a -> m a -> Type

implementation {s : Type} -> EqM (State s) where
  MkState s1 ~~ MkState s2 = (x : s) -> (s1 x) = (s2 x)

Warning: I haven't tested this for usability at all. But I'm able to at least define the instance.

Edit: When I try to use this, I get a weird error that don't think is related:

implementation Monad (State s) where
  (MkState rx) >>= g = MkState (\a => let (a, x) = rx a in let (MkState ry) = g x in ry a)
  
  
lawfulMonad : (m : Type -> Type) -> EqM m => Monad m => Type
lawfulMonad m = {a : Type} -> (x : m a) -> (x >>= pure) ~~ x

stateLawful : {s : Type} -> lawfulMonad (State s)
stateLawful (MkState sem) = ?rhs

"Main.rhs" [P]
 `--           s : Type
               a : Type
             sem : s -> (s, a)
     ------------------------------------------------------------------------------------
      "Main.rhs" : (x : s) -> let (a, x) = sem x in let MkState ry = g x in ry a = sem x

I'm not sure why the name g seems to leak into the goal here, rather than pure being applied. Maybe it's an idris2 bug, but I'm not certain.

Edit 2: It turns out that this is just shadowing: it was trying to turn pure into an implicitly-quantified type. (Why it didn't show up in the context is still a mystery to me, but there you go.) Using explicit dot-notation, I was able to prove things without much difficulty.

lawfulMonad : (m : Type -> Type) -> EqM m => Monad m => Type
lawfulMonad m = {a : Type} -> (x : m a) -> (x >>= Prelude.Interfaces.pure) ~~ x

stateLawful' : {s : Type} -> (x : State s a) -> (st : s) -> ((x >>= Prelude.Interfaces.pure).run st) = x.run st
stateLawful' (MkState run) st with (run st)
  stateLawful' (MkState run) st | (s', x) = Refl

stateLawful : {s : Type} -> lawfulMonad (State s)
stateLawful (MkState run) = stateLawful' (MkState run)

interface EqM m => Monad m => LawfulMonad (m : Type -> Type) where
  triangle1 : {a : Type} -> (x : m a) -> (x >>= Prelude.Interfaces.pure) ~~ x

implementation {s : Type} -> LawfulMonad (State s) where
  triangle1 (MkState run) = stateLawful' (MkState run)

Answer 2

You want

infix 0 ~~
interface EqM (0 m : Type -> Type) where
  (~~) : {a : Type} -> m a -> m a -> Type

Otherwise you're saying that m should be available at runtime for the interface's methods.