What happens to missing type variables in Church-style core?

Question

This is a bit esoteric, but maddening. In an answer to another question, I noted that in this entirely valid program

poo :: String -> a -> a
poo _ = id

qoo :: (a -> a) -> String
qoo _ = ""

roo :: String -> String
roo = qoo . poo

the type variable a is neither solved nor generalized in the process of checking roo. I'm wondering what happens in the translation to GHC's core language, a Church-style variant of System F. Let me spell things out longhand, with explicit type lambdas /\ and type applications @.

poo :: forall a. [Char] -> a -> a
poo = /\ a -> \ s x -> id @ a

qoo :: forall a. (a -> a) -> [Char]
qoo = /\ a -> \ f -> [] @ Char

roo :: [Char] -> [Char]
roo = (.) @ [Char] @ (? -> ?) @ [Char] (qoo @ ?) (poo @ ?)

What on earth goes in the ? places? How does roo become a valid core term? Or do we really get a mysterious vacuous quantifier, despite what the type signature says?

roo :: forall a. [Char] -> [Char]
roo = /\ a -> ...

I've just checked that

roo :: forall . String -> String
roo = qoo . poo

goes through ok, which may or may not mean that the thing typechecks with no extra quantification.

What's happening down there?

Answer 1

Here's the core generated by GHC (after adding some NOINLINE pragmas).

qoo_rbu :: forall a_abz. (a_abz -> a_abz) -> GHC.Base.String
[GblId, Arity=1, Caf=NoCafRefs]
qoo_rbu = \ (@ a_abN) _ -> GHC.Types.[] @ GHC.Types.Char

poo_rbs :: forall a_abA. GHC.Base.String -> a_abA -> a_abA
[GblId, Arity=1]
poo_rbs = \ (@ a_abP) _ -> GHC.Base.id @ a_abP

roo_rbw :: GHC.Base.String -> GHC.Base.String
[GblId]
roo_rbw =
  GHC.Base..
    @ (GHC.Prim.Any -> GHC.Prim.Any)
    @ GHC.Base.String
    @ GHC.Base.String
    (qoo_rbu @ GHC.Prim.Any)
    (poo_rbs @ GHC.Prim.Any)

It seems GHC.Prim.Any is used for the polymorphic type.

From the docs (emphasis mine):

The type constructor Any is type to which you can unsafely coerce any lifted type, and back.

• It is lifted, and hence represented by a pointer
• It does not claim to be a data type, and that's important for the code generator, because the code gen may enter a data value but never enters a function value.

It's also used to instantiate un-constrained type variables after type checking.

It makes sense to have such a type to insert in place of un-constrained types, as otherwise trivial expressions like length [] would cause an ambiguous type error.