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

Question

为什么在签名中使用关联的类型同义词并不意味着相应的约束？

例如，为什么以下内容不能编译：

{-# 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文档似乎没有提到这方面。

Answer 1

如果它暗示了约束，那么任何以任何方式使用关联值的值的人都需要在范围内具有约束。例如，

\n

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

\n

显然对 一无所知，但只要您在调用MyClass范围内，就应该可以使用它。sort :: [AssociatedType a] -> [AssociatedType a]Ord (AssociatedType a)

\n

为了获得像您想要的那样的行为，您需要一个包装的约束而不是关联的类型。这不能用 来完成-XTypeFamilies，但可以用 来完成-XGADTs：

\n

{-# LANGUAGE GADTs #-}\n\nclass MyClass a where\n  bar :: Int\n\ndata MyClassWitness a where\n  MyClassWitness :: MyClass a => MyClassWitness a\n\nfoo :: \xe2\x88\x80 a. MyClassWitness a -> Int\nfoo MyClassWitness = bar @a\n

\n

constraints您还可以使用库中的包装纸来代替自卷包装纸：

\n

import Data.Constraint\n\nfoo :: \xe2\x88\x80 a . Dict (MyClass a) -> Int\nfoo Dict = bar @a\n

\n

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

\n

foo :: \xe2\x88\x80 a . Dict (MyClass a) -> Int\nfoo _ = bar @a\n

\n