[GHC] #10651: Type checking issue with existential quantification, rank-n types and constraint kinds

[GHC]

#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