How to get rid of these apparently superfluous `undefined`s?

Question

I'm using GHC 9.2.2 and playing with OverloadedRecordDot and generic-lens. As an experiment, I want to use the overloaded dot as a "frontend" to the generic-lens functionality (including type-changing update).

I have these auxiliary definitions:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedRecordDot #-}
import Control.Lens ( (&), (.~), Lens )
import Data.Generics.Product.Fields qualified as G
import GHC.Records (HasField (..))
import GHC.TypeLits (Symbol)
import GHC.Generics (Generic)

-- Basically a 'Control.Lens.Reified.ReifiedLens'.
newtype Lensy s t a b = Lensy (Lens s t a b)

pry :: Lensy s t a b -> Lens s t a b
pry (Lensy l) = l

-- Just a dummy starting point for applying the overloaded dot.
data The s t = The
the :: s -> t -> The s t -- the parameters are just to guide type inference
the s t = The

-- This GHC.Records.HasField instance produces lenses, not values.
-- It piggybacks on Data.Generics.Product.Fields.HasField.
instance G.HasField (field :: Symbol) s t a b 
    => HasField field (The s t) (Lensy s t a b) where
    getField _ = Lensy (G.field @field)

And this example datatype taken from Data.Generics.Product.Fields:

data Human a
  = Human
    { name    :: String
    , address :: String
    , other   :: a
    }
  | HumanNoAddress
    { name    :: String
    , other   :: a
    }
  deriving (Generic, Show)

human :: Human Bool
human = Human { name = "Tunyasz", address = "London", other = False }

Putting my helpers to work, this compiles (don't mind the awful verbosity):

human' :: Human Int
human' = human & pry (the human human').other .~ (42 :: Int)

Passing undefineds as arguments to the the also compiles:

human' :: Human Int
human' = human & pry (the undefined undefined).other .~ (42 :: Int)

Ok, they seem to be unnecessary. Let's get rid of those parameters to the, then:

-- Just a dummy starting point for applying the overloaded dot.
data The s t = The
the :: The s t 
the = The

human' :: Human Int
human' = human & pry the.other .~ (42 :: Int)

Alas, this doesn't compile:

* Ambiguous type variables `s0', `t0',
                           `a0' arising from selecting the field `other'
  prevents the constraint `(HasField
                              "other"
                              (The s0 t0)
                              (Lensy (Human Bool) (Human Int) a0 Int))' from being solved.

How to make the parameterless version of the compile?

Answer 1

Unwitting kind polymorphism strikes again.

ghci> :t the
the :: forall {k1} {k2} (s :: k1) (t :: k2). The s t

It was sufficient to add a kind signature to The:

{-# LANGUAGE KindSignatures #-}
import Data.Kind ( Type )
type The :: Type -> Type -> Type
data The s t = The

And the signature of the becomes:

ghci> :t the
the :: forall s t. The s t