[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 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