Opened 2 years ago

Closed 2 years ago

#13985 closed bug (fixed)

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

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: polykinds/T13985
Blocked By: Blocking:
Related Tickets: #13738, #14131 Differential Rev(s): Phab:D3872
Wiki Page:


{-# 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  :? 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:  :? for help
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

    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.

Change History (5)

comment:1 Changed 2 years ago by RyanGlScott

I tried looking at this, but I'm not nearly smart enough to sort out the chicken-and-egg problem that I uncovered. I think the solution would be to call reportFloatingKvs somewhere in the code that typechecks data family instances (e.g., tcDataFamInstDecl seems like a good candidate). However, there's a serious problem with that: reportFloatingKvs needs tyvars to do its thing, but tcDataFamInstDecl starts out only having access to type patterns, not tyvars.

To obtain tyvars, tcDataFamInstDecl calls tcFamTyPats, which in turn calls kcDataDefn to kind-check the type patterns. But therein lies the problem: kcDataDefn kind-checks each of the data constructors! By the time we do this, it's too late, since k wasn't rejected yet, so when we hit k when kind-checking a data constructor's existential type variables, GHC can't find it and throws an internal error.

That is, reportFloatingKvs needs tyvars that tcFamTyPats produces, but tcFamTyPats can't produce the tyvars because it hits a kind variable which should have been rejected earlier by reportFloatingKvs. Ugh.

comment:2 Changed 2 years ago by goldfire

I was hoping to nab this in a drive-by fix, but that didn't happen. The solution here, I think, is to put the kind variables in the implicit part of the dfid_pats field. (This is rather like what happens with ordinary data declarations.) Then, they'll be in scope during type-checking and we can discover that they're "floating".

There's an interesting invariant that data instance declarations violate: every Name invented by the renamer must be bound precisely once. Indeed the "not in scope during type checking" error says the invariant is not upheld. It makes me want a linear type system, but we can't always get what we want.

comment:3 Changed 2 years ago by RyanGlScott

Differential Rev(s): Phab:D3872
Status: newpatch

Thanks Richard, that dfid_pats hint helped me figure out a solution to this as part of the grand Phab:D3872 patch, which also fixes #13988 and #14131.

comment:4 Changed 2 years ago by Ryan Scott <…>

In 0829821a/ghc:

Implicitly bind kind variables in type family instance RHSes when it's sensible

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:

type T = (Nothing :: Maybe a)

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

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:

comment:5 Changed 2 years ago by RyanGlScott

Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Test Case: polykinds/T13985
Note: See TracTickets for help on using tickets.