[GHC] #15989: Adding extra quantified constraints leads to resolution failure
GHC
ghc-devs at haskell.org
Mon Dec 3 02:40:14 UTC 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 (Type | Version: 8.6.2
checker) |
Resolution: | 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: |
-------------------------------------+-------------------------------------
Description changed by eror:
Old description:
> {{{
> {-# LANGUAGE QuantifiedConstraints, FlexibleContexts #-}
>
> import Control.Monad.Reader
>
> data T x = T
>
> 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
New description:
{{{
{-# LANGUAGE QuantifiedConstraints, FlexibleContexts #-}
import Control.Monad.Reader
data T x = T
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` fails 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#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list