为什么GHC认为这个类型变量不是内射的？
我有这段代码：
{-# 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它的工作原理，如果我改变它ma不它，并且(ma -> e) 。
这不完全是一个错误，但它是一个漫长的故事......
故事
在7.0中曾经有一个叫做right的强制构造函数，它的工作方式如下：
g : f a ~ f b
---------------
right g : a ~ b
也就是说，如果g是fa和fb之间的强制，那么right g就是a和b之间a强制。 这只有在f保证是内射的时候才是合理的：否则我们可以合法地拥有f Int ~ f Char ，然后我们可以得出Int ~ Char ，这将是Bad。
但是，当然，类型同义词和类型族不一定是内射的; 例如：
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 ，这两种类型已知是类型构造函数T饱和应用。 理论上，这允许类型同义词和族的部分应用，因为直到我们知道它们在（必然内射）类型构造函数的应用之间，我们才能分解平等。 特别是， nth不适用于强制fa ~ fb因为f是一个类型变量，而不是类型构造函数。
人们认为在变化的时候没人会注意到，但显然这是错误的！
有趣的是，DanielSchüssler的haskell-cafe消息中概述的Olegian技巧显示，类型族的实现没有相应改变！ 问题是，像一个定义
type family Arg fa
type instance Arg (f a) = a
如果f可以是非内射的，则不应该被允许; 在这种情况下，这个定义甚至没有意义。
下一步
我认为正确的做法是恢复right （或类似的东西），因为人们明显需要它！ 希望这将很快完成。
与此同时，允许部分应用的同义词和家族仍然是非常酷的。 这样做的正确方法似乎是追踪类系统中的注入能力：也就是说，每一种类型的箭头都会注入其注入性。 遇到这样当一个平等fa ~ fb ，我们可以看看那种f以确定它是否是安全的，它分解成平等a ~ b 。 并非巧合的是，我目前正在试图设计这样一个系统。 =）
我不确定原因，但是我将你的测试用例缩减为：
{-# 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)
上一篇: Why does GHC think that this type variable is not injective?