[GHC] #14860: QuantifiedConstraints: Can't quantify constraint involving type family

[GHC]

#14860: QuantifiedConstraints: Can't quantify constraint involving type family
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:
      Resolution:                    |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #16123            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Out of all the workarounds documented on this issue, I somehow overlooked
 the best one: Iceland_jack's solution in comment:16 involving `Dict`s.
 This offers a general blueprint to how to sneak type families into
 quantified constraints in the event that the trick in comment:1 doesn't
 work.

 In the particular example of comment:18, we wish to use `Show (T a b)` in
 the head of a quantified constraint. While this isn't directly possible,
 we can define a "class newtype" around `Show (T a b)` and use //that// in
 the head of a quantified constraint:

 {{{#!hs
 class    Show (T a b) => ShowT a b
 instance Show (T a b) => ShowT a b

 class (forall b. Show b => ShowT a b) => C a where
   type family T a :: * -> *
 }}}

 If we try to define a `Show` instance for `D`, it first appears as though
 we are stuck:

 {{{#!hs
 data D a = MkD (T a Int)

 instance C a => Show (D a) where
   showsPrec p (MkD x)
     = showParen (p > 10) $ showString "MkD " . showsPrec 11 x
 }}}
 {{{
 Bug.hs:35:48: error:
     • Could not deduce (Show (T a Int))
         arising from a use of ‘showsPrec’
       from the context: C a
         bound by the instance declaration at Bug.hs:33:10-26
     • In the second argument of ‘(.)’, namely ‘showsPrec 11 x’
       In the second argument of ‘($)’, namely
         ‘showString "MkD " . showsPrec 11 x’
       In the expression:
         showParen (p > 10) $ showString "MkD " . showsPrec 11 x
    |
 35 |     = showParen (p > 10) $ showString "MkD " . showsPrec 11 x
    |                                                ^^^^^^^^^^^^^^
 }}}

 GHC appears to be unable to conclude `Show (T a Int)` from `ShowT a Int`.
 But we can help guide GHC along manually by taking advantage of the ever-
 helpful `Dict` data type:

 {{{
 data Dict c =
   c => Dict

 showTDict :: forall a b. Dict (ShowT a b) -> Dict (Show (T a b))
 showTDict Dict = Dict
 }}}

 Using `showTDict`, we can make our `Show` instance for `D` compile with a
 pinch of pattern guards:

 {{{#!hs
 instance C a => Show (D a) where
   showsPrec p (MkD x)
     | Dict <- showTDict @a @Int Dict
     = showParen (p > 10) $ showString "MkD " . showsPrec 11 x
 }}}

 That's it! With enough persistence, we were able to finally realize
 edsko's dream in comment:18. Having to explicitly match on `Dict`s is a
 bit crude, granted, but this appears to be the best that we can do here at
 the moment.

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