[GHC] #15952: Reduce zonking-related invariants in the type checker

[GHC]

#15952: Reduce zonking-related invariants in the type checker
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 A call this week clarified a few things:

 A. The second commit in comment:3 exposed an underlying bug. That is, we
 sometimes call `typeKind` in the type checker. This calls `piResultTys`.
 But `piResultTys` calls `substTy`, when really we need `nakedSubstTy`. We
 ''could'' make `tc` equivalents for all these to fix the problem. But
 better is just to go ahead with the plan in this ticket, which also fixes
 the problem.

 B. I've expressed worry about `substTy` encountering a `TcTyVar`. But we
 realized what's really going on: every substitution (in the type-checker)
 morally has a `TcLevel`. Substituting variables ''at or above'' that level
 is highly bogus. But substituting variables ''below'' that level is fine
 -- they're effectively rigid anyway. In practice, this means that we can
 instantiate polytypes that still mention meta-type-variables, ''as long as
 the levels are below the level of the substitution''. Should we actually
 track and check this? Probably not. But it's good to understand what's
 going on. This should be put in a Note.

 C. It's unclear what the advantages/disadvantages are of removing the
 second return value from `tc_infer_hs_type`. In the last, fallthrough case
 of that function, it might be quite a lot easier to return the kind rather
 than reconstruct it. I conjecture that this is purely a performance issue,
 not at all a correctness issue.

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