Application of type family to constant is considered polymorphic when checking levity polymorphism

Summary

In some cases where an expected function type might involve levity polymorphism, but does not due to unification of type family arguments with monomorphic types, GHC considers a function argument to be levity polymorphic unless the entire actual function expression is given a type signature (which presumably shields the check from the potentially polymorphic context).

Similar logic using functional dependencies seems to be free of this issue, though perhaps there is a way to trigger it that I have not found.

Steps to reproduce

Using the attached file T.hs, run:

ghc -c -DWORKAROUND=0 T.hs

and note type resulting error:

T.hs:42:38: error:
    A levity-polymorphic type is not allowed here:
      Type: T Int
      Kind: TYPE (R Int)
    When trying to create a variable of type: T Int
   |
42 | tfam = ignoreF (Proxy :: Proxy Int) (\(x :: Int) -> x)
   |                                      ^^^^^^^^^^^^^^^^

For comparison, try setting WORKAROUND to 1.

Expected behavior

Ideally GHC would notice that R Int evaluates to 'LiftedRep, which is monomorphic.

The scenarios in which this issue matters make challenging use of language extensions and are currently far from any production code. Curiosity aside, this has low priority to me.

Environment

• GHC version used: 8.8.1 (first noticed in 8.6.5)
• Operating System: Linux
• System Architecture: x86_64

T.hs