Pourquoi le «truc de contrainte» ne fonctionne-t-il pas dans cette instance HasField définie manuellement?

J'ai ce code (certes bizarre) qui utilise l' objectif et le 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)

L'idée est d'avoir une HasFieldinstance qui évoque des ReifiedGetters à partir d'un proxy, juste pour l'enfer. Mais ça ne marche pas:

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

Je ne comprends pas pourquoi r0reste ambigu. J'ai utilisé l' astuce de contrainte , et mon intuition est que la tête d'instance devrait correspondre, puis le vérificateur de typographie trouverait r0 ~ Persondans les conditions préalables, et cela supprimerait l'ambiguïté.

Si je change (HasField k r v, x ~ r)en (HasField k r v, Glass x ~ Glass r)cela supprime l'ambiguïté et il compile très bien. Mais pourquoi ça marche, et pourquoi ça ne marche pas dans l'autre sens?

GlassÉtonnamment peut-être, cela avait à voir avec le poly-genre:

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

Pendant ce temps, contrairement au paramètre type de Glass, le "record" HasFielddoit être de type Type:

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

Si j'ajoute une signature type autonome comme celle-ci:

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

puis il vérifie même avec (HasField k r v, x ~ r).

En fait, avec la signature aimable, le "truc de contrainte" cesse d'être nécessaire:

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)

Ici, le flux d'informations lors de la vérification typographique semble être:

• Nous savons que nous avons un Person, donc - à travers runGetter- le type de champ dans le HasFielddoit être ReifiedGetter Person vet le rdoit être Person.
• Parce que rc'est Personle type de source dans le HasFielddoit être Glass Person. Nous pouvons maintenant résoudre l' Glassyinstance triviale pour le the.
• La clé kdans le HasFieldest donnée comme un littéral de type: le Symbol name.
• Nous vérifions les conditions préalables de l'instance. Nous savons ket r, et ils déterminent conjointement en vraison de la HasFielddépendance fonctionnelle. L'instance existe (automagiquement généré pour les types d'enregistrement) et maintenant nous savons que vest String. Nous avons réussi à lever l'ambiguïté de tous les types.