Note [Quick Look at value arguments]
The function quickLookArg implements the "QL argument" judgement of
the QL paper, in Fig 5 of "A quick look at impredicativity" (ICFP 2020),
rather directly. The key rule, implemented by `quickLookArg` is
G |-h h:sg -- Find the type of the head
G |-inst sg;pis ~> phis;rho_r -- tcInstFun on the args
(A) rho = T sgs OR (B) fiv(phis) = emptyset -- can_do_ql
APP-QL
G |-ql h pis : rho ~> qlUnify( rho, rho_r )
(The paper uses a lightning-bolt where we use "ql".) The most straightforward
way to implement this rule for a call (f e1 ... en) would be:
1. Take a quick look at the argumets e1..en to guide instantiation
of the function f.
2. Then typecheck e1..en from scratch.
That's wasteful, because in Step 1, the quick look at each argument, say (g
h1..hm), involves instantiating `h` and taking a quick look at /its/
arguments. Then in Step 2 we typecheck (g h1..hm) and again take a quick look
at its arguments. This is quadratic in the nesting depth of the arguments.
Instead, after the quick look, we /save/ the work we have done in an EValArgQL
record, and /resume/ it later. The way to think of it is this:
* `tcApp` typechecks an application. It uses `tcInstFun`, which in turn
calls `quickLookArg` on each value argument.
* `quickLookArg` (which takes a quick look at the argument)
- Does the "initial" part of `tcApp`, especially `tcInstFun`
- Captures the result in an EValArgQL record
- Later, `tcValArg` starts from the EValArgQL record, and
completes the job of typechecking the application
This turned out to be more subtle than I expected. Wrinkles:
(QLA1) `quickLookArg` decides whether or not premises (A) and (B) of the
quick-look-arg judgement APP-QL are satisfied; this is captured in
`arg_influences_enclosing_call`.
(QLA2) We avoid zonking, so the `arg_influences_enclosing_call` sees the
argument type /before/ the QL substitution Theta is applied to it. So we
achieve argument-order independence for free (see 5.7 in the paper). See the
`isGuardedTy orig_arg_rho` test in `quickLookArg`.
(QLA3) Deciding whether the premises are satisfied involves calling `tcInstFun`
(which takes quite some work becuase it calls quickLookArg on nested calls).
That's why we want to capture the work done, in EValArgQL.
Do we really have to call `tcInstFun` before deciding (B) of
`arg_influences_enclosing_call`? Yes (#24686).
Suppose ids :: [forall a. a->a], and consider
(:) (reverse ids) blah
`tcApp` on the outer call will instantiate (:) with `kappa`, and take a
quick look at (reverse ids). Only after instantiating `reverse` with kappa2,
quick-looking at `ids` can we discover that (kappa2:=forall a. a->a), which
satisfies premise (B) of `arg_influence_enclosing_call`.
(QLA4) When we resume typechecking an argument, in `tcValArg` on `EValArgQL`
- Calling `tcInstFun` on the argument may have emitted some constraints, which
we carefully captured in `quickLookArg` and stored in the EValArgQL. We must
now emit them with `emitConstraints`. This must be done /under/ the skolemisation
of the argument's type (see `tcSkolemise` in `tcValArg` for EValArgQL { ...}.
Example: f :: (forall b. Ord b => b -> b -> Bool) -> ...
Call: f (==)
we must skolemise the argument type (forall b. Ord b => b -> b -> Bool)
before emitting the [W] Eq alpha constraint arising from the call to (==).
It will be solved from the Ord b!
- quickLookArg may or may not have done `qlUnify` with the calling context.
If not (eaql_encl = False) must do so now. Example: choose [] ids,
where ids :: [forall a. a->a]
choose :: a -> a -> a
We instantiate choose with `kappa` and discover from `ids` that
(kappa = [forall a. a->a]). Now we resume typechecking argument [], and
we must take advantage of what we have now discovered about `kappa`,
to typecheck [] :: [forall a. a->a]
(QLA5) In the quicklook pass, we don't scale multiplicities. Since arguments
aren't typechecked yet, we don't know their free variable usages
anyway. But, in a nested call, the head of an application chain is fully
typechecked.
In order for the multiplicities in the head to be properly scaled, we store
the head's usage environment in the eaql_fun_ue field. Then, when we do the
full-typechecking pass, we can emit the head's usage environment where we
would have typechecked the head in a naive algorithm.
(QLA6) `quickLookArg` is supposed to capture the result of partially typechecking
the argument, so it can be resumed later. "Capturing" should include all
generated type-class/equality constraints and Linear-Haskell usage info. There
are two calls in `quickLookArg1` that might generate such constraints:
- `tcInferAppHead_maybe`. This can generat Linear-Haskell usage info, via
the call to `tcEmitBindingUsage` in `check_local_id`, which is called
indirectly by `tcInferAppHead_maybe`.
In contrast, `tcInferAppHead_maybe` does not generate any type-class or
equality constraints, because it doesn't instantiate any functions. [But
see #25493 and #25494 for why this isn't quite true today.]
- `tcInstFun` generates lots of type-class and equality constraints, as it
instantiates the function. But it generates no usage info, because that
comes only from the call to `check_local_id`, whose usage info is captured
in the call to `tcInferAppHead_maybe` in `quickLookArg1`.
Conclusion: in quickLookArg1:
- capture usage information (but not constraints)
for the call to `tcInferAppHead_maybe`
- capture constraints (but not usage information)
for the call to `tcInstFun` References 0
This Note does not link to any other.
Referenced by 8
- GHC.Tc.Gen.App call site ×5
- Quick Look overview GHC.Tc.Gen.App
- tcApp: typechecking applications GHC.Tc.Gen.App
- EValArgQL GHC.Tc.Gen.Head