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

{-# 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 (closed), but no TypeApplications are involved here, so I decided to open a separate ticket to be safe.

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related	#13738 (closed)
Blocking
CC
Operating system
Architecture