[GHC] #13364: Remove checkValidTelescope

[GHC]

#13364: Remove checkValidTelescope
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 All of this new `TypeInType` nonsense has provided a number of ways that
 we can arrive at ill-scoped kinds. Let's assume we have

 {{{
 data SameKind :: k -> k -> Type
 }}}

 and then here are three subtly ill-scoped kinds:

 {{{
 forall a (b :: a) (c :: Proxy d). SameKind b d
 forall a. forall (b :: a). forall (c :: Proxy d). SameKind b d
 forall d. forall a (b :: a). SameKind b d
 }}}

 Despite the close similarity between these cases, they are all handled
 separately. See `Note [Bad telescopes]` in !TcValidity for an overview,
 but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`,
 and those functions' calls to `checkValidTelescope`,
 `checkZonkValidTelescope`, and `checkValidInferredKinds`.

 While I am unaware of a concrete bug this all causes, it's a mess.

 Better would be to use the existing machinery to prevent skolem-escape:
 `TcLevel`s and implication constraints. Specifically, it's quite plausible
 that all this can be avoided by a simple rule: bump the `TcLevel` (and
 create an implication constraint) for ''every'' new type variable brought
 into scope (including implicitly). (Actually, implicit variables have an
 implicit ordering that GHC is free to decide, so all implicitly bound
 variables should be brought into scope at once, with just one bump in the
 `TcLevel`.)

 It might all just work! And then we can delete gobs of hairy code. Hooray!

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