Why isn't the "constraint trick" working in this manually defined HasField instance?

Question

I have this (admittedly weird) code which uses lens and GHC.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)

The idea is having a HasField instance that conjures ReifiedGetters out of a proxy, just for the hell of it. But it isn't working:

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

I don't understand why r0 remains ambiguous. I used the constraint trick, and my intuition is that the instance head should match, then the typechecker would find r0 ~ Person in the preconditions, and that would remove the ambiguity.

If I change (HasField k r v, x ~ r) into (HasField k r v, Glass x ~ Glass r) that removes the ambiguity and it compiles fine. But why does it work, and why doesn't it work the other way?

Answer 1

Perhaps surprisingly, it had to do with Glass being poly-kinded:

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

Meanwhile, unlike the type parameter of Glass, the "record" in HasField has to be of kind Type:

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

If I add a standalone kind signature like this:

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

then it typechecks even with (HasField k r v, x ~ r).

---

In fact, with the kind signature, the "constraint trick" ceases to be necessary:

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)

Here, the flow of information during typechecking seems to be:

• We know we have a Person, so—through runGetter—the field's type in the HasField must be ReifiedGetter Person v and the r must be Person.
• Because r is Person, the source type in the HasField must be Glass Person. We can now resolve the trivial Glassy instance for the the.
• The key k in the HasField is given as a type literal: the Symbol name.
• We check the instance preconditions. We know k and r, and they jointly determine v because of the HasField functional dependency. The instance exists (automagically generated for record types) and now we know that v is String. We have successfully disambiguated all types.