haskell - 类型家族多态性

Question

所以我有一个函数 apply::proxy tf -> tf Int -> tf Int ，它采用一个旨在携带类型系列的代理，并将 Int 应用于该类型系列以确定第二个参数和返回值。然而，我从 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 拒绝使用 GHC 进行编译并抛出此错误:

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

令人困惑的是，注释掉 test1 并在 test2 中使用 let 绑定(bind)使 GHC 满意，并且一切都可以正常编译。谁能解释一下这是怎么回事？

Answer 1

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

你不能这样做。类型族必须始终得到充分应用，就像它们所概括的类型同义词一样。类型变量永远无法实例化为未饱和的类型族。

这是 GHC 7.8.3 中的一个错误，它尚未拒绝从以下位置开始的程序

f :: Proxy F