GHC 未根据输入类型派生类型类实例

Question

我最近一直在通过 Singletons 库在 Haskell 中尝试依赖类型。为了更好地理解，我一直在尝试自己的各种类型的实现，而不使用该库。然而，我在让编译器通过类型类构造正确的单例成员时遇到了问题，并且我的第一直觉无法编译。

特别是，我一直在关注的教程具有这些定义（请参阅https://blog.jle.im/entry/introduction-to-singletons-1.html）：

data DoorState = Locked | Closed | Open deriving (Eq, Show) 
newtype Door (s :: DoorState) = UnsafeMkDoor {doorMaterial :: String} deriving (Eq, Show)

为类型

DoorState

的每个元素定义单例类型族：

data SDoorState :: DoorState -> * where
    SLocked :: SDoorState Locked
    SClosed :: SDoorState Closed
    SOpen :: SDoorState Open

以及用于自动派生单例成员的相应类型类：

class InferDoorState s where
    getSDoorState :: SDoorState s
instance InferDoorState 'Closed where
    getSDoorState = SClosed
instance InferDoorState 'Locked where
    getSDoorState = SLocked
instance InferDoorState 'Open where
    getSDoorState = SOpen

对于下面的函数，教程中的版本确实可以编译，但我想我会按如下方式实现它。功能是将单例类型变成具体元素。这个实现（我的第一直觉）无法编译：

doorStatus_ :: (InferDoorState s) => Door s -> DoorState
doorStatus_ _ = toDoorState getSDoorState -- ERROR!
-- ERROR: Could not deduce (InferDoorState s0) 
--        arising from a use of ‘getSDoorState’

但是，如果我手动指定类型类实例，这会发生：

doorStatus_ :: (InferDoorState s) => Door s -> DoorState
doorStatus_ (_ :: Door s) = toDoorState (getSDoorState @s)

在我看来，编译器应该能够根据输入类型派生关联的类型类实例 - 但它不使用输入函数中指定的约束

Door s

。我不明白这是为什么。

Answer 1

该错误更好地描述为编译器不知道您打算在哪里调用

DoorState

。getSDoorState

毕竟，从技术角度来说，

doorStatus_ :: (InferDoorState s) => Door s -> DoorState
doorStatus_ _ = toDoorState (getSDoorState @_s0)
-- ERROR: don't know what _s0 should be set to!

到

_s0

的论点应该是

getSDoorState

。

s

可能很愚蠢，但仍然是类型正确的。由于

doorStatus_ _ = toDoorState (getSDoorState @Locked)

没有明确的解决方案，因此它没有得到解决，并且您会收到错误。当我编译你的代码时，我得到的完整的 GHC 错误

确实

提到“类型变量_s0不明确”。这才是真正的错误。 （我用下划线标记未解决的漏洞，尽管 GHC 不这样做，也只是将它们称为“类型变量”。）该错误被隐藏在“缺失实例”类型错误下的原因可能是以下 GHC 奥秘的结果。考虑定义

s0

您会注意到像 

-- under -XAllowAmbiguousTypes
test :: forall (s :: DoorState). Int
test = 4

这样的东西将会编译，即使您认为它应该被解释为

main = print test

，并且有一个无法解决的

main = print (test @_s0)

漏洞。然而，GHC 愿意对你玩以下肮脏的把戏：如果程序中存在未解决的类型漏洞，

并且对该类型也没有未解决的约束

，那么程序的行为（通过参数性）实际上可以'这取决于用于填充该孔的类型。所以 GHC 将 _s0 塞进洞里以帮助程序编译。这与

GHC.Exts.Any

ing 过程有关，例如未解决的漏洞

default

，其中

_a

也需要被

Num _a

默认。_a := Int

所以，从GHC的角度来看，你的程序中的错误是这样发现的：

GHC 注意到有一个未解决的类型变量

type family Any :: k where -- "type-level 'undefined'", hence no instances
1. 以及相关约束

   _s0

   。只有 GHC 可以默认
InferDoorState _s0
2. ，这才可以实现，但这不需要任何想要的约束来提及

   _s0 := Any

   。因此 GHC 尝试解决
_s0
3. ，但失败了。 （请注意，存在可用的

   InferDoorState _s0

   没有任何帮助，因为它并不意味着

   InferDoorState s

   。）错误的表述方式是错误消息中首先出现失败的步骤 (3)，但根本原因 (1) 被隐藏了一些。