#15244: Ambiguity checks in QuantifiedConstraints -------------------------------------+------------------------------------- Reporter: | Owner: (none) bitwiseshiftleft | Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Great work on QuantifiedConstraints! I'm giving it a whirl. With GHCI 8.5.20180605, I see somewhat annoying behavior around multiple instances. When two copies of the same (or equivalent) quantified constraint are in scope, they produce an error. I think this is about some kind of ambiguity check. {{{ {-# LANGUAGE QuantifiedConstraints, TypeFamilies #-} class (forall t . Eq (c t)) => Blah c -- Unquantified works foo :: (Eq (a t), Eq (b t), a ~ b) => a t -> b t -> Bool foo a b = a == b -- Works -- Two quantified instances fail with double ambiguity check errors bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool bar a b = a == b -- Minimal.hs:11:8: error: -- • Could not deduce (Eq (b t1)) -- from the context: (forall t1. Eq (a t1), forall t1. Eq (b t1), -- a ~ b) -- bound by the type signature for: -- bar :: forall (a :: * -> *) (b :: * -> *) t. -- (forall t1. Eq (a t1), forall t1. Eq (b t1), a ~ b) => -- a t -> b t -> Bool -- at Minimal.hs:11:8-78 -- • In the ambiguity check for ‘bar’ -- To defer the ambiguity check to use sites, enable AllowAmbiguousTypes -- In the type signature: -- bar :: (forall t. Eq (a t), forall t. Eq (b t), a ~ b) => -- a t -> b t -> Bool -- | -- 11 | bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool -- | -- [And then another copy of the same error] -- Two copies from superclass instances fail baz :: (Blah a, Blah b, a ~ b) => a t -> b t -> Bool baz a b = a == b -- Minimal.hs:34:11: error: -- • Could not deduce (Eq (b t)) arising from a use of ‘==’ -- from the context: (Blah a, Blah b, a ~ b) -- bound by the type signature for: -- baz :: forall (a :: * -> *) (b :: * -> *) t. -- (Blah a, Blah b, a ~ b) => -- a t -> b t -> Bool -- at Minimal.hs:33:1-52 -- • In the expression: a == b -- In an equation for ‘baz’: baz a b = a == b -- | -- 34 | baz a b = a == b -- | -- Two copies from superclass from same declaration also fail mugga :: (Blah a, Blah a) => a t -> a t -> Bool mugga a b = a == b -- • Could not deduce (Eq (a t)) arising from a use of ‘==’ -- from the context: (Blah a, Blah a) -- bound by the type signature for: -- mugga :: forall (a :: * -> *) t. -- (Blah a, Blah a) => -- a t -> a t -> Bool -- at Minimal.hs:50:1-47 -- • In the expression: a == b -- In an equation for ‘mugga’: mugga a b = a == b -- | -- 51 | mugga a b = a == b -- | -- One copy works quux :: (Blah a, a ~ b) => a t -> b t -> Bool quux a b = a == b -- Works }}} My program is similar to {{{Baz}}}. The constraints {{{Blah a}}} and {{{Blah b}}} are in scope from a pattern match, and I want to compare values of types {{{a t}}} and {{{b t}}} if they're the same type. So I get {{{a ~ b}}} from Typeable and try to compare them, but this doesn't work. I worked around the issue by writing a helper that only takes {{{(Blah a, Typeable a, Typeable b)}}}, so only one instance is in scope. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15244 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler