haskell - 为什么 "constraint trick"在这个手动定义的 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仍然模棱两可。我用了 constraint trick ，我的直觉是实例头应该匹配，然后类型检查器会找到 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) 进行类型检查.

事实上，有了 kind 签名，“约束技巧”就不再是必要的了:

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 — HasField 中的字段类型必须是 ReifiedGetter Person v和 r必须是 Person .

因为r是 Person ，HasField 中的源类型必须是 Glass Person .我们现在可以解决琐碎的 Glassy the 的实例.

key k在 HasField作为类型文字给出:Symbol name .

我们检查实例的前提条件。我们知道k和 r ，他们共同确定v因为 HasField功能依赖。实例存在(为记录类型自动生成)，现在我们知道 v是 String .我们已经成功地消除了所有类型的歧义。