Constraints on closed type families?

Question

I'd like to write a horribly non-parametric version of a function of type

pretty :: (Show a) => a -> Text

such that

pretty :: Text -> Text = id
pretty :: String -> Text = T.pack
pretty :: (Show a) => a -> Text = T.pack . show

So the idea is that anything that already has a Show instance can be turned into a "pretty" Text by just show-ing it, except for Text and String which we want to special-case.

The following code works:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DataKinds, ConstraintKinds #-}
module Pretty (pretty) where

import Data.Text (Text)
import qualified Data.Text as T

type family StringLike a :: Bool where
    StringLike String = True
    StringLike Text = True
    StringLike a = False

class (b ~ StringLike a) => Pretty' a b where
    pretty' :: a -> Text

instance Pretty' String True where
    pretty' = T.pack

instance Pretty' Text True where
    pretty' = id

instance (Show a, StringLike a ~ False) => Pretty' a False where
    pretty' = T.pack . show

type Pretty a = (Pretty' a (StringLike a))

pretty :: (Pretty a) => a -> Text
pretty = pretty'

and it can be used without exporting anything except the pretty function.

However, I am not too happy about the type signature for pretty:

pretty :: (Pretty a) => a -> Text

I feel that since StringLike is a closed type family, there should be a way for GHC to figure out that if only (Show a) holds, (Pretty a) is already satisfied, since:

1. The following hold trivially just by substituting the results of applying StringLike:
(StringLike String ~ True, Pretty' String True)
(StringLike Text ~ True, Pretty' Text True)

2. For everything else, we *also* know the result of applying StringLike:
(Show a, StringLike a ~ False) => (Pretty' a (StringLike a))

Is there a way to convince GHC of this?

A 'ha-ha just serious' idea just occured to me which is to import Prelude qualified, and rename Pretty to Show... — Cactus
"I feel that since StringLike is a closed type family, there should be a way for GHC to figure out that if only (Show a) holds," I think the following is a big problem: StringLike yields a type of kind(-lifted) Bool, Show yields a type of kind Constraint. It's not just that GHC doesn't understand the relationship; they actually follow different laws of logic. With lifted Bool, you assume the law of the excluded middle, but with Constraint, you may not rely on that. — user824425

Twan van Laarhoven Twan van Laarhoven · Accepted Answer · 2014-05-15T13:07:25

I feel that since StringLike is a closed type family, there should be a way for GHC to figure out that if only (Show a) holds, (Pretty a) is already satisfied

To do that would require type inspection, and would break parameteric polymorphism. Consider defining a type family

type family IsInt a :: Bool where
  IsInt Int = True
  IsInt a = False
class (b ~ IsInt a) => TestInt a b where
  isInt :: a -> Bool
instance TestInt Int True where
  isInt _ = True
instance (IsInt a ~ False) => TestInt a False where
  isInt _ = False

Now by your argument, GHC should be able to satisfy TestInt a from (). In other words, we should be able to test for any given type whether it is equal to Int. This is clearly impossible.

Similarly, a Show a dictionary is equivalent to a function a -> ShowS. How would you be able to decide, given just that, whether the argument is StringLike?

Constraints on closed type families?

2 Answers