[GHC] #14958: QuantifiedConstraints: Doesn't apply implication for existential?
GHC
ghc-devs at haskell.org
Thu Mar 22 10:57:34 UTC 2018
#14958: QuantifiedConstraints: Doesn't apply implication for existential?
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.5
Resolution: | Keywords:
| QuantifiedConstraints, wipT2893
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
This is to do with overlapping instances. We have
{{{
Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) -> Foo
}}}
So from the expression `Foo 10` we have:
Given:
{{{
Skolems: x
Given: d1: forall y. cls0 y => Num y
d2: cls0 x
Wanted: Num x
}}}
Here `cls0` is a unification variable; we don't yet know what it'll tur
out to be, and indeed (given the type of `Foo`) it's ambiguous.
When trying to solve `Num x` GHC doesn't want to use `d1`, because that
make a commitment to solve its sub-goals. If `cls0` turned out to be
`Num`, an alternative would be to pick `d2`. So it simply refrains from
choosing. (The error message doesn't make this clear, I know.)
If you fix `cls0` all is well. For example:
{{{
data Foo (cls :: * -> Constraint) where
Foo :: forall cls.
(forall x. ((forall y. cls y => Num y), cls x) => x)
-> Foo cls
a :: Foo Fractional
a = Foo 10
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14958#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list