An attempt at making a new default for dataCast1 without restricting poly-kinds.

DataCast.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Main where

import Data.Data
import Data.Kind (Type)
import GHC.Exts (Constraint)

data T (phantom :: k) = T

data D (p :: k -> Constraint) (x :: j) where
  D :: forall (p :: k -> Constraint) (x :: k). p x => D p x

class Possibly p x where
  possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)

-- You'd presumably need to generate an instance of this form for every
-- Data instance. Eww...
instance {-# OVERLAPPING #-} Possibly Data () where
  possibly _ _ = Just D
instance {-# OVERLAPPING #-} Possibly Data Char where
  possibly _ _ = Just D

{-
I tried using a generic Data instance like this:

instance {-# OVERLAPPING #-} Data x => Possibly Data x where
  possibly _ _ = Just D

But this doesn't work well in practice, because _every_ type of kind *
tries to use this instance, and if it doesn't have a Data instance,
it'll produce a type error, which isn't what we want.
-}

-- Fallback instance.
instance {-# OVERLAPPABLE #-} Possibly Data (x :: j) where
  possibly _ _ = Nothing

dataCast1T :: forall k c t (phantom :: k).
              (Typeable t, Possibly Data phantom)
           => (forall d. Data d => c (t d))
           -> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
                 Nothing -> Nothing
                 Just D  -> gcast1 f

instance (Typeable k, Typeable phantom, Possibly Data phantom)
    => Data (T (phantom :: k)) where
  gfoldl _ z T = z T
  gunfold _ z _ = z T
  toConstr T = tConstr
  dataTypeOf _ = tDataType
  dataCast1 = dataCast1T

tDataType :: DataType
tDataType = mkDataType "T" [tConstr]

tConstr :: Constr
tConstr = mkConstr tDataType "T" [] Prefix

newtype Q q x = Q { unQ :: x -> q }
ext1Q :: (Data d, Typeable t)
      => (d -> q)
      -> (forall e. Data e => t e -> q)
      -> d -> q
ext1Q def ext arg =
  case dataCast1 (Q ext) of
    Just (Q ext') -> ext' arg
    Nothing       -> def arg

data NotADataInstance a = NotADataInstance

test1, test2, test3 :: Char
test1 = (const 'p') `ext1Q` (\T -> 'q') $ (T :: T ())
test2 = (const 'p') `ext1Q` (\T -> 'q') $ (T :: T Char)
test3 = (const 'p') `ext1Q` (\T -> 'q') $ (T :: T (NotADataInstance :: Type -> Type))

main :: IO ()
main = putStrLn [test1, test2, test3] -- qqp