[GHC] #15989: Adding extra quantified constraints leads to resolution failure

2 Dec 2018


      #15989: Adding extra quantified constraints leads to resolution failure
-------------------------------------+-------------------------------------
           Reporter:  eror           |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.3
          Component:  Compiler       |           Version:  8.6.2
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{
 {-# LANGUAGE QuantifiedConstraints, FlexibleContexts #-}

 import Control.Monad.Reader

 data T x = T { anX :: x, anInt :: Int }


 ok :: ( forall x x'. MonadReader (T x) (m x') )
    => m y Bool
 ok = fmap not (pure True)

 bad :: ( forall x x'. MonadReader (T x) (m x')
        , forall x. Monad (m x) )
     => m y Bool
 bad = fmap not (pure True)

 better :: ( forall x x'. MonadReader (T x) (m x')
           , forall x. Applicative (m x)
           , forall x. Functor (m x) )
        => m y Bool
 better = fmap not (pure True)
 }}}

 `ok` and `better` compile, but `bad` fail to resolve, despite having
 strictly more in the context than `ok`:

 {{{
 BadQC.hs:15:7: error:
     • Could not deduce (Functor (m y)) arising from a use of ‘fmap’
       from the context: (forall x x'. MonadReader (T x) (m x'),
                          forall x. Monad (m x))
         bound by the type signature for:
                    bad :: forall (m :: * -> * -> *) y.
                           (forall x x'. MonadReader (T x) (m x'), forall
 x. Monad (m x)) =>
                           m y Bool
         at BadQC.hs:(12,1)-(14,15)
     • In the expression: fmap not (pure True)
       In an equation for ‘bad’: bad = fmap not (pure True)
    |
 15 | bad = fmap not (pure True)
    |       ^^^^^^^^^^^^^^^^^^^^

 BadQC.hs:15:17: error:
     • Could not deduce (Applicative (m y)) arising from a use of ‘pure’
       from the context: (forall x x'. MonadReader (T x) (m x'),
                          forall x. Monad (m x))
         bound by the type signature for:
                    bad :: forall (m :: * -> * -> *) y.
                           (forall x x'. MonadReader (T x) (m x'), forall
 x. Monad (m x)) =>
                           m y Bool
         at BadQC.hs:(12,1)-(14,15)
     • In the second argument of ‘fmap’, namely ‘(pure True)’
       In the expression: fmap not (pure True)
       In an equation for ‘bad’: bad = fmap not (pure True)
    |
 15 | bad = fmap not (pure True)
    |                 ^^^^^^^^^
 Failed, no modules loaded.
 }}}


 Also:

 * `( forall x. MonadReader (T x) (m x), forall x. Monad (m x) )` compiles
 — the error seems to require two quantified type variables
 * `( forall x x'. Monad (m x), forall x. Monad (m x) )` reports an
 ambiguity error on the constraint, which makes sense; if I turn on
 `AllowAmbiguousTypes`, it fails with the same error as above — the error
 isn't caused by MPTCs, and it doesn't matter that `x'` is unused
 * `( forall x x'. Foldable (m x), forall x. Monad (m x) )` and `( forall x
 x'. Monad (m x), forall x. Foldable (m x) )` compile — being in the same
 class hierarchy matters
 * `( forall x x'. Applicative (m x), forall x. Monad (m x) )` fails on
 `fmap` (but not `pure`) — which is the superclass doesn't seem to matter

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15989
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler