[GHC] #15359: Quantified constraints do not work with equality constraints

11 Jul 2018

      #15359: Quantified constraints do not work with equality constraints
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.5
           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:
-------------------------------------+-------------------------------------
 Feeling abusive toward GHC this morning, I tried this:

 {{{#!hs
 class C a b

 data Dict c where
   Dict :: c => Dict c

 foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
 foo Dict x = x
 }}}

 I thought it wouldn't work, and I was right:

 {{{
     • Class ‘~’ does not support user-specified instances
     • In the quantified constraint ‘forall (a :: k) (b :: k).
                                     C a b =>
                                     a ~ b’
       In the type signature:
         foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
 }}}

 Good. But then I tried something more devious:

 {{{#!hs
 class C a b
 class a ~ b => D a b

 data Dict c where
   Dict :: c => Dict c

 foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b
 foo Dict x = x
 }}}

 This also fails, with ` Couldn't match expected type ‘b’ with actual type
 ‘a’`.

 I'm fine with the second case failing (because I think anything else would
 be very challenging), but the error message is unfortunate. According to
 the semantics of class constraints and quantified constraints, this case
 should be accepted. So if we reject it, we should have a good reason --
 like we offer in the first case. Essentially, we need to explain that any
 logical entailment of an equality constraint simply doesn't hold in the
 presence of a quantified constraint. I neither know a good pithy way of
 explaining that to users nor how to detect when to do so.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler