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
r2even though it appears aftera. However, as this isn't possible in general (e.g. if the kind ofr2mentioneda, 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).
Edited by sheaf