何时(如果有的话)可以部分应用类型同义词？

Question

显然有点心不在焉,我写了类似下面的内容:

{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE TypeFamilies        #-}

class Foo f where
  type Bar f :: *
  retbar :: Bar f -> IO f

type Baz f = (Foo f, Eq f)

  -- WithBar :: * -> (*->Constraint) -> * -> Constraint
type WithBar b c f = (c f, Bar f ~ b)

instance Foo () where
  type Bar () = ()
  retbar = return

naim :: WithBar () Baz u => IO u  -- why can I do this?
naim = retbar ()

main = naim :: IO ()

只有在成功编译之后,我意识到这实际上不应该工作:Baz被定义为具有一个参数的类型同义词,但是在这里我使用它而没有直接参数.Type synonym ‘Baz’ should have 1 argument, but has been given none当我尝试这样的事情时,通常GHC会咆哮.

现在,不要误会我的意思:我真的希望能够写出来,并且很容易看到它在这个特定的例子中如何工作(简单的内联会WithBar产生签名naim :: (Foo u, Bar u ~ ()) => IO u,这当然很好),但是我不明白为什么它实际上就像这里一样.它可能只是一个ghc-7.8.2允许这个的错误吗？

Answer 1

您的文件在GHC 7.8中编译,但在GHC 7.10中我收到错误:

类型同义词'Baz'应该有1个参数,但是没有给出

在'naim'的类型签名中:naim :: WithBar()Baz u => IO u

添加-XLiberalTypeSynonyms修复错误.因此,这是7.8中的错误.

Answer 2

部分应用程序应由LiberalTypeSynonyms扩展程序启用。

基本上，这会推迟对类型同义词的大多数一致性检查，直到它们被扩展，因此您的“内联”解释基本上是正确的想法。

但是，这里奇怪的是，您的模块中的扩展并未隐含此扩展。我刚刚测试过，部分应用程序通常不适用于ConstraintKinds,TypeFamilies和PolyKinds。（我加的是后者，因为种的扩张前检查，我的测试类型得到否则推断错误的。）

尽管如此，您的文件在 GHCi 7.8.3 中对我来说加载良好。也许这是某种错误，即使有扩展使其合法。

Answer 3

我不知道官方规则是什么，但这种事情在最左外类型同义词扩展策略的基础上工作似乎是合理的。唯一重要的是，在进行其余类型检查之前，可以在单独的终止阶段处理类型同义词。我不知道您是否可以使用部分应用的类型同义词 F 作为另一个类型同义词 G 的参数，只要 G 确保 F 接收其丢失的参数即可，但这肯定与类型同义词的想法一致都是一种浅层的便利。