Specify nested type variable constraints are of same instance in Haskell

Question

The following which uses FooA explicitly as the type in (#) and in queryP compiles as expected:

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Foo where

class Foo a where

newtype FooParser a = FooParser { (#) :: FooA -> (a, FooA) }

queryP :: (FooA -> a) -> FooParser a
queryP f = FooParser $ \(b :: FooA) -> (f b, b)

data FooA = FooA Int
instance Foo FooA where

But when I try to define FooParser and queryP using the typeclass Foo like so:

{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Foo where

class Foo a where

newtype FooParser a = FooParser { (#) :: Foo b => b -> (a, b) }

queryP :: Foo b => (b -> a) -> FooParser a
queryP f = FooParser $ \(b :: Foo b => b) -> (f b, b)

I get a could-not-deduce error:

Foo.hs:11:52:
    Could not deduce (b ~ b1)
    from the context (Foo b)
      bound by the type signature for
                 queryP :: Foo b => (b -> a) -> FooParser a
      at Foo.hs:10:11-42
    or from (Foo b1)
      bound by a type expected by the context: Foo b1 => b1 -> (a, b1)
      at Foo.hs:11:12-53
      ‘b’ is a rigid type variable bound by
          the type signature for queryP :: Foo b => (b -> a) -> FooParser a
          at Foo.hs:10:11
      ‘b1’ is a rigid type variable bound by
           a type expected by the context: Foo b1 => b1 -> (a, b1)
           at Foo.hs:11:12
    Relevant bindings include
      b :: Foo b => b (bound at Foo.hs:11:26)
      f :: b -> a (bound at Foo.hs:11:8)
      queryP :: (b -> a) -> FooParser a (bound at Foo.hs:11:1)
    In the expression: b
    In the expression: (f b, b)

How can I specify that the b in the lambda function in queryP is of the same instance of the typeclass Foo as in the first parameter of f?

Cactus Cactus · Accepted Answer · 2015-08-04T02:44:02

In the type definition

newtype FooParser a = FooParser { (#) :: Foo b => b -> (a, b) }

the type variable b is bound universially in a higher-rank type; i.e. the type of the newly introduced selector function (#) is

*Foo> :t (#)
(#) :: Foo b => FooParser a -> b -> (a, b)

But that means when you construct a FooParser a, the function you pass to the constructor must be typed at b -> (a, b) for any choice of b (as long as Foo b holds):

*Foo> :t FooParser
FooParser :: (forall b. Foo b => b -> (a, b)) -> FooParser a

However, in queryP you are given a function of type b -> a for some choice of b (the b is chosen by the caller, with the only restriction that Foo b will hold).

So if I set b ~ b1 and call queryP, that means I am passing you a function of type f :: b1 -> a. You then have to return to me a function of type forall b. (Foo b) => b -> (a, b) (wrapped in the constructor FooParser).

You can't just use f for this purpose, as for any choice of b other than b1 (e.g. b ~ b2) it will not be of the right type.

In its present form, you can basically only use functions from the Foo class and parametrically sufficiently polymorphic functions to construct your forall b. (Foo b) => b -> (a, b) function. Depending on what you are trying to do, you can either

Change queryP so that it takes a polymorphic function:

queryP :: (forall b. Foo b => (b -> a)) -> FooParser a
queryP f = FooParser $ \b -> (f b, b)

Change FooParser so that b is existentially bound:

{-# LANGUAGE ExistentialQuantification #-}
data FooParser a = forall b. Foo b => FooParser { (#) :: b -> (a, b) }

Note that these two changes mean (and imply) very different things.

Specify nested type variable constraints are of same instance in Haskell

1 Answers