Re: [GHC] #13985: GHC 8.0 regression: ‘k’ is not in scope during type checking, but it passed the renamer

[GHC]

#13985: GHC 8.0 regression: ‘k’ is not in scope during type checking, but it passed
the renamer
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13738, #14131    |  Differential Rev(s):  Phab:D3872
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Ryan Scott <ryan.gl.scott@…>):

 In [changeset:"0829821a6b886788a3ba6989e57e25a037bb6d05/ghc"
 0829821a/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="0829821a6b886788a3ba6989e57e25a037bb6d05"
 Implicitly bind kind variables in type family instance RHSes when it's
 sensible

 Summary:
 Before, there was a discrepancy in how GHC renamed type synonyms as
 opposed to type family instances. That is, GHC would accept definitions
 like
 this one:

 ```lang=haskell
 type T = (Nothing :: Maybe a)
 ```

 However, it would not accept a very similar type family instance:

 ```lang=haskell
 type family   T :: Maybe a
 type instance T = (Nothing :: Maybe a)
 ```

 The primary goal of this patch is to bring the renaming of type family
 instances up to par with that of type synonyms, causing the latter
 definition
 to be accepted, and fixing #14131.

 In particular, we now allow kind variables on the right-hand sides of type
 (and data) family instances to be //implicitly// bound by LHS type (or
 kind)
 patterns (as opposed to type variables, which must always be explicitly
 bound by LHS type patterns only). As a consequence, this allows programs
 reported in #7938 and #9574 to typecheck, whereas before they would
 have been rejected.

 Implementation-wise, there isn't much trickery involved in making this
 happen.
 We simply need to bind additional kind variables from the RHS of a type
 family
 in the right place (in particular, see `RnSource.rnFamInstEqn`, which has
 undergone a minor facelift).

 While doing this has the upside of fixing #14131, it also made it easier
 to
 trigger #13985, so I decided to fix that while I was in town. This was
 accomplished by a careful blast of `reportFloatingKvs` in `tcFamTyPats`.

 Test Plan: ./validate

 Reviewers: simonpj, goldfire, austin, bgamari

 Reviewed By: simonpj

 Subscribers: rwbarton, thomie

 GHC Trac Issues: #13985, #14131

 Differential Revision: https://phabricator.haskell.org/D3872
 }}}

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