为什么关联的类型同义词不暗示约束

如何解决为什么关联的类型同义词不暗示约束

为什么在签名中不使用关联的类型同义词暗示相应的约束？

例如为什么不编译以下内容？

{-# LANGUAGE TypeApplications,ScopedTypeVariables,TypeFamilies,AllowAmbiguousTypes #-}

class MyClass a where
  type AssociatedType a 
  bar :: Int

foo :: forall a. AssociatedType a -> Int
foo _ = bar @a

ghc 8.6.5出现以下错误：

error:
    * No instance for (MyClass a) arising from a use of `bar'
      Possible fix:
        add (MyClass a) to the context of
          the type signature for:
            foo :: forall a. AssociatedType a -> Int
    * In the expression: bar @a
      In an equation for `foo': foo _ = bar @a
  |
8 | foo _ = bar @a
  |         ^^^^^^

GHC文档似乎没有提到这方面。

解决方法

如果隐含约束，则任何以任何方式使用关联值的值的人都需要在范围内具有约束。例如，

sort :: Ord a => [a] -> [a]

显然对MyClass一无所知，但只要您在 calling 范围内拥有sort :: [AssociatedType a] -> [AssociatedType a]，就可以将其用作Ord (AssociatedType a)。

要获得看起来像您正在寻找的行为，您需要一个包装约束而不是关联的类型。这无法通过-XTypeFamilies完成，但是可以通过-XGADTs完成：

{-# LANGUAGE GADTs #-}

class MyClass a where
  bar :: Int

data MyClassWitness a where
  MyClassWitness :: MyClass a => MyClassWitness a

foo :: ∀ a. MyClassWitness a -> Int
foo MyClassWitness = bar @a

除了使用自卷式包装器之外，您还可以使用constraints library中的包装器：

import Data.Constraint

foo :: ∀ a . Dict (MyClass a) -> Int
foo Dict = bar @a

在两种情况下，重要的是您实际上是在GADT构造函数上进行模式匹配，因为只有这样才能将约束真正纳入范围。这将不有效：

foo :: ∀ a . Dict (MyClass a) -> Int
foo _ = bar @a

,

因为仅使用类型不需要类型约束。例如，它将编译：

foo :: forall a. AssociatedType a -> Int
foo _ = 42

在运行时，无需将类型类字典传递给此函数，这与类型检查期间缺少约束是一致的。

在您的代码中，需要约束是因为您正在使用bar，而不是因为您正在使用类型。