Por que o "truque de restrição" não funciona nesta instância do HasField definida manualmente?

Eu tenho esse código (reconhecidamente estranho) que usa lente e GHC .

{-# 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)

A idéia é ter uma HasFieldinstância que evoque ReifiedGetters de um proxy, apenas para o inferno. Mas não está funcionando:

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

Não entendo por que r0permanece ambíguo. Eu usei o truque de restrição , e minha intuição é que o cabeçalho da instância corresponda, o typechecker encontraria r0 ~ Personnas pré-condições e isso removeria a ambiguidade.

Se eu mudar (HasField k r v, x ~ r)para (HasField k r v, Glass x ~ Glass r)isso remove a ambiguidade e compila bem. Mas por que funciona e por que não funciona de outra maneira?

Talvez, surpreendentemente, tenha a ver com Glassser do tipo poli:

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

Enquanto isso, diferentemente do parâmetro type Glass, o "record" in HasFielddeve ser do tipo Type:

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

Se eu adicionar uma assinatura do tipo autônoma como esta:

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

então verifica até mesmo com (HasField k r v, x ~ r).

De fato, com a assinatura gentil, o "truque de restrição" deixa de ser necessário:

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)

Aqui, o fluxo de informações durante a digitação parece ser:

• Sabemos que temos um Person, então-through runGettertipo -a de campo no HasFielddeve ser ReifiedGetter Person ve o rdeve ser Person.
• Porque ré Person, o tipo de fonte no HasFielddeve ser Glass Person. Agora podemos resolver a Glassyinstância trivial para o arquivo the.
• A chave kno HasFieldé fornecida como um tipo literal: o Symbol name.
• Verificamos as pré-condições da instância. Conhecemos ke r, e eles determinam em conjunto vpor causa da HasFielddependência funcional. A instância existe (automagicamente gerados para tipos de registro) e agora sabemos que vé String. Desambiguamos com êxito todos os tipos.