[GHC] #14288: ScopedTypeVariables with nested foralls broken since 8.0.2

[GHC]

#14288: ScopedTypeVariables with nested foralls broken since 8.0.2
-------------------------------------+-------------------------------------
        Reporter:  MikolajKonarski   |                Owner:  RyanGlScott
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Linux             |         Architecture:  x86_64
 Type of failure:  GHC rejects       |  (amd64)
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Hm. Implementing the renaming part of this patch is a breeze, but
 modifying the typechecker is proving to be a pain. The source of my
 headaches can be traced down to this
 [http://git.haskell.org/ghc.git/blob/0e9681268a38cbc15c9c2b50979624732c9077ce:/compiler/typecheck/TcMType.hs#l437
 tcInstType] function:

 {{{#!hs
 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
                    -- ^ How to instantiate the type variables
            -> Id                                            -- ^ Type to
 instantiate
            -> TcM ([(Name, TcTyVar)], TcThetaType, TcType)  -- ^ Result
                 -- (type vars, preds (incl equalities), rho)
 }}}

 The problem is that at the moment, the first part of the triple that
 `tcInstType` returns corresponds to the lexically scoped type variables.
 But there's an assumption that these variables will all appear
 consecutively, uninterrupted by a `TcThetaType`. With the proposed changes
 in this ticket, this assumption will no longer hold true.

 But I can't just return more type variables in the first part of the
 triple, because almost all call sites of `tcInstType` reconstruct the
 instantiated type with something like `forall <tvs>. <theta-type> => <tc-
 type>`. In other words, cramming more type variables would cause the wrong
 types to be constructed! So `tcInstType` just seems to be designed the
 wrong way for what I want to accomplish, but I can't figure out how to
 redesign it sensibly...

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14288#comment:18>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler