Quantified constrained constraints

Qcc.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE QuantifiedConstraints #-}
import Data.Kind (Constraint, Type)
import Data.Monoid (Sum(..))

data Has (c :: Type -> Constraint) = 
  forall t. c t => Has t

class (Monoid a, Show a) => MonoidShow a
instance (Monoid a, Show a) => MonoidShow a

show3 :: Has MonoidShow 
show3 = Has (Sum @Int 3)

withHasShow :: Has Show -> String
withHasShow (Has x) = show x

withCanHaveShow 
  :: (forall a. c a => Show a)
  => Has c
  -> String
withCanHaveShow (Has x) = show x

newtype X a = X a

{-
  Meant to solve same problem illustrated by @withHasShow@, but for definition of an instance
  
  However all methods with default implementation will produce type error
  @Could not deduce: c (X (Has c))
        arising from a use of `GHC.Show.$dmshowList'@
 -}       
instance (forall a. c a => Show a) => Show (X (Has c)) where
  show (X (Has a)) = show a

main = do
  putStrLn . withHasShow $ show3 -- won't compile, MonoidShow too wide even though capable of satisfying
  putStrLn . withCanHaveShow $ show3 -- this one works