为什么在这个手动定义的 HasField 实例中“约束技巧”不起作用？

Question

我有这个（公认的奇怪）代码，它使用了lens和GHC.Records：

{-# LANGUAGE DataKinds, PolyKinds, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
import Control.Lens
import GHC.Records 

data Glass r = Glass -- just a dumb proxy

class Glassy r where
  the :: Glass r

instance Glassy x where
  the = Glass

instance (HasField k r v, x ~ r)
-- instance (HasField k r v, Glass x ~ Glass r) 
  => HasField k (Glass x) (ReifiedGetter r v) where
  getField _ = Getter (to (getField @k))

data Person = Person { name :: String, age :: Int } 

main :: IO ()
main = do
  putStrLn $ Person "foo" 0 ^. runGetter (getField @"name" the)

这个想法是有一个从代理HasField中召唤ReifiedGetter出的实例，只是为了它的地狱。但它不起作用：

* Ambiguous type variable `r0' arising from a use of `getField'
  prevents the constraint `(HasField
                              "name"
                              (Glass r0)
                              (ReifiedGetter Person [Char]))' from being solved.

我不明白为什么r0仍然模棱两可。我使用了约束技巧，我的直觉是实例头应该匹配，然后类型检查器会r0 ~ Person在前提条件中找到，这将消除歧义。

如果我(HasField k r v, x ~ r)改成 (HasField k r v, Glass x ~ Glass r)那个消除歧义，它编译得很好。但是为什么它会起作用，为什么它不能以其他方式起作用？

Answer 1

也许令人惊讶的是，它与Glass多类有关：

*Main> :kind! Glass
Glass :: k -> *

同时，与 的类型参数不同Glass，中的“记录”HasField必须是一种Type：

*Main> :set -XPolyKinds
*Main> import GHC.Records
*Main GHC.Records> :kind HasField
HasField :: k -> * -> * -> Constraint

如果我添加这样的独立类型签名：

{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind (Type)
type Glass :: Type -> Type
data Glass r = Glass

然后即使使用(HasField k r v, x ~ r).

事实上，有了善意的签名，“约束技巧”就不再需要了：

instance HasField k r v => HasField k (Glass r) (ReifiedGetter r v) where
  getField _ = Getter (to (getField @k))

main :: IO ()
main = do
  print $ Person "foo" 0 ^. runGetter (getField @"name" the)
  print $ Person "foo" 0 ^. runGetter (getField @"age" the)

在这里，类型检查期间的信息流似乎是：

• 我们知道我们有一个Person，所以 - 通过runGetter- 字段的类型HasFieldmust beReifiedGetter Person v和rmust be Person。
• 因为ris Person， 中的源类型HasField必须是Glass Person。现在，我们可以解决琐碎Glassy的实例the。
• 关键k的HasField是作为一种文字：中Symbol name。
• 我们检查实例先决条件。我们知道k和r，它们v由于HasField函数依赖而共同确定。该实例存在（为记录类型自动生成），现在我们知道它v是String. 我们已经成功地消除了所有类型的歧义。