T2T (term-to-type) transformation in expressions

GHC Proposal #281: Visible forall in types of terms introduces the so-called T2T-Mapping, a term-to-type transformation that comes into play when we typecheck function applications to required type arguments. Example:

f :: forall a -> ...

x = f (Maybe Int)

The Maybe Int argument is parsed and renamed as a term. There is no syntactic marker to tell GHC that it is actually a type argument. We only discover this by the time we get to type checking, where we know that f's type has a visible forall forall a -> at the front, so we are expecting a type argument. More precisely, this happens in tcVDQ in GHC/Tc/Gen/App.hs:

-- See Note [Visible type application and abstraction]
tcVDQ :: ConcreteTyVars              -- See Note [Representation-polymorphism checking built-ins]
      -> (ForAllTyBinder, TcType)    -- Function type
      -> LHsExpr GhcRn               -- Argument type
      -> TcM (TcType, TcType)

What we want is a type to instantiate the forall-bound variable. But what we have is an HsExpr, and we need to convert it to an HsType in order to reuse the same code paths as we use for checking f @ty (see tc_inst_forall_arg).

f (Maybe Int)
-- ^^^^^^^^^
-- parsed & renamed as:   HsApp   (HsVar   "Maybe") (HsVar   "Int")  ::  HsExpr GhcRn
-- must be converted to:  HsTyApp (HsTyVar "Maybe") (HsTyVar "Int")  ::  HsType GhcRn

To a first approximation, T2T can be thought of as a helepr function with the following type:

t2t :: HsExpr GhcRn -> HsType GhcRn    -- 1st attempt

Unfortunately, in practice things are slightly more complicated. The first complication arises from the fact that not all term syntax has corresponding type syntax:

f (\x -> x)

There are no type-level lambdas, so HsType isn't capable of representing this function argument. This means that T2T may fail. We actually have a similar issue when we are checking bidirectional pattern synonyms, except we need to convert between patterns and expressions:

-- GHC/Tc/TyCl/PatSyn.hs

tcPatToExpr :: [LocatedN Name] -> LPat GhcRn
            -> Either PatSynInvalidRhsReason (LHsExpr GhcRn)
-- Given a /pattern/, return an /expression/ that builds a value
-- that matches the pattern.  E.g. if the pattern is (Just [x]),
-- the expression is (Just [x]).  They look the same, but the
-- input uses constructors from HsPat and the output uses constructors
-- from HsExpr.
--
-- Returns (Left r) if the pattern is not invertible, for reason r.

This looks quite similar in spirit. Maybe we could draw inspiration from it?

t2t :: HsExpr GhcRn -> Either T2TError (HsType GhcRn)   -- 2nd attempt

Better, but still not quite there. The second complication arises due to punning of variable names:

x = 42
f, g :: forall a -> ...
f (type x) = g x

The g x function call is renamed as a term, so the x refers to the top-level binding x = 42, not to the type variable binding type x, even though g is expecting a type argument. Remember: we don't know until type checking. Such behavior is well-defined, and the proposal goes to great lengths to specify it (see the "Resolved Syntax Tree" section). Nonetheless, users who are not intimately familiar with the compiler pipeline might find it surprising or confusing. We want a dedicated error message for such conflicts. So the proposal also says:

In the type checking environment, there should be no variable of the same name but from a different namespace, or else raise an ambiguity error (does not apply to constructors).

This means we need access to the type checking environment in addition to reporting warnings or errors. All in all, the path of least resistance seems to be to make t2t monadic

t2t :: HsExpr GhcRn -> TcM (HsType GhcRn)   -- 3rd attempt

Finally, there's also the need to perform a similar transformation in patterns, but let us limit the scope of this ticket to expressions. Patterns are discussed at #23739 (closed)