Ambiguity checks in QuantifiedConstraints

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.

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture