#10651: Type checking issue with existential quantification, rank-n types and constraint kinds -------------------------------------+------------------------------------- Reporter: Roboguy | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.1 (Type checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: | valid program Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- 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): {{{#!hs {-# 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): {{{#!hs 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`: {{{#!hs 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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10651 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler