Quantified constraints with type families https://stackoverflow.com/questions/56470600/quantified-constraints-vs-closed-type-families

QCTF.hs

{-# LANGUAGE
    DeriveGeneric,
    QuantifiedConstraints,
    ScopedTypeVariables,
    MultiParamTypeClasses,
    FlexibleInstances,
    ConstraintKinds,
    DataKinds,
    DerivingVia,
    StandaloneDeriving,
    TypeFamilies,
    KindSignatures,
    UndecidableInstances,
    FlexibleContexts,
    TypeOperators,
    PolyKinds #-}

module QCTF where

import Generic.Data
import Data.Kind (Type, Constraint)
import Data.Functor.Identity

import GHC.Generics

type family HKD f a where
    HKD Identity a = a
    HKD f        a = f a

-- Version A1: with Generics

data Result1 f = MkResult1 (HKD f Int) (HKD f Bool)
  deriving Generic

instance GShow0 (Rep (Result1 f)) => Show (Result1 f) where
  showsPrec = gshowsPrec

-- Version A2: with Generics and DerivingVia

data Result2 f = MkResult2 (HKD f Int) (HKD f Bool)
  deriving Generic

deriving via Generically (Result2 f) instance GShow0 (Rep (Result2 f)) => Show (Result2 f)

-- Version B1: with Generics and QuantifiedConstraints

data Result f = MkResult
    { foo :: HKD f Int
    , bar :: HKD f Bool
    }
  deriving Generic

instance (forall a. Show a => ShowHKD f a) => Show (Result f) where
  showsPrec = gshowsPrec :: ShowHKDFields f (Rep (Result HKDTag)) => Int -> Result f -> ShowS

-- Version B2: with Generics, QuantifiedConstraints, and DerivingVia

data Result' f = MkResult' (HKD f Int) (HKD f Bool)
  deriving Generic

deriving via GenericallyHKD Result' f instance (forall a. Show a => ShowHKD f a) => Show (Result' f)

-- Library code
-- This is written once for a large class generic types, so users only have to write a single instance for each type in one of the above styles.
-- As it stands, the code below currently supports only generic types where all fields are of the form (HKD f X) for various types X.
-- This needs some tweaking to support less regular types, e.g., if not all fields are HKD.

-- Library code for version B1

class    Show (HKD f a) => ShowHKD f a
instance Show (HKD f a) => ShowHKD f a

data HKDTag a
type family ShowHKDFields f (r :: Type -> Type) :: Constraint where
  ShowHKDFields f (M1 i c r) = ShowHKDFields f r
  ShowHKDFields f (r1 :+: r2) = (ShowHKDFields f r1, ShowHKDFields f r2)
  ShowHKDFields f (r1 :*: r2) = (ShowHKDFields f r1, ShowHKDFields f r2)
  ShowHKDFields f (K1 i (HKDTag a)) = ShowHKD f a

-- Additional library code for version B2

newtype GenericallyHKD r f = GenericallyHKD (r f)

class GShow0 (Rep (r f)) => GShowRep r f
instance GShow0 (Rep (r f)) => GShowRep r f

instance (Generic (r f), Generic (r HKDTag), ShowHKDFields f (Rep (r HKDTag)), ShowHKDFields f (Rep (r HKDTag)) => GShowRep r f) => Show (GenericallyHKD r f) where
  showsPrec n (GenericallyHKD a) = gshowsPrec n a :: GShowRep r f => ShowS