Variable associated types / data types in Haskell

Question

I'm currently trying to overload MonadTransformer extraction functions. My current attempt was to place the inner-monad m as an instance of an associated type Result:

class ( Monad Result
      , MonadTrans m
      , MonadReader prefix m
      , ) => FooReader prefix m where
  type Result
  runFooReader :: forall b. m b -> prefix -> Result b

instance Monad m => FooReader prefix (ReaderT prefix m)
  type Result = m -- This is there the error is thrown
  runFooReader = runReaderT

The only reason why Foo is shaped funny is due to the MonadTrans and MonadReader restrictions. Basically, this is forcing all associated type instances to be monomorphic types (correct?).

I then thought to redesign it, to make Result simply a polymorphic vairable:

...
class FooReader prefix m where
  runFooReader :: forall b result. m b -> prefix -> result b

... but then in the instances, the types result and w (if it's ReaderT prefix w as m, for instance) will not unify. Is there any way to make this result varialbe / idea polymorphic, yet decidable?

Answer 1

Cleaning up the syntax errors and adding a kind annotation to Result, we get this:

class ( Monad Result
      , MonadTrans m
      , MonadReader prefix m
      ) => FooReader prefix m where
  type Result :: * -> *
  runFooReader :: forall b. m b -> prefix -> Result b

instance Monad m => FooReader prefix (ReaderT prefix m) where
  type Result = m -- Again, error triggered here
  runFooReader = runReaderT

And a more interesting error:

The RHS of an associated type declaration mentions type variable `m'
  All such variables must be bound on the LHS

This is expanded in the GHC docs:

The visibility of class parameters in the right-hand side of associated family instances depends solely on the parameters of the family. As an example, consider the simple class declaration

class C a b where 
  data T a 

Only one of the two class parameters is a parameter to the data family. Hence, the following instance declaration is invalid:

instance C [c] d where
  data T [c] = MkT (c, d)    -- WRONG!!  'd' is not in scope

Here, the right-hand side of the data instance mentions the type variable d that does not occur in its left-hand side. We cannot admit such data instances as they would compromise type safety.

To explore the "it would compromise type safety" point, imagine this GHCi session:

> :kind! Result
Result :: * -> *
= {- ... well, what? m? -}

You probably mean type Result prefix (ReaderT prefix m) = m.

There are still errors remaining. Notably, the kind of m is inconsistent; MonadTrans needs a parameter of kind (* -> *) -> * -> * while MonadReader's second parameter needs * -> *. I don't see why you need MonadTrans.

I don't understand what you mean by "forcing all associated type instances to be monomorphic types"; the Result type you've written isn't really a type function, because it doesn't have any parameters; there aren't any type variables on its LHS.

Here's something that compiles:

class ( Monad (Result m)
      , MonadReader prefix m
      ) => FooReader prefix (m :: * -> *) where
  type Result m :: * -> *
  runFooReader :: forall b. m b -> prefix -> Result m b

instance Monad m => FooReader prefix (ReaderT prefix m) where
  type Result (ReaderT prefix m) = m
  runFooReader = runReaderT

 

> :kind! Result (ReaderT Int IO)
Result (ReaderT Int IO) :: * -> *
= IO