## 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 |