Generalising / DRYing functions which apply to GADTs

gadt-filter-with-typeable.hs

{-# LANGUAGE GADTs, DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main where

import Data.Typeable (cast)
import Type.Reflection

-- See: https://new.reddit.com/r/haskell/comments/yebk9v/generalising_drying_functions_which_apply_to_gadts/

data MyType = TypeOne | TypeTwo
data MyEntity (t :: MyType) where
  MyEntityOne :: String -> MyEntity 'TypeOne
  MyEntityTwo :: String -> String -> MyEntity 'TypeTwo

-- Every value of @MyEntity b@ contains enough information to determine the
-- type @b@ to be a known type.
--
-- This fact can be represented by the following function:
hasTypeable :: MyEntity b -> (Typeable b => MyEntity b -> r) -> r
hasTypeable x@(MyEntityOne {}) f = f x
hasTypeable x@(MyEntityTwo {}) f = f x

filterFor :: forall a b. Typeable a => MyEntity b -> Maybe (MyEntity a)
filterFor x = hasTypeable x (cast :: Typeable b => MyEntity b -> Maybe (MyEntity a))

filterForOne :: forall b. MyEntity b -> Maybe (MyEntity 'TypeOne)
filterForOne = filterFor @'TypeOne

main :: IO ()
main = putStrLn "compiles"