Constrained closed type family

Question

Can I convince the compiler that a constraint is always satisfied by the type synonyms in a closed type family? The family is indexed by a finite set of promoted values.

Something along the lines of

data NoShow = NoShow
data LiftedType = V1 | V2 | V3

type family (Show (Synonym (a :: LiftedType)) => Synonym (a :: LiftedType)) where
  Synonym V1 = Int
  Synonym V2 = NoShow -- no Show instance => compilation error
  Synonym V3 = ()

I can enforce a constraint on open type families:

class (Show (Synonym a)) => SynonymClass (a :: LiftedType) where
  type Synonym a
  type Synonym a = ()

instance SynonymClass Int where
  type Synonym V1 = Int

-- the compiler complains here
instance SynonymClass V2 where
  type Synonym V2 = NoShow

instance SynonymClass V3

but the compiler would then have to be able to reason about the fact that there exists an instance of SynonymClass a for each of V1, V2 and V3? But in any case, I'd prefer not to use an open type family.

My motivation for requiring this is that I want to convince the compiler that all instances of a closed type family in my code have Show/Read instances. A simplified example is:

parseLTandSynonym :: LiftedType -> String -> String
parseLTandSynonym lt x =
  case (toSing lt) of
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv =
      case (readEither flv :: Either String (Synonym lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right x  -> "Synonym value: " ++ show x 

[Someone mentioned in the comments that it's not possible - is this because it's technically impossible (and if so, why) or just a limitation of the GHC implementation?]

Answer 1

The problem is that we can't put Synonym in an instance head because it's a type family, and we can't write a "universally quantified" constraint like (forall x. Show (Synonym x)) => ... because there's no such thing in Haskell.

However, we can use two things:

• forall x. f x -> a is equivalent to (exists x. f x) -> a
• singletons's defunctionalization lets us put type families into instance heads anyway.

So, we define an existential wrapper that works on singletons-style type functions:

data Some :: (TyFun k * -> *) -> * where
  Some :: Sing x -> f @@ x -> Some f

And we also include the defunctionalization symbol for LiftedType:

import Data.Singletons.TH
import Text.Read
import Control.Applicative

$(singletons [d| data LiftedType = V1 | V2 | V3 deriving (Eq, Show) |])

type family Synonym t where
  Synonym V1 = Int
  Synonym V2 = ()
  Synonym V3 = Char

data SynonymS :: TyFun LiftedType * -> * -- the symbol for Synonym
type instance Apply SynonymS t = Synonym t

Now, we can use Some SynonymS -> a instead of forall x. Synonym x -> a, and this form can be also used in instances.

instance Show (Some SynonymS) where
  show (Some SV1 x) = show x
  show (Some SV2 x) = show x
  show (Some SV3 x) = show x

instance Read (Some SynonymS) where
  readPrec = undefined -- I don't bother with this now...

parseLTandSynonym :: LiftedType -> String -> String
parseLTandSynonym lt x =
  case (toSing lt) of
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv =
      case (readEither flv :: Either String (Some SynonymS)) of
        Left err -> "Can't parse synonym: " ++ err
        Right x  -> "Synonym value: " ++ show x 

This doesn't directly provide us Read (Synonym t) for any specific choice of t, although we can still read Some SynonymS and then pattern match on the existential tag to check if we got the right type (and fail if it's not right). This pretty much covers all the use cases of read.

If that's not good enough, we can use another wrapper, and lift Some f instances to "universally quantified" instances.

data At :: (TyFun k * -> *) -> k -> * where
  At :: Sing x -> f @@ x -> At f x

At f x is equivalent to f @@ x, but we can write instances for it. In particular, we can write a sensible universal Read instance here.

instance (Read (Some f), SDecide (KindOf x), SingKind (KindOf x), SingI x) =>
  Read (At f x) where
    readPrec = do
      Some tag x <- readPrec :: ReadPrec (Some f)
      case tag %~ (sing :: Sing x) of
        Proved Refl -> pure (At tag x)
        Disproved _ -> empty

We first parse a Some f, then check whether the parsed type index is equal to the index we'd like to parse. It's an abstraction of the pattern I mentioned above for parsing types with specific indices. It's more convenient because we only have a single case in the pattern match on At, no matter how many indices we have. Notice though the SDecide constraint. It provides the %~ method, and singletons derives it for us if we include deriving Eq in the singleton data definitions. Putting this to use:

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv = withSingI slt $ 
      case (readEither flv :: Either String (At SynonymS lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right (At tag x)  -> "Synonym value: " ++ show (Some tag x :: Some SynonymS)

We can also make the conversion between At and Some a bit easier:

curry' :: (forall x. At f x -> a) -> Some f -> a
curry' f (Some tag x) = f (At tag x)

uncurry' :: (Some f -> a) -> At f x -> a
uncurry' f (At tag x) = f (Some tag x)

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv = withSingI slt $ 
      case (readEither flv :: Either String (At SynonymS lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right atx  -> "Synonym value: " ++ uncurry' show atx

Answer 2

If I understand correctly what you want to do, this is not possible. If it were, you could easily construct a non-constant function of type Proxy t -> Bool, along the lines of

data YesNo = Yes | No
class Foo (yn :: YesNo) where foo :: Proxy yn -> Bool
type family (Foo (T t) => T t) where
    T X = Yes
    T y = No

f :: forall t. Proxy t -> Bool
f _ = foo (Proxy (T t))

But you cannot construct such a function, even when all the kinds involved are closed (which is of course either a feature or a limitation of GHC, depending on your point of view).