[GHC] #5927: A type-level "implies" constraint on Constraints

[GHC]

#5927: A type-level "implies" constraint on Constraints
-------------------------------------+-------------------------------------
        Reporter:  illissius         |                Owner:  (none)
            Type:  feature request   |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.4.1
  checker)                           |             Keywords:
      Resolution:  duplicate         |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #2893             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Hm. That is not at all how I would have expected that instance to be
 solved. I agree that when typechecking `$dmshowsPrec`, we should start
 with:

 * `[W] Show (Exists c)`

 But don't we get that immediately? In other words, this typechecks:

 {{{#!hs
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE UndecidableInstances #-}
 module T5927 where

 import Text.Show

 data Exists c where Exists :: c a => a -> Exists c

 instance Show (Exists c) where
   show = show
   showsPrec = undefined
   showList = undefined
 }}}

 Because when typechecking the RHS of `show`, we need `[W] Show (Exists
 c)`, but we already have that. It's only when we strengthen the context:

 {{{#!hs
 instance  (forall a. c a => Show a) => Show (Exists c) where
   show = show
   showsPrec = undefined
   showList = undefined
 }}}

 That GHC complains:

 {{{
 Bug.hs:12:10: error:
     • Could not deduce: c (Exists c) arising from a use of ‘show’
       from the context: forall a. c a => Show a
         bound by the instance declaration at Bug.hs:11:10-53
     • In the expression: show
       In an equation for ‘show’: show = show
       In the instance declaration for ‘Show (Exists c)’
     • Relevant bindings include
         show :: Exists c -> String (bound at Bug.hs:12:3)
    |
 12 |   show = show
    |          ^^^^
 }}}

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