为什么这个函数在where子句中使用范围类型变量而不是类型检查？ [英] Why does this function that uses a scoped type variable in a where clause not typecheck?

问题描述

我有一个函数在中定义了一个值，其中子句，我想给它一个明确的类型注释。注释需要使用顶级函数中的类型变量，所以我的理解是我需要使用 ScopedTypeVariables 。这是一个最小化的问题：

$ $ p $ { - ＃LANGUAGE ScopedTypeVariables＃ - }

导入Control.Monad.Trans.Except
import Data.Functor.Identity

f :: ExceptT String Identity a - >也许
fm = Nothing
其中x :: Identity（或者String a）
x = runExceptT m


这段代码没有 typecheck。它会失败并显示以下错误消息：
$ b

 =lang-none prettyprint-override> 无法将类型'a'与'a1 '
'a'是由
绑定的刚性类型变量f :: ExceptT的类型签名String Identity a  - >也许在src / Lib.hs：20：6 
'a1'处的
是一个刚性类型变量，由
绑定x :: Identity的类型签名（或者String a1）
在src / Lib.hs：22：14 
预期类型：ExceptT字符串标识a1 
实际类型：ExceptT字符串标识a 
相关绑定包括
x :: Identity（任一字符串a1）（绑定在src / Lib.hs：23：9）
m :: ExceptT字符串标识a（绑定在src / Lib.hs：21：3）
f :: ExceptT字符串标识a  - > ; 
在'runExceptT'的第一个参数中，即'm'
在表达式：runExceptT m 
中 

为什么这会失败？我不明白为什么这会导致问题 - 这看起来像是一本教科书中使用的范围类型变量。作为参考，我使用GHC 7.10.3。

解决方案

您需要一个 explicit forall ：

  { - ＃LANGUAGE ScopedTypeVariables＃ - } 
 
导入Control.Monad.Trans.Except 
导入Data.Functor.Identity 
 
f :: forall a。 ExceptT字符串标识a  - >也许
fm = Nothing 
其中x :: Identity（或者String a）
x = runExceptT m 
  

但为什么

这是一个很好的问题。这似乎是 ScopedTypeVariables 的规则。我们知道在GHC Haskell中，所有的顶级变量隐含地 forall 'd，如记录这里。人们会怀疑GHC开发者为了向后兼容而增加了这种行为：如果没有这个规则，没有打开扩展名的文件可能会在扩展打开后停止类型检查。我们可以很容易想象一个场景，其中中声明的帮助函数阻止无意中重用常用类型变量名称 a，b，c，t ，等等。如果有人能够在GHC源代码中找到显式和隐式 forall 'd变量之间的区别的确切位置，那将是非常好的。

update

在这里我们开始了（尽管这些都是来自评论和欺骗的猜测）：

$ b

• 类型检查用户签名时，函数 tcUserTypeSig 调用 findScopedTyVars 。 TcBinds.hs：ef44606：L1786 TcRnTypes 用于<$ c的过滤器
  

• findScopedTyVars $ c> forall s，方法是调用 tcSplitForAllTys 。 TcRnTypes.hs：ef44606：L1221




• 它是 splitForAllTys 的一个包装，它折叠在一个类型的子类型上以构建一个类型变量列表由 forall s引入。 Types / Type.hs：ef44606：L1361

I have a function that has a value defined in a where clause, and I want to give it an explicit type annotation. The annotation needs to use a type variable from the top-level function, so it was my understanding that I needed to use ScopedTypeVariables. Here is a minimal reduction of the problem:

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Monad.Trans.Except
import Data.Functor.Identity

f :: ExceptT String Identity a -> Maybe a
f m = Nothing
  where x :: Identity (Either String a)
        x = runExceptT m

This code does not typecheck. It fails with the following error message:

Couldn't match type ‘a’ with ‘a1’
  ‘a’ is a rigid type variable bound by
      the type signature for f :: ExceptT String Identity a -> Maybe a
      at src/Lib.hs:20:6
  ‘a1’ is a rigid type variable bound by
       the type signature for x :: Identity (Either String a1)
       at src/Lib.hs:22:14
Expected type: ExceptT String Identity a1
  Actual type: ExceptT String Identity a
Relevant bindings include
  x :: Identity (Either String a1) (bound at src/Lib.hs:23:9)
  m :: ExceptT String Identity a (bound at src/Lib.hs:21:3)
  f :: ExceptT String Identity a -> Maybe a
    (bound at src/Lib.hs:21:1)
In the first argument of ‘runExceptT’, namely ‘m’
In the expression: runExceptT m

Why does this fail? I do not understand why this would cause problems—it seems like a textbook use of scoped type variables. For reference, I am using GHC 7.10.3.

解决方案

You need an explicit forall:

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Monad.Trans.Except
import Data.Functor.Identity

f :: forall a. ExceptT String Identity a -> Maybe a
f m = Nothing
  where x :: Identity (Either String a)
        x = runExceptT m

but why

That is a great question. This appears to be a rule of ScopedTypeVariables. We know in GHC Haskell that all top-level variables are implicitly forall'd, as documented here. One would suspect that the GHC devs added this behavior for backwards compatibility: without this rule, a file without the extension turned on could stop type-checking once the extension was turned on. We can easily imagine a scenario where helper functions declared in the where block to inadvertently reuse the common type variable names a, b, c, t, so on. It would be great if someone could find the exact spot in the GHC source code where this distinction between explicit and implicit forall'd variables arose.

update

Here we go (although this is all guesswork from the comments and grepping):

• While type-checking user signatures, the function tcUserTypeSig invokes findScopedTyVars. TcBinds.hs:ef44606:L1786

• findScopedTyVars in TcRnTypes filters for foralls by calling tcSplitForAllTys. TcRnTypes.hs:ef44606:L1221

• Which is a wrapper around splitForAllTys, which folds over a type's subtypes to build up a list of type variables introduced by foralls. Types/Type.hs:ef44606:L1361

这篇关于为什么这个函数在where子句中使用范围类型变量而不是类型检查？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！