dependent fun

Test.hs

{-# LANGUAGE
    AllowAmbiguousTypes
  , DataKinds
  , FlexibleContexts
  , FlexibleInstances
  , GADTs
  , MultiParamTypeClasses
  , PolyKinds
  , RankNTypes
  , ScopedTypeVariables
  , StandaloneDeriving
  , TemplateHaskell
  , TypeApplications
  , TypeFamilies
 #-}

{-# OPTIONS_GHC -ddump-splices #-}

import Data.Constraint.Compose
import Data.Constraint.Extras
import Data.Constraint.Extras.TH
import Data.Dependent.Sum
import Data.GADT.Show

-- Main data structure
data U a t where
  U :: a -> U a '()
deriveArgDict ''U

deriving instance Show a => Show (U a x)
instance Show a => GShow (U a) where gshowsPrec = showsPrec

-- GADT for enumerating "U a t" where "Show a" is satisfied.
-- The intention is to help us write "GShow k => E k -> (GShow v => x) -> x"
-- but we fail, see below.
data E t where
  EB :: E (U Bool)
  EI :: E (U Int)
deriveArgDict ''E

-- an example of a utility function "(GShow v => x)" that we want to convert to
-- just "x" without the constraint requirement (by injecting the relevant
-- constraint on the RHS of a GADT match).
printSum :: forall k v. (GShow k, Has' Show k v) => DSum k v -> IO ()
printSum s = putStrLn (show s)

-- works with a fixed k
applyInt
  :: forall a
   . E (U Int)
  -> (forall (v :: () -> *). Has' Show (U Int) v => a)
  -> a
applyInt d pr = case d of
  EB -> pr @(U Bool)
  EI -> pr @(U Int)

printAnyIntE :: E (U Int) -> DSum (U Int) (U Int) -> IO ()
printAnyIntE e = applyInt e printSum

-- try to generalise to any k, fails :(
apply2
  :: forall s (k :: () -> *) a
   . GShow k
  => E k
  -> (forall (v :: () -> *). Has' Show k v => a)
  -> a
apply2 d pr = case d of
  EB -> pr @(U Bool)
  EI -> pr @(U Int)

printAnyE :: forall k. GShow k => E k -> DSum k (U Int) -> IO ()
printAnyE e = apply2 @k e printSum

main :: IO ()
main = do
  printSum @(U Int) (U 3 :=> U 50)