Почему «трюк с ограничениями» не работает в этом экземпляре HasField, заданном вручную?

Question

У меня есть этот (по общему признанию странный) код, который использует объектив и GH C .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 s из прокси, просто ради этого. Но это не работает:

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

Я не понимаю, почему r0 остается неоднозначным. Я использовал трюк с ограничением , и моя интуиция заключается в том, что заголовок экземпляра должен совпадать, тогда проверщик типов найдет 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).

---

На самом деле, с доброй подписью «трюк ограничения» перестает быть необходимым:

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.
• Ключ k в HasField задается как литерал типа: Symbol name.
• Мы проверяем предварительные условия экземпляра. Мы знаем k и r, и они совместно определяют v из-за функциональной зависимости HasField. Экземпляр существует (автоматически генерируется для типов записей), и теперь мы знаем, что v равно String. Мы успешно удалили все типы.