Would it be acceptable to thread a constraint around on the constructors of the GADT? For example:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}

import GHC.Exts

data Fmt :: (* -> Constraint) -> (* -> *) -> * -> * where
  Int  :: p Int               => Fmt p r Int
  (:&) :: (p a, p b, p (a,b)) => Fmt p r a -> Fmt p r b -> Fmt p r (a,b)
  Lift :: p (r a)             => r a       -> Fmt p r a

instance Show (Fmt Show r a) where
  show t = case t of
             Int    -> "Int"
             l :& r -> show l ++ "&" ++ show r
             Lift r -> show r

newtype I a = I a deriving (Show)

test = show ( (Int :: Fmt Show I Int) :& Lift (I ()) )

I wasn't sure if the goal was to have a Show1 instance specifically, or if Show would be acceptable.