Inconsistent instantiation of inferred type variables when they don't all come first
Currently, in GHC.Tc.Gen.App.tcInstFun
, when we are instantiating inferred type variables (for example for :type
in GHCi), we instantiate only the inferred type variables that appear before any other quantified type variables.
Example:
{r1 :: RuntimeRep} (a :: TYPE r1) {r2 :: RuntimeRep} (b :: TYPE r2)
Here we will instantiate r1
, but not r2
because r2
comes after a
which we are not instantiating because a
is not an inferred type variable (recall that we are in the case in which inst_fun = inst_inferred
). This means that :type
in GHCi could end up reporting a type like
forall a {r2 :: RuntimeRep} (b :: TYPE r2)
This is just too confusing, in my opinion.
How to fix this?
- Initially I thought we might make an effort to re-arrange the type variables and still instantiate
r2
even though it appears aftera
. However, as this isn't possible in general (e.g. if the kind ofr2
mentioneda
, we wouldn't be able to re-arrange the telescope), and @rae dissuaded me from pursuing it further. -
@mpickering instead suggested that we don't instantiate any inferred type variables when we run into such a situation. This is what I will be pursuing; it only entails adding a single additional check that there are no more splittable quantified variables (in
GHC.Tc.Gen.App.tcInstFun.go1
).