Type Family Polymorphism

Question

So I have a function apply :: proxy tf -> tf Int -> tf Int which takes a Proxy intended to carry a type family and applies Int to that type family to determine the type of the second argument and return value. However, I'm getting some confusing responses from GHC.

{-# LANGUAGE TypeFamilies #-}

import Data.Proxy

type family F (a :: *) :: * where
    F Int = ()

f :: Proxy F
f = Proxy

apply :: proxy tf -> tf Int -> tf Int
apply _ x = x

-- Doesn't typecheck.
test1 :: ()
test1 = apply f ()

-- Typechecks fine
test2 :: ()
test2 = let g = apply f in g ()

test1 refuses to compile with GHC spitting out this error:

tftest.hs:16:9:
    Couldn't match expected type ‘()’ with actual type ‘F Int’
    In the expression: apply f ()
    In an equation for ‘test1’: test1 = apply f ()

tftest.hs:16:17:
    Couldn't match expected type ‘F Int’ with actual type ‘()’
    In the second argument of ‘apply’, namely ‘()’
    In the expression: apply f ()

Confusingly, commenting out test1 and using a let binding in test2 makes GHC happy and everything compiles fine. Can anyone explain what's going on here?

Answer 1

So I have a function apply :: proxy tf -> tf Int -> tf Int which takes a Proxy intended to carry a type family

You can't do this. Type families must always be fully applied, like the type synonyms of which they are a generalization. A type variable can never be instantiated to a under-saturated type family.

It's a bug in GHC 7.8.3 that it did not already reject your program starting at

f :: Proxy F