[GHC] #15636: Implication constraint priority breaks default class implementations

[GHC]

#15636: Implication constraint priority breaks default class implementations
-------------------------------------+-------------------------------------
           Reporter:  i-am-tom       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.6.1-beta1
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Hello,

 Not 100% sure that this is a bug, but I've done some investigating (with a
 ''lot'' of help from Csongor Kiss) and thought it was, at the very least,
 behaviour worth clarifying. The following code...

 {{{#!hs
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Test where

 class D a where
   f :: a -> String
   g :: a -> String
   g = f

 class C a

 instance (forall a. C a => D a) => D x where
   f _ = "uh oh"
 }}}

 ... produces the error:

 {{{
     • Could not deduce (C x) arising from a use of ‘Test.$dmg’
       from the context: forall a. C a => D a
         bound by the instance declaration at Test.hs:19:10-38
       Possible fix: add (C x) to the context of the instance declaration
     • In the expression: Test.$dmg @(x)
       In an equation for ‘g’: g = Test.$dmg @(x)
       In the instance declaration for ‘D x’
    |
 19 | instance (forall a. C a => D a) => D x where
    |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 It appears that the problem here is with the default implementation for
 `g`. Namely, when `f` is called, two matching instances are found:

 - `forall a. C a => D a`
 - `(forall a. C a => D a) => D x`

 The issue, as far as we can tell, is that the first instance is chosen
 (and then the constraint check fails). I'm currently working around this
 by introducing a newtype into the head of the quantified constraint†, but
 I thought it best to check whether this is a bug or, indeed, the expected
 behaviour in this situation.

 Let me know if I've missed anything from this ticket - it's my first one!

 Thanks,
 Tom

 † An example of this can be found at https://github.com/i-am-tom/learn-
 me-a-haskell/blob/dbf2a22c5abb78ab91124dcf1e0e7ecd3d88831d/src/Bag/QuantifiedInstances.hs#L92-L94

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