Opened 16 months ago

Closed 15 months ago

## #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

Version: | 8.4.3 → 8.5 |
---|

### comment:2 Changed 15 months ago by

### comment:3 Changed 15 months ago by

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:5 Changed 15 months ago by

Resolution: | → fixed |
---|---|

Status: | new → closed |

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.

You'd never write this, correct? Because if

`a~b`

then the two quantified constraints are identical.But your point is that in

you can't avoid having two identical superclass constraints.

In general if we have two quantified constraints

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?