#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here's a somewhat more minimal example: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Bug where import Data.Coerce newtype Wrap f a = Wrap (f a) class C f where c :: f a instance C f => C (Wrap f) where c = coerce @(forall (a :: k). f a) @(forall (a :: k). C f a) c }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170516: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:15:29: error: • GHC internal error: ‘k’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [a1tN :-> Type variable ‘a’ = a, a1tQ :-> Type variable ‘f’ = f, a1uU :-> Type variable ‘k’ = k] • In the kind ‘k’ In the type ‘(forall (a :: k). f a)’ In the expression: coerce @(forall (a :: k). f a) @(forall (a :: k). C f a) c | 15 | c = coerce @(forall (a :: k). f a) | }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): There are two workarounds that I'm aware of. One is to explicitly quantify the kind variable `k` in the instance declaration: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Coerce import Data.Kind (Type) newtype Wrap f a = Wrap (f a) class C f where c :: f a instance forall k (f :: k -> Type). C f => C (Wrap f) where c = coerce @(forall (a :: k). f a) @(forall (a :: k). C f a) c }}} (This, of course, requires that you turn on `TypeInType`.) The other workaround is to leave off the kind annotations in the instance altogether: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Bug where import Data.Coerce newtype Wrap f a = Wrap (f a) class C f where c :: f a instance C f => C (Wrap f) where c = coerce @(forall a. f a) @(forall a. C f a) c }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #13985 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Oh dear, I think I've been operating under a misconception in trying to debug this issue. I was originally under the impression that when renaming the expression `coerce @(forall (a :: k). f a)`, we would implicitly bind the `k` in the `forall` type (i.e., it would become something like `coerce @(forall k (a :: k). f @k a)`. However, this is decidedly //not// the case --as the [http://git.haskell.org/ghc.git/blob/1cdceb9fa3bc3ad01b2d840caad8e735513e14ed... Haddocks] for `HsAppType` reveal, we use `LHsWcType` for representing a visible type argument, precisely because it can have wildcards but //not// implicit quantification. In light of this, I think that the original program should actually give a `"Not in scope: type variable 'k'"` error. But there's a problem: `bindLHsTyVarBndr` //always// attempts to implicitly bind any free kind variables in `forall`'d type variables' kind signatures. As a result, `k` never gets reported as out-of-scope after renaming (which would be the ideal way to catch this). What is the best way to detect this scenario, then? We could add a `Bool` argument to `bindLHsTyVarBndr` that controls whether it attempts to implicitly bind free kind variables or not. But this feels like a heavy approach, since we'd be tweaking the behavior of a very widely used function in renamer (and causing a lot of replumbing) only to account for `LHsWcType`, something which AFAICT is really only used in one particular place: visible type application. But I'm not aware of a more clever way to address this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Phab:D3873 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3873 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: RyanGlScott Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * owner: (none) => RyanGlScott * differential: Phab:D3873 => Comment: Thanks for the advice! I'll abandon Phab:D3873 and try again, since the approach you recommend is quite different in spirit. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: RyanGlScott Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Ugh. Trying to change anything involving `bindLHsTyVarBndr` is proving to be a massive headache. There are numerous complications here that I'm not sure how to deal with: * Using `rnImplicitBinders` simply won't work in `bindHsQTyVars`. `rnImplicitBinders` expects an `LHsType GhcPs` as an argument, which `bindHsQTyVars` doesn't have. * Even if we did somehow pass an `LHsType GhcPs` to `rnImplicitBndrs` from `bindHsQTyVars`, I'm not convinced it would do the right thing. The problem: the `kv_bndrs` from `bindHsQTyVars` need to be bound using `newTyVarNameRn mb_assoc` (since the `kv_bndrs` might be from an associated class), but `rnImplicitBndrs` does nothing of the sort. * `bindLHsTyVarBndr` performs a validity check ([http://git.haskell.org/ghc.git/blob/7463a95dbe53d789f8f245f26735a7ac74bb6e11... here]) to ensure that a list of tyvar binders is well scoped (i.e., reject something like `forall (a :: k) k.`). But we can only perform this check because `bindLHsTyVarBndrs` keeps track of the kind variables that are implicitly bound so far, one by one, and communicates this information to each call to `bindLHsTyVarBndr` so that it can check if a binder is in the set of implicitly bound kind variables. If we removed `bindLHsTyVarBndr`'s ability to implicitly bind kind variables, I'm not sure how we'd perform this check at all. * Could we move this error check to `rnImplicitBndrs`? Perhaps, but then we'd need to migrate the code which tracks one-by-one all of the implicitly bound kind variables so far. That doesn't sound fun. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is in my area. I'll take a look in due course. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"0257dacf228024d0cc6ba247c707130637a25580/ghc" 0257dacf/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="0257dacf228024d0cc6ba247c707130637a25580" Refactor bindHsQTyVars and friends This work was triggered by Trac #13738, which revealed to me that the code RnTypes.bindHsQTyVars and bindLHsTyVarBndrs was a huge tangled mess -- and outright wrong on occasion as the ticket showed. The big problem was that bindLHsTyVarBndrs (which is invoked at every HsForAll, including nested higher rank ones) was attempting to bind implicit kind variables, which it has absolutely no busineess doing. Imlicit kind quantification is done at the outside only, in fact precisely where we have HsImplicitBndrs or LHsQTyVars (which also has implicit binders). Achieving this move was surprisingly hard, because more and more barnacles had accreted aroud the original mistake. It's much much better now. Summary of changes. Almost all the action is in RnTypes. * Implicit kind variables are bound only by - By bindHsQTyVars, which deals with LHsQTyVars - By rnImplicitBndrs, which deals with HsImplicitBndrs * bindLHsTyVarBndrs, and bindLHsTyVarBndr are radically simplified. They simply does far less, and have lots their forest of incomprehensible accumulating parameters. (To be fair, some of the code in bindLHsTyVarBndrs just moved to bindHsQTyVars, but in much more perspicuous form.) * The code that checks if a variable appears in both a kind and a type (triggering RnTypes.mixedVarsErr) was bizarre. E.g. we had this in RnTypes.extract_hs_tv_bndrs ; check_for_mixed_vars bndr_kvs acc_tvs ; check_for_mixed_vars bndr_kvs body_tvs ; check_for_mixed_vars body_tvs acc_kvs ; check_for_mixed_vars body_kvs acc_tvs ; check_for_mixed_vars locals body_kvs I cleaned all this up; now we check for mixed use at binding sites only. * Checks for "Variable used as a kind before being bound", like data T (a :: k) k = rhs now just show up straightforwardly as "k is not in scope". See Note [Kind variable ordering] * There are some knock-on simplifications in RnSource. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | polykinds/T13738 Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): Ryan encountered a related regression in 8.2.1, reported as #14209. Perhaps comment:17 should be merged. Unfortunately it's not a terribly small patch. What do you think, Simon? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#13738: TypeApplications-related GHC internal error -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: simonpj Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | polykinds/T13738 Blocked By: | Blocking: Related Tickets: #13985 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): FWIW, I didn't notice #14209 in a package in the wild, only when stress- testing different ways of implicitly binding kind variables. And indeed, it doesn have a workaround. Instead of writing this: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} module Bug where data MyProxy k (a :: k) = MyProxy data Foo (z :: MyProxy k (a :: k)) }}} You can write this: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeInType #-} module Bug where data MyProxy k (a :: k) = MyProxy data Foo (z :: MyProxy k a) }}} So I would be OK with not merging that patch. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13738#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler