[GHC] #9867: PatternSynonyms + ScopedTypeVariables triggers an internal error

[GHC]

#9867: PatternSynonyms + ScopedTypeVariables triggers an internal error
-------------------------------------+-------------------------------------
              Reporter:  antalsz     |            Owner:  cactus
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by cactus):

 Hrm.

 So what's happening here is that when we see

 {{{
 pattern Nil = [] :: [a]

 }}}

 we rename and typecheck `[] :: [a]` as a pattern (like in a function
 definition); this by itself requires `ScopedTypeVariables` (in
 `rnHsBndrSig` I believe), as you can see by trying the following:

 {{{
 {-# LANGUAGE PatternSynonyms #-}
 pattern Nil = [] :: [a]
 }}}

 {{{
 T9867a.hs:2:21:
     Illegal type signature: ‘[a]’
       Perhaps you intended to use ScopedTypeVariables
     In a pattern type-signature
 }}}

 If you do turn on `ScopedTypeVariables`, renaming succeeds and puts an
 unbound type variable in the type signature:

 {{{
 pattern main at main:Main.Nil{d rvh} =
             ghc-prim-0.3.1.0:GHC.Types.[]{(w) d 6m} :: [a{tv awt}]
 }}}

 Then `tcInferPatSynDecl` typechecks this right-hand side, via some
 indirections:

 {{{
 T9867.hs:2:15:
     env2 [(a{tv awt}, Type variable ‘a{tv awt}’ = a{tv aww}[sig:2])]
 T9867.hs:2:9: Skolemising a{tv aww}[sig:2] := a{tv awx}[sk]
 T9867.hs:2:9: writeMetaTyVar a{tv aww}[sig:2] := a{tv awx}[sk]
 }}}

 but by the time we get to `tc_patsyn_finish`, both `a{tv aww}` and `a{tv
 awx}` show up, as two separate types: the pattern type is `[a{tv awx}]`,
 but the pattern definition is `[] :: [a{tv aww}]`, so we end up generating
 the following code for the matcher:

 {{{
 main at main:Main.$mNil{v rws}[gid]
   :: forall (r{tv awy}[sk] :: ghc-prim-0.3.1.0:GHC.Prim.OpenKind{(w) tc
 34g})
              a{tv awx}[sk].
      [a{tv awx}[sk]]
      -> (ghc-prim-0.3.1.0:GHC.Prim.Void#{(w) tc 32L} -> r{tv awy}[sk])
      -> (ghc-prim-0.3.1.0:GHC.Prim.Void#{(w) tc 32L} -> r{tv awy}[sk])
      -> r{tv awy}[sk]
 [GblId, Str=DmdType]
 main at main:Main.$mNil{v rws}
    = /\(@ (r{tv awy}[sk] :: ghc-prim-0.3.1.0:GHC.Prim.OpenKind{(w) tc
 34g})).
      /\(@ a{tv awx}[sk]).
      \ ((scrut_awA{v}[lid] :: [a{tv awx}[sk]]))
        ((cont_awB{v}[lid] :: Void#{(w) tc 32L} -> r{tv awy}[sk]))
        ((fail_awC{v}[lid] :: Void#{(w) tc 32L} -> r{tv awy}[sk]))
        -> case
              scrut_awA{v}
           of {
             ghc-prim-0.3.1.0:GHC.Types.[]{(w) d 6m}{EvBinds{}} :: [a{tv
 aww}[sig:2]]
               -> cont_awB{v} ghc-prim-0.3.1.0:GHC.Prim.void#{(w) v 0l}
             _ -> fail_awC{v} ghc-prim-0.3.1.0:GHC.Prim.void#{(w) v 0l} }
 }}}


 (note how we still have `[a{tv aww}]` in the type annotation of the case
 branch). This is where the error message is coming from.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9867#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler