[GHC] #14961: QuantifiedConstraints: class name introduced via an equality constraint does not reduce

[GHC]

#14961: QuantifiedConstraints: class name introduced via an equality constraint
does not reduce
-------------------------------------+-------------------------------------
           Reporter:  mrkgnao        |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints wipT2893     |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #14860
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following doesn't typecheck with the `wip/T2893` branch:

 {{{#!hs
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE TypeFamilies #-}

 module Subst where

 class (forall x. c x => d x) => c ~=> d
 instance (forall x. c x => d x) => c ~=> d

 foo :: forall c a. c ~=> Monoid => (c a => a) -- ok
 foo = mempty

 bar :: forall c a m. (m ~ Monoid, c ~=> m) => (c a => a) -- ok
 bar = mempty

 baz :: forall c a. (forall m. m ~ Monoid => c ~=> m) => (c a => a) --
 fails
 baz = mempty
 }}}

 {{{
 Prelude> :reload
 [1 of 1] Compiling Subst            ( src/Subst.hs, interpreted )

 src/Subst.hs:21:7: error:
     • Could not deduce (Monoid a) arising from a use of ‘mempty’
       from the context: (forall (m :: * -> Constraint).
                          (m ~ Monoid) =>
                          c ~=> m,
                          c a)
         bound by the type signature for:
                    baz :: forall (c :: * -> Constraint) a.
                           (forall (m :: * -> Constraint). (m ~ Monoid) =>
 c ~=> m, c a) =>
                           a
         at src/Subst.hs:20:1-66
       Possible fix:
         add (Monoid a) to the context of
           the type signature for:
             baz :: forall (c :: * -> Constraint) a.
                    (forall (m :: * -> Constraint). (m ~ Monoid) => c ~=>
 m, c a) =>
                    a
     • In the expression: mempty
       In an equation for ‘baz’: baz = mempty
    |
 21 | baz = mempty
    |       ^^^^^^
 Failed, no modules loaded.
 }}}

 Shouldn't the equality constraint be "substituted in"?

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