Why can't a function take a type constrained only by a typeclass?

Question

I don't have quite the vocabulary for phrasing this question (and therefore for searching for answers, so apologies if the answer is easily available). Consider the following

class RunFoo m where
  runFoo :: m a -> a

class RunFooWrapper m where
  doRunFoo :: (RunFoo n) => n a -> m a

newtype RunFast a = RunFast a

newtype RunSlow a = RunSlow a

fooExample :: (RunFoo m) => m Bool
fooExample = undefined

fooWrapperExample :: (RunFooWrapper m) => m Bool
fooWrapperExample = doRunFoo fooExample

This does not compile: Could not deduce (RunFoo n0) arising from a use of ‘doRunFoo’.

It seems that the compiler (GHC 7.10) is insisting on a concrete instantiation of the m from fooExample, and is therefore refusing to continue. But in this case I can't see why the program is ill-typed - fooExample explicitly defines a RunFoo m and all doRunFoo requires is a RunFoo x. So why doesn't this work?

As a supplementary question, is there some kind of special extension (something to do with existential types perhaps) that would allow a program like this? Ideally I'd like to be able to say that doRunFoo takes anything defined existentially (?) as RunFoo m => m (rather than taking any concrete instantiation of RunFoo).

Motivation

I'd like to create composable functions that operate on some aspect of a type constrained by a typeclass - I can provide a concrete example of what I mean if necessary!

Edit with more motivation and alternative implementation

I was curious about the answer to this question in the general case, but I thought I'd add that in the context I ran across this issue what I really wanted is for a sort of constrained delegation between monads. So I wanted to write functions in a monad constrained only by a typeclass that invoked monads in another type class. The top level function could then be run in different contexts, performing the same logic but with the underlying implementation swapped out according to the wrapping monad. As there was a one-to-one correspondence between the wrapping and the implementation monad I was able to use type families to do this, so

class (RunFoo (RunFooM m)) => RunFooWrapper m where
  type RunFooM m :: * -> *
  doRunFoo :: RunFooM m a -> m a

instance RunFooWrapper RunFooWrapperSlow where 
  type RunFooM RunFooWrapperSlow = RunSlow
  doRunFoo :: [...]

This meant that the resolution of the fooExample m was determined by the class context of the wrapper monad, and seems to work fine, but it is a very narrow solution compared to that provided by haoformayor.

This is just the show . read problem. You need to pick a type n for doRunFoo. — Reid Barton
How should the caller of fooWrapperExample specify which instance of RunFoo they want you to use in fooExample? — amalloy
@ReidBarton Yes that will compile but it sadly won't help with the issue here because I specifically don't want to force an particular type. — matchwood
@amalloy Good question - the simple answer in that in my use case for this it doesn't have to - the real point behind the structure I was attempting to capture is that RunFooWrapper will impose a type at some point (i.e. the implementation of doRunFoo will be free to force any concrete implementation it wants at the time eg (bool :: RunSlow Bool) <- x — matchwood

hao hao · Accepted Answer · 2016-09-13T21:44:44

RankNTypes

{-# language RankNTypes #-}    

class RunFoo m where
  runFoo :: m a -> a

class RunFooWrapper m where
  doRunFoo :: (forall n. RunFoo n => n a) -> m a

fooExample :: RunFoo m => m Bool
fooExample = undefined

fooWrapperExample :: RunFooWrapper m => m Bool
fooWrapperExample = doRunFoo fooExample

The (forall n. RunFoo n => n a) -> m a is the key difference. It lets you pass in fooExample, which has the type forall m. RunFoo m => m Bool (the forall being implicitly added by the compiler) and so the m unifies with the n and everybody is happy. Though I cannot read minds, I believe this type reflects your true intent. You only wanted a RunFoo instance, nothing more, and having the n scoped to the first argument provides it.

The problem was that your given code is implicitly typed as forall n. RunFoo n => n a -> m a. That means you need to first pick an n such that RunFoo n and then come up with a value with type n a to pass in as the first argument. This simple act of moving the parentheses (increasing the rank of n) changes the meaning entirely.

For an example of someone who had the same problem, see this Stack Overflow question. For a better explanation of RankNTypes than I could provide, see Oliver's blog post on it.

Why can't a function take a type constrained only by a typeclass?

1 Answers

RankNTypes