为什么这个在 where 子句中使用作用域类型变量的函数不进行类型检查? [英] Why does this function that uses a scoped type variable in a where clause not typecheck?

问题描述

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

{-# LANGUAGE ScopedTypeVariables #-}导入 Control.Monad.Trans.Except导入 Data.Functor.Identityf :: 除 T 字符串标识 a ->也许一个f m = 没有其中 x :: 身份(字符串 a)x = runExceptT m

此代码不类型检查.它失败并显示以下错误消息:

无法匹配类型a"和a1"‘a’是一个刚性类型变量，由f :: exceptT String Identity a -> 的类型签名也许一个在 src/Lib.hs:20:6‘a1’是一个刚性类型变量，由x :: Identity 的类型签名(字符串 a1)在 src/Lib.hs:22:14预期类型:ExceptT String Identity a1实际类型:ExceptT String Identity a相关绑定包括x :: Identity (Either String a1)(绑定在 src/Lib.hs:23:9)m :: 除 T 字符串标识 a(绑定在 src/Lib.hs:21:3)f :: 除 T 字符串标识 a ->也许一个(绑定在 src/Lib.hs:21:1)在‘runExceptT’的第一个参数中，即‘m’在表达式中:runExceptT m

为什么会失败?我不明白为什么这会导致问题——这似乎是对作用域类型变量的教科书使用.作为参考，我使用的是 GHC 7.10.3.

解决方案

您需要一个 显式 forall:

{-# LANGUAGE ScopedTypeVariables #-}导入 Control.Monad.Trans.Except导入 Data.Functor.Identityf :: forall a.除了 T 字符串标识 a ->也许一个f m = 没有其中 x :: 身份(字符串 a)x = runExceptT m

但是为什么

这是一个很好的问题.这似乎是 ScopedTypeVariables 的规则.我们知道在 GHC Haskell 中，所有顶级变量都是隐式 forall d，如文档此处.有人会怀疑 GHC 开发人员为了向后兼容而添加了此行为:如果没有此规则，未打开扩展名的文件可能会在打开扩展名后停止类型检查.我们可以很容易地想象一个场景，在 where 块中声明的辅助函数无意中重用了公共类型变量名称 a, b, c, t 等等.如果有人能在 GHC 源代码中找到显式和隐式 forall 变量之间出现这种区别的确切位置，那就太好了.

更新

我们开始(虽然这都是评论和grepping的猜测):

• 在对用户签名进行类型检查时，tcUserTypeSig 函数会调用 findScopedTyVars.TcBinds.hs:ef44606:L1786p>

• findScopedTyVars 在 TcRnTypes 中通过调用 tcSplitForAllTys 为 forall 过滤.TcRnTypes.hs

• 它是 splitForAllTys 的包装器，它折叠类型的子类型以构建由 foralls 引入的类型变量列表.Types/Type.hs:ef43606

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屋！