Skip to content

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?

  1. Initially I thought we might make an effort to re-arrange the type variables and still instantiate r2 even though it appears after a. However, as this isn't possible in general (e.g. if the kind of r2 mentioned a, we wouldn't be able to re-arrange the telescope), and @rae dissuaded me from pursuing it further.
  2. @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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information