¿Por qué no funciona el "truco de restricción" en esta instancia de HasField definida manualmente?

Tengo este código (ciertamente extraño) que usa lentes y 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)

La idea es tener una HasFieldinstancia que evoque ReifiedGetters de un proxy, solo por el placer de hacerlo. Pero no 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.

No entiendo por qué r0sigue siendo ambiguo. Utilicé el truco de restricción , y mi intuición es que el encabezado de la instancia debe coincidir, entonces el typechecker lo encontraría r0 ~ Personen las condiciones previas, y eso eliminaría la ambigüedad.

Si me cambio (HasField k r v, x ~ r)a (HasField k r v, Glass x ~ Glass r)eso, elimina la ambigüedad y se compila bien. Pero, ¿por qué funciona y por qué no funciona a la inversa?

Quizás sorprendentemente, tenía que ver con Glassser polivinílico:

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

Mientras tanto, a diferencia del parámetro tipo de Glass, el "registro" HasFielddebe ser de tipo Type:

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

Si agrego una firma tipo independiente como esta:

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

luego escribe incluso con (HasField k r v, x ~ r).

De hecho, con la amable firma, el "truco de restricción" deja de ser necesario:

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)

Aquí, el flujo de información durante la verificación de tipos parece ser:

• Sabemos que tenemos un Person, así que, a través runGetterdel tipo de campo, HasFielddebe ser ReifiedGetter Person vy rdebe ser Person.
• Porque res Person, el tipo de fuente en el HasFielddebe ser Glass Person. Ahora podemos resolver la Glassyinstancia trivial para the.
• La clave ken el HasFieldse da como un tipo literal: el Symbol name.
• Verificamos las condiciones previas de la instancia. Sabemos ky r, y se determinan conjuntamente vdebido a la HasFielddependencia funcional. La instancia existe (generada automáticamente para los tipos de registro) y ahora sabemos que ves así String. Hemos desambiguado con éxito todos los tipos.