tcVTA: untested zonk and outdated Note [Visible type application zonk]
In compiler/GHC/Tc/Gen/App.hs
, we have a function for type checking type applications f @t
:
tcVTA :: TcType -- Function type
-> LHsWcType GhcRn -- Argument type
-> TcM (TcType, TcType)
The first thing it does is split off the forall from the function type given to it
tcVTA fun_ty hs_ty
| Just (tvb, inner_ty) <- tcSplitForAllTyVarBinder_maybe fun_ty
, binderFlag tvb == Specified
= do { ...
...
... }
So if the fun_ty
is forall a. a -> a
, then tvb
stands for a
and inner_ty
stands for a -> a
. Quite straightforward so far.
Then, a bit further into the function definition, it zonks the inner_ty
; inner_ty <- liftZonkM $ zonkTcType inner_ty
-- See Note [Visible type application zonk]
But why is this zonk needed? The referenced Note explains
Note [Visible type application zonk]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).
* tcHsTypeApp only guarantees that
- ty_arg is zonked
- kind(zonk(tv)) = kind(ty_arg)
(checkExpectedKind zonks as it goes).
So we must zonk inner_ty as well, to guarantee consistency between zonk(tv)
and inner_ty. Otherwise we can build an ill-kinded type. An example was #14158,
where we had:
id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a
and we had the visible type application
id @(->)
* We instantiated k := kappa, yielding
forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a
* Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *).
* That instantiated (->) as ((->) q1 q1), and unified kappa := q1,
Here q1 :: RuntimeRep
* Now we substitute
cat :-> (->) q1 q1 :: TYPE q1 -> TYPE q1 -> *
but we must first zonk the inner_ty to get
forall (a :: TYPE q1). cat a a
so that the result of substitution is well-kinded
Failing to do so led to #14158.
-}
The issue is that I can't reproduce the problem described by the Note. The test case T14158
passes even if the zonk is removed! In fact, the entire test suite passes. This could mean one of two things:
- The zonk is not needed anymore
- We need a better test case for the zonk
So which one it is? Depending on the answer, the solution to this ticket is either to remove the zonk or to add a new test case.