#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