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

26 Feb 2018

      #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. I suppose you could add the original program from this ticket:

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

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

 instance (forall a. c a => Show a) => Show (Exists c) where
   show (Exists a) = show a
 }}}

 But this actually fails!

 {{{
 Bug.hs:9:10: error:
     • Could not deduce: c (Exists c)
         arising from a use of ‘GHC.Show.$dmshowsPrec’
       from the context: forall a. c a => Show a
         bound by the instance declaration at Bug.hs:9:10-53
     • In the expression: GHC.Show.$dmshowsPrec @(Exists c)
       In an equation for ‘showsPrec’:
           showsPrec = GHC.Show.$dmshowsPrec @(Exists c)
       In the instance declaration for ‘Show (Exists c)’
     • Relevant bindings include
         showsPrec :: Int -> Exists c -> ShowS (bound at Bug.hs:9:10)
   |
 9 | instance (forall a. c a => Show a) => Show (Exists c) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 Bug.hs:9:10: error:
     • Could not deduce: c (Exists c)
         arising from a use of ‘GHC.Show.$dmshowList’
       from the context: forall a. c a => Show a
         bound by the instance declaration at Bug.hs:9:10-53
     • In the expression: GHC.Show.$dmshowList @(Exists c)
       In an equation for ‘showList’:
           showList = GHC.Show.$dmshowList @(Exists c)
       In the instance declaration for ‘Show (Exists c)’
     • Relevant bindings include
         showList :: [Exists c] -> ShowS (bound at Bug.hs:9:10)
   |
 9 | instance (forall a. c a => Show a) => Show (Exists c) where
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 I'm not sure what to make of this. If you implement `showsPrec` and
 `showList` manually:

 {{{#!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 (forall a. c a => Show a) => Show (Exists c) where
   show (Exists a) = show a
   showsPrec p (Exists a) = showsPrec p a
   showList l = showListWith (\(Exists a) -> shows a) l
 }}}

 Then it typechecks.

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