[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:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           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
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 import Data.Proxy

 data family Fam
 data instance Fam = MkFam (forall (a :: k). Proxy a)
 }}}

 On GHC 8.0.1, 8.0.2, 8.2.1, and HEAD, this fails with a GHC internal
 error:

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Bug.hs
 GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:9:41: error:
     • GHC internal error: ‘k’ is not in scope during type checking, but it
 passed the renamer
       tcl_env of environment: [r1vy :-> APromotionErr FamDataConPE]
     • In the kind ‘k’
       In the type ‘(forall (a :: k). Proxy a)’
       In the definition of data constructor ‘MkFam’
   |
 9 | data instance Fam = MkFam (forall (a :: k). Proxy a)
   |                                         ^
 }}}

 This is a regression, since on GHC 7.10.3, it did not crash:

 {{{
 $ /opt/ghc/7.10.3/bin/ghci Bug.hs
 GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:9:21:
     Data constructor ‘MkFam’ has existential type variables, a context, or
 a specialised result type
       MkFam :: forall (k :: BOX).
                (forall (k :: BOX) (a :: k). Proxy a) -> Fam
       (Use ExistentialQuantification or GADTs to allow this)
     In the definition of data constructor ‘MkFam’
     In the data instance declaration for ‘Fam’
 }}}

 This smells like #13738, but no `TypeApplications` are involved here, so I
 decided to open a separate ticket to be safe.

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