#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