下面描述的所有实验都是使用 GHC 8.0.1 完成的。
这个问题是后续问题具有类型别名混淆的 RankNTypes https://stackoverflow.com/q/40252867/2751851。那里的问题归结为像这样的函数类型......
{-# LANGUAGE RankNTypes #-}
sleight1 :: a -> (Num a => [a]) -> a
sleight1 x (y:_) = x + y
...被类型检查器拒绝...
ThinAir.hs:4:13: error:
* No instance for (Num a) arising from a pattern
Possible fix:
add (Num a) to the context of
the type signature for:
sleight1 :: a -> (Num a => [a]) -> a
* In the pattern: y : _
In an equation for `sleight1': sleight1 x (y : _) = x + y
...因为更高阶的约束Num a 不能移动到第二个参数的类型之外 https://stackoverflow.com/a/14593131/2751851（如果我们有的话就有可能a -> a -> (Num a => [a])反而）。既然如此，我们最终尝试为整个事情已经量化的变量添加一个更高等级的约束，即：
sleight1 :: forall a. a -> (Num a => [a]) -> a
完成这个重述后，我们可能会尝试稍微简化一下这个例子。我们来替换一下(+)用不需要的东西Num，并将有问题的参数的类型与结果的类型分开：
sleight2 :: a -> (Num b => b) -> a
sleight2 x y = const x y
这不像以前那样工作（除了错误消息中的细微变化）：
ThinAir.hs:7:24: error:
* No instance for (Num b) arising from a use of `y'
Possible fix:
add (Num b) to the context of
the type signature for:
sleight2 :: a -> (Num b => b) -> a
* In the second argument of `const', namely `y'
In the expression: const x y
In an equation for `sleight2': sleight2 x y = const x y
Failed, modules loaded: none.
Using const然而，这里可能是不必要的，所以我们可以尝试自己编写实现：
sleight3 :: a -> (Num b => b) -> a
sleight3 x y = x
令人惊讶的是，这确实有效！
Prelude> :r
[1 of 1] Compiling Main ( ThinAir.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t sleight3
sleight3 :: a -> (Num b => b) -> a
*Main> sleight3 1 2
1
更奇怪的是，似乎并没有真正的Num对第二个参数的约束：
*Main> sleight3 1 "wat"
1
我不太确定如何使其易于理解。也许我们可以这么说，就像我们可以杂耍一样undefined只要我们从不评估它，一个不可满足的约束就可以很好地保留在类型中，只要它不用于右侧任何地方的统一。然而，这感觉像是一个相当弱的类比，特别是考虑到我们通常理解的非严格性是一个涉及值而不是类型的概念。此外，这并没有让我们更接近于理解世界是如何发生的。String与Num b => b——假设这样的事情真的发生了，但我完全不确定。那么，当约束似乎以这种方式消失时，对正在发生的情况的准确描述是什么？
