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 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 3 weeks 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 3 weeks 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 3 weeks 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 3 weeks ago by RyanGlScott (previous) (diff)

comment:5 Changed 3 weeks 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 3 weeks 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 3 weeks 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 13 days 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 11 days 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 10 days 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 10 days 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 10 days 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 10 days 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 10 days ago by RyanGlScott (previous) (diff)

comment:14 Changed 10 days 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 8 days 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.

Note: See TracTickets for help on using tickets.