Opened 6 months ago

Closed 5 months ago

#14498 closed bug (fixed)

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: patsyn/should_fail/T14498
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 (19)

comment:1 Changed 6 months ago 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?

comment:2 Changed 6 months ago by RyanGlScott

Component: CompilerCompiler (Type checker)
Keywords: PatternSynonyms added
Type of failure: None/UnknownCompile-time crash or panic

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 foralls). I suspect fixing #14288 would quite naturally lead to a solution to this bug as well.

comment:3 Changed 6 months ago 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.

comment:4 in reply to:  3 Changed 6 months ago by RyanGlScott

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.
Last edited 6 months ago by RyanGlScott (previous) (diff)

comment:5 Changed 6 months ago by RyanGlScott

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 6 months ago 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:

{-# 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 6 months ago 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).

comment:8 Changed 6 months ago 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.
  1. 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!

comment:9 in reply to:  8 Changed 6 months ago 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 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:

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 Changed 6 months ago 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.)

comment:11 in reply to:  10 Changed 6 months ago by RyanGlScott

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 6 months ago 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.

comment:13 Changed 6 months ago by RyanGlScott

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 :)

Last edited 6 months ago by RyanGlScott (previous) (diff)

comment:14 Changed 6 months ago 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 :-).

comment:15 Changed 6 months ago by goldfire

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.

comment:16 Changed 5 months ago 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.

comment:17 Changed 5 months ago by goldfire

Yes, I agree with comment:16 and retract my comment:15. I guess what I really want is Proposal 96, but that's (rightly) separate from this ticket.

comment:18 Changed 5 months ago by RyanGlScott

I would be fine with not bringing existentials into scope. It does mean that my original motivation for wanting to bring nested foralld 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. :)

comment:19 Changed 5 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: patsyn/should_fail/T14498

OK good. Fixed by

commit f1fe5b4adf6a4094ecc600a28f64f7628903d017
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Mon Dec 18 12:03:33 2017 +0000

    Fix scoping of pattern-synonym existentials
    
    This patch fixes Trac #14998, where we eventually decided that
    the existential type variables of the signature of a pattern
    synonym should not scope over the pattern synonym.
    
    See Note [Pattern synonym existentials do not scope] in TcPatSyn.

Sorry about mis-typing the ticket number in the commit message!

Note: See TracTickets for help on using tickets.