I have some computations tagged with a type ('A/'B) of a specific kind (T). I would like to eventually depend on the type from the code, so I map the type back, using an instance:
data T = A | B -- also generates types 'A and 'B
class R (t :: T) where r :: Proxy t -> T
instance R 'A where r _ = A
instance R 'B where r _ = B
foo :: forall (t :: T) . R t => Bar T Int
foo = case r (Proxy :: Proxy t) of A -> ....
This is ok, but I wonder if I can spare writing out the R t constraint all the time, if I anyway have the type t annotated with the kind. Is some reorganization of this scheme possible for more convenient use? Thank you.
(Title edit: originally I wrote closed type family, but here it is rather a closed set of types for the given kind.)
The closest I can get to what you want is using PartialTypeSignatures to let GHC infer the constraints, as follows:
{-# LANGUAGE DataKinds, PartialTypeSignatures #-}
import Data.Proxy
data T = A | B
class R (t :: T) where r :: Proxy t -> T
instance R 'A where r _ = A
instance R 'B where r _ = B
data Bar (t :: T) b = Bar
foo :: forall (t :: T) . _ => Bar t Int
-- The _ above tells GHC "infer this for me"
foo = case r (Proxy :: Proxy t) of
A -> undefined
B -> undefined
This will still generate warnings for the use of _, which can be silenced with the compiler flag -Wno-partial-type-signatures.
As always when using inference, be careful. It could happen that GHC might accidentally infer different constraints than the ones you intended to use, making foo compile just fine but then causing mysterious type errors when foo is used later on. Inference is great but can be the source of much confusion sometimes.