Opened 3 weeks ago
Last modified 8 days ago
#14498 new bug
GHC internal error: "not in scope during TC but it passed the renamer"
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.2.1 |
Keywords: | PatternSynonyms | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #14288 | Differential Rev(s): | |
Wiki Page: |
Description
{-# 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>
Change History (15)
comment:1 Changed 3 weeks ago by
comment:2 Changed 3 weeks ago by
Component: | Compiler → Compiler (Type checker) |
---|---|
Keywords: | PatternSynonyms added |
Related Tickets: | → #14288 |
Type of failure: | None/Unknown → Compile-time crash or panic |
comment:3 follow-up: 4 Changed 3 weeks ago by
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.
comment:4 Changed 3 weeks ago by
Replying to simonpj:
Short term: GHC should not crash. Maybe it should just reject the 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 renames 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.
comment:5 Changed 3 weeks ago by
Here's a much simpler way to reproduce the bug, for debugging purposes:
{-# 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)) | ^
comment:6 Changed 3 weeks ago by
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:
{-# 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
?
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 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 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:
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)?
comment:7 Changed 3 weeks ago by
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).
comment:8 follow-up: 9 Changed 13 days ago by
There are two separate things going on here.
- Where are the implicitly-added foralls? Example
f :: forall (a :: j). Int -> forall (b :: k). MyProxy a
This is short forf :: forall {j,k}. forall (a :: j). Int -> forall (b :: k). MyProxy a
That is, implicit foralls are added at the top (only). Theforall b
stays where it is, of course.
- 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? Presumablya
andj
. But the choice to bringk
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. blahFor these, should
b
scope over the body off
? That's the debate in #14288.
For pattern synonyms, the answers may differ.
- 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 forpattern SS :: forall {k'}. forall (t :: k'). () => forall {kk}. forall (a :: kk -> k') (n :: kk). (t ~ a n) => blah
Notice that theforall {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!
comment:9 Changed 11 days ago by
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 simonpj:
- Where are the implicitly-added foralls? Example
pattern SS :: forall (t :: k'). () => forall (a :: kk -> k') (n :: kk). (t ~ a n) => blahThis is short forpattern 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:
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.)
comment:10 follow-up: 11 Changed 10 days ago by
comment:11 Changed 10 days ago by
Replying to 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
!
comment:12 Changed 10 days ago by
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.
comment:13 Changed 10 days ago by
Apologies, 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 :)
comment:14 Changed 10 days ago by
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 :-).
comment:15 Changed 8 days ago by
What about this example:
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.
Hmm. It's clear that
t
andk'
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
andkk
?I think it would make sense for them to scope too, in the same way. Does everyone agree?