Type checking issue with existential quantification, rank-n types and constraint kinds

I'm trying to create a library for working with lists with existentially quantified types and I ran into an issue implementing mapM_ for my type (note that the map and mapM implementations both work fine):

{-# LANGUAGE RankNTypes, ExistentialQuantification, ConstraintKinds #-}
data ConstrList c = forall a. c a => a :> ConstrList c
                  | CNil
infixr :>

constrMap :: (forall a. c a => a -> b) -> ConstrList c -> [b]
constrMap f (x :> xs) = f x : constrMap f xs
constrMap f CNil      = []

constrMapM :: Monad m => (forall a. c a => a -> m b) -> ConstrList c -> m [b]
constrMapM f = sequence . constrMap f

  -- Doesn't work, even with the definition as undefined (?)
constrMapM_ :: Monad m => (forall a. c a => a -> m b) -> ConstrList c -> m ()
constrMapM_ = undefined

It fails with this error message:

/users/dyoung/Test.hs:16:16:
    Couldn't match type ‘b0’ with ‘b’
      ‘b0’ is untouchable
        inside the constraints (c a)
        bound by the type signature for constrMapM_ :: c a => a -> m b0
        at /users/dyoung/Test.hs:16:16-77
      ‘b’ is a rigid type variable bound by
          the type signature for
            constrMapM_ :: Monad m =>
                           (forall a. c a => a -> m b) -> ConstrList c -> m ()
          at /users/dyoung/Test.hs:16:16
    Expected type: a -> m b0
      Actual type: a -> m b
    In the ambiguity check for the type signature for ‘constrMapM_’:
      constrMapM_ :: forall (c :: * -> Constraint) (m :: * -> *) b.
                     Monad m =>
                     (forall a. c a => a -> m b) -> ConstrList c -> m ()
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘constrMapM_’:
      constrMapM_ :: Monad m =>
                     (forall a. c a => a -> m b) -> ConstrList c -> m ()
Failed, modules loaded: none.

If I add AllowAmbiguousTypes, it works when the definition is undefined but it doesn't work if I put the real definition in.

I believe that this is accepted and works as I had intended on 7.8.3 (with the correct definition as well) after talking to some people on IRC, but I haven't personally tested it.

bitemyapp on IRC noticed that it does compile on 7.10.1 if we add an extra argument of type b to both constrMap_ and constrMapM and pass that value from constrMapM_ to constrMap (I think all of those things must happen in order for this to work):

constrMapM :: Monad m => b -> (forall a. c a => a -> m b) -> ConstrList c -> m [b]
constrMapM ignoredB f = sequence . constrMap f

constrMapM_ :: Monad m => b -> (forall a. c a => a -> m b) -> ConstrList c -> m ()
constrMapM_ b f xs = fmap (const ()) (constrMapM b f xs)

Is this expected behavior? I don't fully understand the new ambiguity check.

This kind of reminds me of linear types (or a relevant type system) in a way: we must make explicit use of the b to "discharge" it in order to have a valid type.

Also, I notice that this works fine as well, which makes me think it the type error above is related to ConstraintKinds:

data AnyList f = forall a. (f a) :| (AnyList f)
               | Nil
infixr :|

anyMap :: (forall a. f a -> b) -> AnyList f -> [b]
anyMap f (x :| xs) = f x : anyMap f xs
anyMap _ Nil       = []

anyMapM :: Monad m => (forall a. f a -> m b) -> AnyList f -> m [b]
anyMapM f xs = sequence (anyMap f xs)

anyMapM_ :: Monad m => (forall a. f a -> m b) -> AnyList f -> m ()
anyMapM_ f xs = fmap (const ()) (anyMapM f xs)

Trac metadata

Trac field	Value
Version	7.10.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture