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 |