CODEWITHSUNDEEP
haskell
ron
ron

Reputation: 9396

Can I make Haskell's type system pick up class constraint on closed set of types by providing kind signature?

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.)

Upvotes: 1

Views: 46

Answers (1)

chi
chi

Reputation: 116174

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.

Upvotes: 1

Related Questions