Instantiate eagerly in terms
The Visible Type Application paper describes how we can use lazy instantiation in terms to be compatible with visible type application. Specifically, when f
has a polymorphic type (say forall a b. a -> b -> a
), and we use f
in an expression, we do not immediately instantiate it to t1 -> t2 -> t1
. Instead, we wait until seeing arguments, using instantiation to reveal the underlying arrows. This means that visible type arguments @ty
can be used for instantiation.
However, while compelling from a theory standpoint, lazy instantiation has always had an uneasy home within GHC. The biggest problem is that, sometimes, we really do need to instantiate eagerly. Here are two examples:
-
Suppose one defines
f x = show
with no type signature. If we instantiate lazily, we will inferf :: forall {b}. b -> forall a. Show a => a -> String
. This is not the type users want. -
Suppose one defines
plus = (+)
. If we instantiate lazily, we will inferplus :: forall a. Num a => a -> a -> a
. However, the monomorphism restriction compels us to inferplus :: Integer -> Integer -> Integer
(or similar monotype). Indeed, the only way to know whether to apply the monomorphism restriction at all is to instantiate.
Support for the two use cases above involves some delicate code in the type checker, and it would seem to be an improvement to erase this code. Instead of lazy instantiation, we can do eager guided instantiation: GHC can treat an entire application form f @t1 a2 a3 @t4 a5
as a chunk, and instantiate f
according to the parameters present. This would mean that only certain syntactic forms would be allowed at the head of an application with type arguments. Specifically, we think we should support variables, data constructors, literals, and expressions with type annotations. (The algorithm will ignore parentheses.) Given that, in our estimation, the vast majority of uses of visible type application already have this form, this change should break very little code. Note that term-level and type-level arguments can be interleaved in this scenario.
What's lost is code like (let myId :: forall a. a -> a; myId x = x in myId) @Bool True
: note that the head of the application is a let
, not an atom. This seems contrived, however, and I think it's OK to lose.
A few other points in favor of this change:
-
No one has ever asked for the current plan of allowing arbitrary forms in the head of an application with type arguments.
-
@RyanGlScott has said that the current plan causes trouble for the
singletons
package. -
if
andcase
(with multiple branches) already require that their result be a monotype, so this change does not affect them. -
The current scenario caused #13834 (closed) and #17150 (closed), which were terrible error messages caused by using an unbound identifier at the head of a type argument application. While we can do an ad-hoc fix for that particular problem, as long as the head of a visible type application is unconstrained, we won't be able to handle the general case.
-
Currently, we have special-casing for the use of
[]
to allow[] @Int
to work. But this special case is not general:(let in []) @Int
does not work (even though it should).
This ticket is to track explorations @RyanGlScott has volunteered to undertake at exploring breakage. We might even implement the change just to see how the codebase is affected. At some point, we recognize that a proposal will be necessary.
This ticket is made in consultation with @simonpj.