Dlaczego „sztuczka z ograniczeniami” nie działa w tym ręcznie zdefiniowanym wystąpieniu HasField?

Mam ten (co prawda dziwny) kod, który używa obiektywu i 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)

Chodzi o HasFieldinstancję, która wyczarowuje ReifiedGetters z serwera proxy, na wszelki wypadek. Ale to nie działa:

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

Nie rozumiem, dlaczego r0pozostaje niejednoznaczny. Użyłem sztuczki z ograniczeniami , a moją intuicją jest to, że głowa instancji powinna pasować, a następnie sprawdzanie typów znajdzie się r0 ~ Personw warunkach wstępnych, a to usunie niejednoznaczność.

Jeśli zmienię (HasField k r v, x ~ r)na (HasField k r v, Glass x ~ Glass r)który usuwa niejednoznaczność i kompiluje grzywny. Ale dlaczego to działa i dlaczego nie działa w drugą stronę?

haskell typeclass typechecking

— danidiaz
źródło

Być może, co zaskakujące, miało to związek z Glassbyciem wielorakim:

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

Tymczasem, w przeciwieństwie do parametru type Glass, „record” in HasFieldmusi być swego rodzaju Type:

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

Jeśli dodam samodzielny podpis podobny do tego:

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

to sprawdza typ nawet z (HasField k r v, x ~ r).

W rzeczywistości, dzięki uprzejmości, „sztuczka z ograniczeniami” przestaje być konieczna:

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)

Tutaj przepływ informacji podczas sprawdzania typu wygląda następująco:

Wiemy, że mamy Persontaki runGettertyp pola, który HasFieldmusi być ReifiedGetter Person vi rmusi być Person.
Ponieważ rto Person, typ źródła w HasFieldmusi być Glass Person. Możemy teraz rozwiązać trywialną Glassyinstancję dla the.
Kluczem kw HasFieldpodany jest jako typ dosłownym: the Symbol name.
Sprawdzamy warunki instancji. Wiemy ki rwspólnie ustalają z vpowodu HasFieldzależności funkcjonalnej. Instancja istnieje (generowana automatycznie dla typów rekordów) i teraz wiemy, że tak vjest String. Z powodzeniem ujednoliciliśmy wszystkie typy.

— danidiaz
źródło