Can a typeclass constraint be used in a newtype de

Question

Suppose we have the following newtype definition:

newtype A = A { _run :: Monad m => A -> [Int] -> m Int }

This does not compile with GHC 8.0.2:

error: Not in scope: type variable ‘m’

Replacing m with a concrete typeclass like IO or [] does compile, as I would expect. Given that this is ok, why does GHC not allow the signature above? What is wrong with adding a typeclass constraint inside of this newtype?

Answer 1

It depends on what you're trying to store in A.

If you're trying to store any function like that, as long as m is a Monad, use it as a type parameter, and specify this contraint in your functions:

newtype A m = A { _run :: A m -> [Int] -> m Int }

myFunction :: Monad m => A m -> A m

You could then have things like A [] -> [Int] -> [Int] or A Maybe -> [Int] -> Maybe Int inside the constructor.

f :: A Maybe -> [Int] -> Maybe Int
f _ (x:_) = Just x
f _ [] = Nothing

g :: Monad m => A m -> [Int] -> m Int
g _ xs = return $ head xs

myA :: A Maybe
myA = A f  -- this works

myOtherA :: Monad m => A m
myOtherA = A g  -- this works too

---

On the other hand, if you want to force the data you store to be polymorphic, you can use the GHC extension RankNTypes.

{-# LANGUAGE RankNTypes #-}
newtype A = A { _run :: forall m. Monad m => A -> [Int] -> m Int }

myFunction :: A -> A

You couldn't have things like A -> [Int] -> [Int] or A -> [Int] -> Maybe Int within the constructor, because the forall forces them to be general over any Monad m, so it would have to be of type Monad m => A -> [Int] -> Maybe Int.

f :: A -> [Int] -> Maybe Int
f _ (x:_) = Just x
f _ [] = Nothing

g :: Monad m => A -> [Int] -> m Int
g _ xs = return $ head xs

myA :: A
myA = A f  -- this does not work ; it wants forall m. Monad m => m, not []

myOtherA :: A
myOtherA = A g  -- this does work

This will only really be useful if you intend to use different specific Monad instances for an A-value. For example, Lenses work this way by using different functors to do different things to the lens.

Answer 2

This is possible:

{-# LANGUAGE RankNTypes #-}
newtype A = A { _run :: forall m. Monad m => A -> [Int] -> m Int }

It's hard to tell what you want to do, but this isn't very usable. Any value of type A needs to work for all monads (you don't get to choose).

This is also possible, with the same restrictions:

{-# LANGUAGE GADTs #-}
data A where A :: Monad m => (A -> [Int] -> m Int) -> A

But perhaps you mean something more like

newtype A m = A { _run :: A m -> [Int] -> m Int }

This allows for values of different types of A using different monads.

Answer 3

How would GHC know what instance of Monad to use when you create a piece of data of type A?

Or, put another way, the type variable m isn't in scope on the left hand side of the type definition. That means it doesn't know what m should be, and can't work it out. It's implicit.

I'm sure there's some way you could do what you want to with an extension, probably using an explicit forall. (The RankNTypes extension), however we'd need to know what you were after a bit more.