[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
#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