为什么GHC认为这个类型变量不是单射的？

Question

我有这段代码：

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, GADTs, FlexibleInstances, FlexibleContexts #-}

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin (CatchError h) = \f -> f h

这无法编译，最后一行出现此类型错误：

Could not deduce (a1 ~ a)
from the context (Monad m)
[...]
or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
[...]

如果我将 m 更改为 [] 它编译正常，所以显然 GHC认为 m 不是单射的。 （尽管它不像类型族那样警告单射性。）

我的 GHC 版本是 7.2.1。

编辑：如果我将 (e -> ma) 更改为 e 它可以工作，如果我将其更改为 m a 它就不行，并且对于(ma -> e) 都不是。

Answer 1

这不完全是一个错误，但它是一个很长的故事......

故事

在7.0中曾经有一个名为right的强制构造函数，它的工作原理如下：

g : f a ~ f b
---------------
right g : a ~ b

也就是说，如果g 是 f a 和 f b 之间的强制转换，那么 right g 是 a 和 之间的强制转换b。只有保证 f 是单射的，这才是合理的：否则我们可能合法地拥有，例如，f Int ~ f Char，然后我们就能够得出 Int ~ Char，这会很糟糕。

但当然，类型同义词和类型族不一定是单射的；例如：

type T a = Int

type family F a :: *
type instance F Int  = Bool
type instance F Char = Bool 

那么这种保证如何可能呢？嗯，这正是不允许部分应用类型同义词和类型族的原因。类型同义词和类型族的部分应用可能不是单射的，但饱和应用（即使是导致更高类型的应用）始终是单射的。

当然，对部分申请的限制是令人烦恼的。因此，在 7.2 中，为了朝着允许部分应用的方向发展（并且因为它简化了强制语言的理论和实现），right 构造函数被替换为构造函数 nth，以及伴随的规则

g : T a1 .. an ~ T b1 .. bn
---------------------------
nth i g : ai ~ bi

即，nth 仅适用于强制 g，它位于已知为 a 的饱和应用的两种类型之间。类型构造函数T。理论上，这允许类型同义词和族的部分应用，因为我们无法分解等式，直到我们知道它们位于（必然是单射的）类型构造函数的应用之间。特别是，nth 不适用于强制 fa ~ f b，因为 f 是类型变量，而不是类型构造函数。

当时认为没有人会真正注意到这一变化，但显然这是错误的！

有趣的是，来自 Daniel Schüssler 的 haskell-cafe 消息中概述的 Olegian 技巧表明类型族的实现没有相应改变！问题是，

type family Arg fa
type instance Arg (f a) = a

如果 f 可能是非内射的，则不应允许这样的定义；在这种情况下，这个定义甚至没有意义。

后续步骤

我认为正确的做法是恢复right（或类似的东西），因为人们显然想要它！希望这将很快完成。

与此同时，允许部分应用类型同义词和族仍然非常酷。似乎做到这一点的正确方法（tm）是跟踪种类系统中的单射性：也就是说，每个箭头类型都将用其单射性进行注释。这样，当遇到等式 fa ~ f b 时，我们可以查看 f 的类型，以确定将其分解为等式 a ~ b< 是否安全/代码>。并非巧合的是，我目前正在尝试设计这样一个系统。 =)

Answer 2

我不确定原因，但我将您的测试用例减少为：

{-# LANGUAGE GADTs #-}

data ErrorEff x where
  CatchError :: m a -> ErrorEff (m a)

fin :: ErrorEff (m a) -> m a
fin (CatchError h) = h

它在 GHC 7.0.3 中编译，但不在 7.3.20111021 中编译。

这绝对是一个编译器错误。

更改后编译：

data ErrorEff x where
  CatchError :: x -> ErrorEff x

并且可以使用记录语法恢复函数“fin”：

data ErrorEff x where
  CatchError :: { fin :: m a } -> ErrorEff (m a)