Rank-2 polymorphism with a type variable constrained by another type variable

Question

Suppose we want to write a function ifE that takes a boolean, two handler functions (producing results of different types but implementing the same type class c), and some postprocessing function that can handle arbitrary c's. In other words, we want to generalize this function over Show:

ifShow :: (Show b1, Show b2)
       => Bool
       -> (a -> b1)
       -> (a -> b2)
       -> a
       -> (forall v. Show v => v -> res)
       -> res
ifShow b f1 f2 arg postproc = if b then postproc (f1 arg) else postproc (f2 arg)

I've heard there's ConstraintKinds, so let's turn that on and write this:

{-# LANGUAGE RankNTypes, ConstraintKinds, KindSignatures #-}

import Data.Kind

ifE :: forall (c :: Type -> Constraint) a b1 b2 res
     . (c b1, c b2)
    => Bool
    -> (a -> b1)
    -> (a -> b2)
    -> a
    -> (forall v. c v => v -> res)
    -> res
ifE b f1 f2 arg postproc = if b then postproc (f1 arg) else postproc (f2 arg)

Now, GHC (8.10.4 in my case) complains about the type signature itself:

Main.hs:5:8: error:
    • Could not deduce: (c0 b1, c0 b2)
      from the context: (c b1, c b2)
        bound by the type signature for:
                   ifE :: forall (c :: * -> Constraint) a b1 b2 res.
                          (c b1, c b2) =>
                          Bool
                          -> (a -> b1)
                          -> (a -> b2)
                          -> a
                          -> (forall v. c v => v -> res)
                          -> res
        at Main.hs:(5,8)-(12,10)
    • In the ambiguity check for ‘ifE’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        ifE :: forall (c :: Type -> Constraint) a b1 b2 res.
               (c b1, c b2) =>
               Bool
               -> (a -> b1)
                  -> (a -> b2) -> a -> (forall v. c v => v -> res) -> res
  |
5 | ifE :: forall (c :: Type -> Constraint) a b1 b2 res
  |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

Main.hs:5:8: error:
    • Could not deduce: c v
      from the context: (c b1, c b2)
        bound by the type signature for:
                   ifE :: forall (c :: * -> Constraint) a b1 b2 res.
                          (c b1, c b2) =>
                          Bool
                          -> (a -> b1)
                          -> (a -> b2)
                          -> a
                          -> (forall v. c v => v -> res)
                          -> res
        at Main.hs:(5,8)-(12,10)
      or from: c0 v
        bound by a type expected by the context:
                   forall v. c0 v => v -> res
        at Main.hs:(5,8)-(12,10)
    • In the ambiguity check for ‘ifE’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        ifE :: forall (c :: Type -> Constraint) a b1 b2 res.
               (c b1, c b2) =>
               Bool
               -> (a -> b1)
                  -> (a -> b2) -> a -> (forall v. c v => v -> res) -> res
  |
5 | ifE :: forall (c :: Type -> Constraint) a b1 b2 res
  |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

I understand that GHC might have trouble figuring out what c should be (although I'm not sure why it would — can't it do that by unifying c with the type of postproc at the call site?), but the error is telling something slightly different. Namely, for some reason another type variable c0 is introduced, although I would expect c to be bound by the outer forall. What's going on, and where did I mess up?

user_3234959 · Answer

The code looks fine, you can turn on AllowAmbiguousTypes as suggested. By default, GHC rejects the type because when ifE is called, c can not be deduced from the type of arguments.

To better understand why c is ambiguous, note that this type checks:

> foo :: (forall t. Ord t => t->t->Bool) -> Bool ; foo f = f True True
> bar :: forall t. Eq t => t->t->Bool ; bar x y = x == y
> foo bar
True

Note how Eq and Ord do not have to match, it suffices that Ord is a subclass of Eq.

Hence, in your code c does not have to be matched exactly, but represents any subclass of the actual constraint found in your postproc.

Because of this, you will likely also need TypeApplications later on to disambiguate calls to your ifE.

Rank-2 polymorphism with a type variable constrained by another type variable

1 Answers