[GHC] #13881: Inexplicable error message when using out-of-scope type variable in pattern type signature

[GHC]

#13881: Inexplicable error message when using out-of-scope type variable in pattern
type signature
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Poor/confusing    |  Unknown/Multiple
  error message                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I attempted to debug this a bit. I at least know why the error message is
 happening. In an attempt to detect type variables that are manufactured
 out of thin air in pattern signatures, such as this:

 {{{#!hs
 type T a = Int
 f :: Int -> Int
 f (x :: T a) = ...
 }}}

 GHC first collects the tyvars of the pattern signature, then collects the
 //exact// tyvars (read: after type synonym expansion) of the typechecked
 pattern signature, and if any tyvars from the first set aren't in the
 second set, it errors. Seems simple enough.

 Here's what I don't get though. Surprisingly, this variant of the program
 compiles, even with `ScopedTypeVariables`:

 {{{#!hs
 fl :: forall (l :: [a]). Sing l -> Sing l
 fl (SNil :: Sing (song :: [a])) = (SNil :: Sing l) :: Sing song
 fl (SCons x xs)                 = SCons x xs
 }}}

 Here, the pattern signature for `SNil` //binds// the tyvar `song`, and
 type inference figures out that it's equal to `l`. As a result, everything
 works out.

 But in the original variant of the program:

 {{{#!hs
 fl :: forall (l :: [a]). Sing l -> Sing l
 fl (SNil :: Sing (l :: [y])) = SNil
 fl (SCons x xs)              = SCons x xs
 }}}

 Due to `ScopedTypeVariables`, the pattern signature is not binding `l`.
 Therefore, after typechecking the pattern signature `l :: [y]` becomes `l
 :: [a]`, since `a` is the kind variable we used when quantifying `l` in
 the type signature for `fl`. But this presents a problem, because:

 1. The kind vars of the original pattern signature include `y`
 2. The exact kind vars of the typechecked pattern signature do //not//
 include `y` (only `a`)

 Thus, GHC errors.

 I'm still not sure of the best way to inform GHC that `y` isn't bound by a
 type synonym, however...

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