[GHC] #15244: Ambiguity checks in QuantifiedConstraints

[GHC]

#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