Difference between type family and partial newtype? (and partial data?)

Question

I've had to interface two libraries where metadata is represented as a type parameter in one and as a record field in the other. I wrote an adaptor using a GADT. Here's a distilled version:

{-# LANGUAGE GADTs #-}

newtype TFId  a = MkId   a
data    TFDup a = MkDup !a !a

data GADT tf where
  ConstructorId  :: GADT TFId
  ConstructorDup :: GADT TFDup

main = do
  f ConstructorId
  f ConstructorDup

f :: GADT tf -> IO ()
f = _

This works. (May not be perfect; comments welcome, but that's not the question.)

It took me some time to get to this working state. My initial intuition was to use a type family for TFId, figuring: “GADT has kind (* -> *) -> *; in ConstructorDup TFDup has kind * -> *; so for ConstructorId I can use the following * -> * type family:”

{-# LANGUAGE TypeFamilies #-}
type family TFId a where TFId a = a

The type constructor does have the same kind * -> *, but GHC apparently won't have it in the same place:

error: …

• The type family ‘TFId’ should have 1 argument, but has been given none
• In the definition of data constructor ‘ConstructorId’ In the data type declaration for ‘GADT’

Well, if it says so…

I'm no sure I understand why it would make such a difference. No using type family stems without applying them? What's going on? Any other (better) way to do?

Answer 1

Injectivity.

type family F :: * -> *
type instance F Int  = Bool
type instance F Char = Bool

here F Int ~ F Char. However,

data G (a :: *) = ...

will never cause G Int ~ G Char. These are guaranteed to be distinct types.

In universal quantifications like

foo :: forall f a. f a -> a

f is allowed to be G (injective) but not allowed to be F (not injective).

This is to make inference work. foo (... :: G Int) can be inferred to have type Int. foo (... :: F Int) is equivalent to foo (... :: Bool) which may have type Int, or type Char -- it's an ambiguous type.

Also consider foo True. We can't expect GHC to choose f ~ F, a ~ Int (or Char) for us. This would involve looking at all type families and see if Bool can be produced by any on them -- essentially, we would need to invert all the type families. Even if this were feasible, it would generate a huge amount of possible solutions, so it would be ambiguous.