[GHC] #14498: GHC internal error: "not in scope during TC but it passed the renamer"

[GHC]

#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:/compiler/hsSyn/HsTypes.hs#l837
 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:/compiler/typecheck/TcPatSyn.hs#l167
 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