[GHC] #13985: GHC 8.0 regression: ‘k’ is not in scope during type checking, but it passed the renamer
#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
#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 (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 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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 [http://git.haskell.org/ghc.git/blob/d774b4e2de4f07d2432b67010305fede7aeefc78... reportFloatingKvs] somewhere in the code that typechecks data family instances (e.g., [http://git.haskell.org/ghc.git/blob/d774b4e2de4f07d2432b67010305fede7aeefc78... 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13985#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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 (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 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13985#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3872 * related: #13738 => #13738, #14131 Comment: 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13985#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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
#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: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | polykinds/T13985 Blocked By: | Blocking: Related Tickets: #13738, #14131 | Differential Rev(s): Phab:D3872 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * testcase: => polykinds/T13985 * resolution: => fixed * milestone: => 8.4.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13985#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC