[GHC] #14498: GHC internal error: "not in scope during TC but it passed the renamer"
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds #-} import Type.Reflection import Data.Kind data Dict c where Dict :: c => Dict c asTypeable :: TypeRep a -> Dict (Typeable a) asTypeable rep = withTypeable rep Dict pattern Typeable :: () => Typeable a => TypeRep a pattern Typeable <- (asTypeable -> Dict) where Typeable = typeRep data N = O | S N type SN = (TypeRep :: N -> Type) pattern SO = (Typeable :: TypeRep (O::N)) pattern SS :: forall (t :: k'). () => forall (a :: kk -> k') (n :: kk). (t ~ a n) => TypeRep n -> TypeRep t pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k')) n) }}} fails with **GHC internal error** {{{ $ ghci -ignore-dot-ghci Bug.hs GHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:31:47: error: • GHC internal error: ‘kk’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [a1Ao :-> Type variable ‘k'’ = k' :: *, a1Aq :-> Type variable ‘t’ = t :: k', a1Hs :-> Type variable ‘a’ = a :: k0, r1v4 :-> Identifier[asTypeable::forall k (a :: k). TypeRep a -> Dict (Typeable a), TopLevelLet]] • In the kind ‘kk -> k'’ In the first argument of ‘TypeRep’, namely ‘(a :: kk -> k')’ In the type ‘TypeRep (a :: kk -> k')’ | 31 | pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k')) n) | ^^ Failed, 0 modules loaded. Prelude> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Hmm. It's clear that `t` and `k'` from the pattern signature should scope over the pattern declaration, by the usual rules (top level forall'd variables from the signature do scope in this way). But what about the existentials, `a` and `kk`? I think it would make sense for them to scope too, in the same way. Does everyone agree? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => PatternSynonyms * failure: None/Unknown => Compile-time crash or panic * component: Compiler => Compiler (Type checker) * related: => #14288 Comment: Yes, `kk` should definitely scope over the pattern synonym body. In fact, the only reason that it doesn't currently is due to #14288 (that is, `ScopedTypeVariables` doesn't pick up variables from nested `forall`s). I suspect fixing #14288 would quite naturally lead to a solution to this bug as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ah, indeed comment:6 of #14288 concerns exactly this point. Short term: GHC should not crash. Maybe it should just reject the program. Slightly longer term: we need to decide if we want to adopt the proposal in commment:15 of #14288. Would this be worth a short GHC proposal? It's certainly a change in the surface language. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Short term: GHC should not crash. Maybe it should just reject the
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:3 simonpj]: program. I agree that until we implement #14288, this shouldn't crash. In fact, given that `kk` doesn't technically scope over the pattern at the moment, I'm surprised that GHC doesn't come up with a fresh `kk` type variable in the pattern `(App (Typeable :: TypeRep (a::kk -> k')) n)` (in fact, if you change it to `(App (Typeable :: TypeRep (a::kk2 -> k')) n)`, then it compiles). This makes me suspect that the code which renamed pattern synonyms is doing something suspicious at the moment.
Slightly longer term: we need to decide if we want to adopt the proposal in commment:15 of #14288. Would this be worth a short GHC proposal? It's certainly a change in the surface language.
To answer your two questions: * Yes. I've been lacking the free time to look at comment:15 of #14288, but perhaps I can take a look this week. * I suppose we could put this forth as a proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here's a much simpler way to reproduce the bug, for debugging purposes: {{{#!hs {-# LANGUAGE PatternSynonyms, PolyKinds, ScopedTypeVariables #-} module Bug where import Data.Proxy pattern Foo :: forall (a :: j). () => forall (b :: k). () => Proxy a pattern Foo = (Proxy :: Proxy (b :: k)) }}} {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:7:37: error: • GHC internal error: ‘k’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [a1vz :-> Type variable ‘j’ = j, a1vB :-> Type variable ‘a’ = a, a1vD :-> Type variable ‘b’ = b] • In the kind ‘k’ In the first argument of ‘Proxy’, namely ‘(b :: k)’ In the type ‘Proxy (b :: k)’ | 7 | pattern Foo = (Proxy :: Proxy (b :: k)) | ^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK, I now know why this particular internal error occurs. To better explain what is going on, it's helpful to look at this program: {{{#!hs {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} data MyProxy (a :: k) = MyProxy f :: forall (a :: j). Int -> forall (b :: k). MyProxy a f _ = MyProxy @_ @b }}} GHC (rightfully) rejects this: {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:9:19: error: Not in scope: type variable ‘b’ | 9 | f _ = MyProxy @_ @b | ^ }}} As one might expect, `b` is not brought into scope in the body of `f`—both in the current rules that GHC abides by, as well as in the proposed rules in #14288—since `b`'s quantification site is separated from the outermost `forall` by a visible argument. Now, what about this version of `f`? {{{#!hs f :: forall (a :: j). Int -> forall (b :: k). MyProxy a f _ = MyProxy @k @_ }}} GHC also rejects this, but this time it's a type error instead of a renamer error: {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:9:7: error: • Couldn't match type ‘k’ with ‘j’ ‘k’ is a rigid type variable bound by the type signature for: f :: forall j k (a :: j). Int -> forall (b :: k). MyProxy a at Bug.hs:8:1-55 ‘j’ is a rigid type variable bound by the type signature for: f :: forall j k (a :: j). Int -> forall (b :: k). MyProxy a at Bug.hs:8:1-55 Expected type: MyProxy a Actual type: MyProxy a • In the expression: MyProxy @k @_ In an equation for ‘f’: f _ = MyProxy @k @_ • Relevant bindings include f :: Int -> forall (b :: k). MyProxy a (bound at Bug.hs:9:1) | 9 | f _ = MyProxy @k @_ | ^^^^^^^^^^^^^ }}} This time, `k` passes the renamer, indicating that `k` is in fact brought into scope over the body of `f`! Why is `k` treated differently from `b`? As it turns out, it's due to the fact that `k` is implicitly quantified. Implicitly quantified type variables are always put at the front of function type signatures, as `-fprint-explicit-foralls` reveals: {{{ $ ghci -fprint-explicit-foralls -XPolyKinds -XRankNTypes GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci λ> data MyProxy (a :: k) = MyProxy λ> f :: forall (a :: j). Int -> forall (b :: k). MyProxy a; f = undefined λ> :type +v f f :: forall j k (a :: j). Int -> forall (b :: k). MyProxy a }}} As a result, nested, implicitly quantified type variables are always brought into scope over the bodies of //functions//. See [http://git.haskell.org/ghc.git/blob/abdb5559b74af003a6d85f32695c034ff739f508... hsWcScopedTvs and hsScopedTvs] for the code which is responsible for this behavior in the renamer. I put "//functions//" in italics since something different happens for pattern synonyms. Functions, when being typechecked, will bring all implicitly quantified type variables (nested or not) into scope, so you get a proper type error when typechecking the second iteration of `f`. Pattern synonyms, however, only bring the //outermost// implicitly quantified type variables into scope when being typechecked. (See [http://git.haskell.org/ghc.git/blob/abdb5559b74af003a6d85f32695c034ff739f508... this code in TcPatSyn].) As a result, there's a discrepancy between the treatment of pattern synonym signature type variables in the renamer (i.e., `hsScopedTvs`) and in the typechecker (the code in `TcPatSyn`), leading to the internal error reported above. Now that we've identified the cause of the issue, a question remains of how to fix it. I believe `TcPatSyn`'s strategy of only bringing the outermost implicitly quantified type variables into scope is the right one, and would think that adopting the same approach in the renamer (in `hsScopedTvs`) would be the right call. Even better, this wouldn't depend on a fix for #14288. There is a downside to this approach, however: there would be some obscure GHC programs that typecheck today that wouldn't after this change. For instance, this currently typechecks: {{{#!hs g :: forall (a :: j). Int -> forall (b :: k). MyProxy b g _ = MyProxy @k }}} But wouldn't after this proposed change, as `k` would no longer be in scope over the body of `g`. Is this an acceptable breakage? Or should we wait until a full-blown fix for #14288 is available (and put forth the fact that `g` would no longer typecheck as a downside in the GHC proposal accompanying #14288)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I suppose we wouldn't have to break anything for now if we went with another option: create a separate copy `hsScopedTvs` intended only for use with pattern synonyms and only apply the fix to that copy for now. That way, `g` would still continue to compile, as it would use the old codepath. Of course, we wouldn't want to maintain this `hsScopedTvs` split forever, but we can merge them back together when #14288 is implemented (where we have the liberty of changing the semantics of existing programs). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): There are two separate things going on here. 1. Where are the implicitly-added foralls? Example {{{ f :: forall (a :: j). Int -> forall (b :: k). MyProxy a }}} This is short for {{{ f :: forall {j,k}. forall (a :: j). Int -> forall (b :: k). MyProxy a }}} That is, implicit foralls are added at the top (only). The `forall b` stays where it is, of course. 2. What type variables are lexically scoped? Once we have {{{ f :: forall {j,k}. forall (a :: j). Int -> forall (b :: k). MyProxy a }}} which variables are in scope? Presumably `a` and `j`. But the choice to bring `k` into scope is less obvious. Apparently it is. Arguably it should not be. But what about {{{ f2 :: forall a. forall b. blah f3 :: forall a. Ord a => forall b. blah }}} For these, should `b` scope over the body of `f`? That's the debate in #14288. For pattern synonyms, the answers may differ. 1. Where are the implicitly-added foralls? Example {{{ pattern SS :: forall (t :: k'). () => forall (a :: kk -> k') (n :: kk). (t ~ a n) => blah }}} This is short for {{{ pattern SS :: forall {k'}. forall (t :: k'). () => forall {kk}. forall (a :: kk -> k') (n :: kk). (t ~ a n) => blah }}} Notice that the `forall {kk}` is nested: `kk` is existential according to our rules. This is annoying. I'm not arguing for a particular outcome, just pointing out that there are two issues, best discussed separately. Let's not discuss implementation until we have a design! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): To be clear here: I'm not proposing to change anything regarding the rules for ordinary functions (I'll save that for #14288, which will require a GHC proposal). I'm only proposing to change the rules for pattern synonyms, since (1) pattern synonyms are a more experimental feature, and (2) the current rules governing them are clearly broken, as this ticket demonstrates. Replying to [comment:8 simonpj]:
1. Where are the implicitly-added foralls? Example {{{ pattern SS :: forall (t :: k'). () => forall (a :: kk -> k') (n :: kk). (t ~ a n) => blah }}} This is short for {{{ pattern SS :: forall {k'}. forall (t :: k'). () => forall {kk}. forall (a :: kk -> k') (n :: kk). (t ~ a n) => blah }}}
Ideally, this would be the case. The typechecker thinks this way, but unfortunately, the renamer does not. It thinks it's this: {{{#!hs pattern SS :: forall {k' kk}. forall (t :: k'). () => forall (a :: kk -> k') (n :: kk). (t ~ a n) => blah }}} That is, the renamer believes everything implicitly quantified is put up front, as as a result, tries to bring `kk` into scope over the body of `SS`, leading to the internal error seen above. I propose to simply not bring `kk` into scope in the renamer. That's all. (I tried implementing this last week, but this turns out to be quite tricky, so I gave up.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See #144548. And I am increasingly dubious about comment:1 and comment:2, which suggest that `kk` should be in scope in the pattern. I can't make sense of that. (The builder is different, as discussed in comment:6 of #14288.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:10 simonpj]:
And I am increasingly dubious about comment:1 and comment:2, which suggest that `kk` should be in scope in the pattern. I can't make sense of that.
I'm not sure how you came to that conclusion. I'm suggesting the opposite—`kk` (from the type signature) should //not// be brought into scope over the body of `SS`! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I'm suggesting the opposite—kk (from the type signature) should not be brought into scope over the body of SS!
Fine. I think so too. But comment:2 says "Yes, kk should definitely scope over the pattern synonym body." I think we are saying "no" to that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Apoligies, I can see why you'd be misled by comment:2. What I meant in comment:2 is "under the design proposed in #14288, `kk` would be brought into scope". But I later realized there was a simpler way forward that didn't require implementing all of #14288, so you can ignore anything I said before that :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Richard claims that `a` (and `kk`) ''should'' be in scope in the pattern declaration. But he didn't have time to explain wny. This comment is to remind him to add that explanation :-). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): What about this example: {{{#!hs data Ex = forall a. C a => MkEx (Proxy a) (F a) class C a where type F a type G a meth :: F a -> G a pattern P :: () => forall a. C a => G a -> Ex pattern P x <- MkEx _ (meth @a -> x) }}} Note that `meth`'s type is ambiguous, and thus we want to specialize it to the existential variable `a`. You might argue that we could bring `a` into scope by matching on the `Proxy` argument -- and you'd be right -- but that's akin to arguing that `forall` should never bring variables into scope in the bodies of definition because you can (almost) always use a pattern signature to bring a type variable into scope. I thus claim that bringing existentials into scope in pattern synonyms is indeed useful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I thus claim that bringing existentials into scope in pattern synonyms is indeed useful.
I disagree. If you try to do this there is nothing to stop you using the existential variable in place where it really isn't in scope. Eg. {{{ pattern Q :: () => forall a. C a => Int -> G a -> (Int,Ex) pattern Q y x <- (y::a, MkEx _ (meth @a -> x)) }}} Now this is a bit stupid because `y::Int`, but it really should not be possible to refer to the existential `a` except underneath the appropriate pattern match. There may be many, possibly nested or possibly peer, existential patterns in a single pattern synonym. Moreover in terms we are content to be stuck with the choice of {{{ f x = case x of { MkEx (_ :: Proxy a) (meth @a -> x) -> ... } }}} Again we can only bring `a` into scope under the match. Maybe we'll add visible (existential) type application in patterns like this {{{ f x = case x of { MkEx @a _ (meth @a -> x) -> ... } }}} in which case that'll work in both cases. No no no. The more I think about this the more I'm convinced that the existentials absolutely should not scope, contrary to my original comment:1. Richard, do you agree? Then we can implement it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, I agree with comment:16 and retract my comment:15. I guess what I really want is [https://github.com/ghc-proposals/ghc-proposals/pull/96 Proposal 96], but that's (rightly) separate from this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer" -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: Resolution: | PatternSynonyms Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14288 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I would be fine with not bringing existentials into scope. It does mean that my original motivation for wanting to bring nested `forall`d variables into scope with `ScopedTypeVariables` would go away (in #14288). Of course, this would have the distinct upside that we could fix #14288 by changing no code and simply adding documentation, which is nice. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14498#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14498: GHC internal error: "not in scope during TC but it passed the renamer"
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.2.1
checker) | Keywords:
Resolution: fixed | PatternSynonyms
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: Compile-time | Test Case:
crash or panic | patsyn/should_fail/T14498
Blocked By: | Blocking:
Related Tickets: #14288 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Changes (by simonpj):
* status: new => closed
* testcase: => patsyn/should_fail/T14498
* resolution: => fixed
Comment:
OK good. Fixed by
{{{
commit f1fe5b4adf6a4094ecc600a28f64f7628903d017
Author: Simon Peyton Jones
participants (1)
-
GHC