#15244 closed bug (fixed)

Ambiguity checks in QuantifiedConstraints

Reported by: bitwiseshiftleft Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: testsuite/tests/quantified-constraints/T15244
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (5)

comment:1 Changed 16 months ago by bitwiseshiftleft

Version: 8.4.38.5

comment:2 Changed 15 months ago by simonpj

bar :: (forall t . Eq (a t), forall t . Eq (b t), a ~ b) => a t -> b t -> Bool

You'd never write this, correct? Because if a~b then the two quantified constraints are identical.

But your point is that in

class (forall t . Eq (c t)) => Blah c

baz :: (Blah a, Blah b, a ~ b) => a t -> b t -> Bool

you can't avoid having two identical superclass constraints.

In general if we have two quantified constraints

forall a. Q1 => t a
forall a. Q2 => t a

and we have to solve t Int, say, GHC doesn't know which to pick. (Solving Q1 might be easier than Q2; we don't know.) So it picks neither. And that is what is happening here.

But in this case the quantified constraints are identical; but GHC doesn't currently spot that. It would not be hard to combine identical quantified constraints, which would solve this problem.

Is this an application that matters to you?

comment:3 Changed 15 months ago by bitwiseshiftleft

Thanks for the quick response Simon.

Right, bar is only to help track down the cause. It's the Blah case that's more likely, in particular when the Blah instance comes into scope from a pattern match. Something like (and I didn't test this example):

data GenericBlah t where
    GB :: (Typeable a, Blah a) => a t -> GenericBlah t

instance Eq (GenericBlah t) where
    (GB (a::ca t)) == (GB (b::cb t)) = case eqT @ca @cb of
        Nothing -> False
        Just Refl -> a==b

The constraint inside the Eq instance is equivalent to baz.

I'm exploring QuantifiedConstraints, and might eventually use them at my job. However, QuantifiedConstraints would only be used in a few places. This pattern would be used rare and the bug isn't difficult to work around, so it's not urgent.

comment:4 Changed 15 months ago by Simon Peyton Jones <simonpj@…>

In a169149c/ghc:

Remove duplicate quantified constraints

This is an easy fix for Trac #15244: just avoid adding
the same quantified Given constraint to the inert set twice.

See TcSMonad Note [Do not add duplicate quantified instances].

comment:5 Changed 15 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: testsuite/tests/quantified-constraints/T15244

I fixed this! The fix will be in 8.6.

Note: See TracTickets for help on using tickets.