为什么这种类型变量不明确,尽管它应该在范围内？

Question

请考虑以下代码:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
class Foo a where
  type Bar a

class Foo a => Foo2 a where
  bar :: Bar a

它在GHC 8.2中给出以下错误消息:

 error:
    • Couldn't match expected type ‘Bar a’ with actual type ‘Bar a0’
      NB: ‘Bar’ is a type function, and may not be injective
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘bar’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method: bar :: forall a. Foo2 a => Bar a
      In the class declaration for ‘Foo2’
  |
7 |   bar :: Bar a
  |   ^^^^^^^^^^^^

有什么问题？为什么它普遍量化a？如果我将最后一行更改为

  bar :: a

问题消失了.为什么它a在范围内没有类型变量呢？

(我现在查看了所有"模糊类型变量"的问题,但似乎没有任何帮助.)

Answer 1

想象一下,您Foo使用相同的关联类型创建两个实例,然后定义

..
{-# LANGUAGE InstanceSigs        #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications    #-}
..

instance Foo Int   where type Bar Int   = Bool
instance Foo Float where type Bar Float = Bool

instance Foo2 Int where
  bar :: Bool
  bar = False

instance Foo2 Float where
  bar :: Bool
  bar = True

这意味着类型bar不足以在Foo2 Int和Foo2 Float实例之间做出决定.

bar :: Foo2 a => Bar a

GHC将尝试a为您推断类型,但如果您要求

bar :: Bool

它无法在Int/ Float或之后可能出现的任何其他实例之间进行选择.您必须使用明确指定类型-XTypeApplications

>>> :set -XTypeApplications
>>
>> bar @Int
False
>> bar @Float
True

编辑:如果每个实例Foo都是不同的类型(Foo是单射的),您可以指定结果使用此语法确定实例类型.. = res | res -> a

..
{-# Language TypeFamilyDependencies #-}

class Foo a where
  type Bar a = res | res -> a

你不能定义Bar Int,Bar Float两者都等于Bool.如果我们只定义Foo Int,Foo2 Int那么bar :: Bool就足以让GHC知道你正在寻找bar @Int = False.