Suppose f :: (forall a. a->a) -> blah, and we have the application (f e)
Then we want to typecheck `e` pushing in the type `forall a. a->a`. But we
need to be careful:
* Roughly speaking, in (tcPolyExpr e (forall a b. rho)), we skolemise `a` and `b`,
and then call (tcExpr e rho)
* But not quite! We must be careful if `e` is a type lambda (\ @p @q -> blah).
Then we want to line up the skolemised variables `a`,`b`
with `p`,`q`, so we can't just call (tcExpr (\ @p @q -> blah) rho)
* A very similar situation arises with
(\ @p @q -> blah) :: forall a b. rho
Again, we must line up `p`, `q` with the skolemised `a` and `b`.
* Another similar situation arises with
g :: forall a b. rho
g @p @q x y = ....
Here again when skolemising `a` and `b` we must be careful to match them up
with `p` and `q`.
OK, so how exactly do we check @p binders in lambdas? First note that we only
we only attempt to deal with @p binders when /checking/. We don't do inference for
(\ @a -> blah), not yet anyway.
For checking, there are two cases to consider:
* Function LHS, where the function has a type signature
f :: forall a. a -> forall b. [b] -> blah
f @p x @q y = ...
* Lambda \ @p x @q y -> ...
\cases { @p x @q y -> ... }
(\case p behaves like \cases { p -> ... }, and p is always a term pattern.)
Both ultimately handled by matchExpectedFunTys.
* Function LHS case is handled by `GHC.Tc.Gen.Bind.tcPolyCheck`:
* It calls `tcSkolemiseCompleteSig`
* Passes the skolemised variables into `tcFunBindMatches`
* Which uses `matchExpectedFunTys` to decompose the function type to
match the arguments
* And then passes the (skolemised-variables ++ arg tys) on to `tcMatches`
* For the Lambda case there are two sub-cases:
* An expression with a type signature: (\ @a x y -> blah) :: hs_ty
This is handled by `GHC.Tc.Gen.Head.tcExprWithSig`, which kind-checks
the signature and hands off to `tcExprPolyCheck` via `tcPolyLExprSig`.
Note that the foralls at the top of hs_ty scope over the expression.
* A higher order call: h e, where h :: poly_ty -> blah
This is handlded by `GHC.Tc.Gen.Expr.tcPolyExpr`, which (in the
checking case) again hands off to `tcExprPolyCheck`. Here there is
no type-variable scoping to worry about.
So both sub-cases end up in `GHC.Tc.Gen.Expr.tcPolyExprCheck`
* This skolemises the /top-level/ invisible binders, but remembers
the binders as [ExpPatType]
* Then it looks for a lambda, and if so, calls `tcLambdaMatches` passing in
the skolemised binders so they can be matched up with the lambda binders.
* Otherwise it does deep-skolemisation if DeepSubsumption is on,
and then calls tcExpr to typecheck `e`
The outer skolemisation in tcPolyExprCheck is done using
* tcSkolemiseCompleteSig when there is a user-written signature
* tcSkolemiseGeneral when the polytype just comes from the context e.g. (f e)
The former just calls the latter, so the two cases differ only slightly:
* Both do shallow skolemisation
* Both go via checkConstraints, which uses implicationNeeded to decide whether
to build an implication constraint even if there /are/ no skolems.
See Note [When to build an implication] below.
The difference between the two cases is that `tcSkolemiseCompleteSig`
also brings the outer type variables into scope. It would do no
harm to do so in both cases, but I found that (to my surprise) doing
so caused a non-trivial (1%-ish) perf hit on the compiler.
* `tcFunBindMatches` and `tcLambdaMatches` both use `matchExpectedFunTys`, which
ensures that any trailing invisible binders are skolemised; and does so deeply
if DeepSubsumption is on.
This corresponds to the plan: "skolemise at the '=' of a function binding or
at the '->' of a lambda binding". (See #17594 and "Plan B2".)
Some wrinkles
(SK1) tcSkolemiseGeneral and tcSkolemiseCompleteSig make fresh type variables
See Note [Instantiate sig with fresh variables]
(SK2) All skolemisation (even without DeepSubsumption) builds just one implication
constraint for a nested forall like:
forall a. Eq a => forall b. Ord b => blah
The implication constraint will look like
forall a b. (Eq a, Ord b) => <constraints>
See the loop in GHC.Tc.Utils.Instantiate.topSkolemise.
and Note [Skolemisation en-bloc] in that module
Some examples:
* f :: forall a b. blah
f @p x = rhs
`tcPolyCheck` calls `tcSkolemiseCompleteSig` to skolemise the signature, and
then calls `tcFunBindMatches` passing in [a_sk, b_sk], the skolemsed
variables. The latter ultimately calls `tcMatches`, and thence `tcMatchPats`.
The latter matches up the `a_sk` with `@p`, and discards the `b_sk`.
* f :: forall (a::Type) (b::a). blah
f @(p::b) x = rhs
`tcSkolemiseCompleteSig` brings `a` and `b` into scope, bound to `a_sk` and `b_sk` resp.
When `tcMatchPats` typechecks the pattern `@(p::b)` it'll find that `b` is in
scope (as a result of tcSkolemiseCompleteSig) which is a bit strange. But
it'll then unify the kinds `Type ~ b`, which will fail as it should.
* f :: Int -> forall (a::Type) (b::a). blah
f x @p = rhs
`matchExpectedFunTys` does shallow skolemisation eagerly, so we'll skolemise the
forall a b. Then `tcMatchPats` will bind [p :-> a_sk], and discard `b_sk`.
Discarding the `b_sk` means that
f x @p = \ @q -> blah
or f x @p = let .. in \ @q -> blah
will both be rejected: this is Plan B2: skolemise at the "=".
* Suppose DeepSubsumption is on
f :: forall a. a -> forall b. b -> b -> forall z. z
f @p x @q y = rhs
The `tcSkolemiseCompleteSig` uses shallow skolemisation, so it only skolemises
and brings into scope [a :-> a_sk]. Then `matchExpectedFunTys` skolemises the
forall b, because it needs to expose two value arguments. Finally
`matchExpectedFunTys` concludes with deeply skolemising the remaining type.
So we end up with `[p :-> a_sk, q :-> b_sk]`. Notice that we must not
deeply-skolemise /first/ or we'd get the tyvars [a_sk, b_sk, c_sk] which would
not line up with the patterns [@p, x, @q, y]