[GHC] #13881: Inexplicable error message when using out-of-scope type variable in pattern type signature
#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 | Version: 8.0.1 (Type checker) | 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: -------------------------------------+------------------------------------- This code gives an error on any version of GHC since 7.6: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Bug where data family Sing (a :: k) data instance Sing (z :: [a]) where SNil :: Sing '[] SCons :: Sing x -> Sing xs -> Sing (x ': xs) fl :: forall (l :: [a]). Sing l -> Sing l fl (SNil :: Sing (l :: [y])) = SNil fl (SCons x xs) = SCons x xs }}} {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:16:5: error: • The type variable ‘y’ should be bound by the pattern signature ‘Sing l’ but are actually discarded by a type synonym To fix this, expand the type synonym [Note: I hope to lift this restriction in due course] • In the pattern: SNil :: Sing (l :: [y]) In an equation for ‘fl’: fl (SNil :: Sing (l :: [y])) = SNil | 16 | fl (SNil :: Sing (l :: [y])) = SNil | ^^^^^^^^^^^^^^^^^^^^^^^ }}} I can't wrap my head around the error message, though. It complains about a type synonym discarding `y`, but there are no type variables in this program! The //real// source of the issue, the fact that `y` is out of scope (and should actually be `a`), is obscured. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13881 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 Simon Peyton Jones
#13881: Inexplicable error message when using out-of-scope type variable in pattern type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Poor/confusing | Test Case: error message | typecheck/should_compile/T13881 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => typecheck/should_compile/T13881 Comment: Great diagnosis, as ever. All fixed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13881#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13881: Inexplicable error message when using out-of-scope type variable in pattern type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Poor/confusing | Test Case: error message | typecheck/should_compile/T13881 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: => 8.2.1 Comment: Thanks, Simon! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13881#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13881: Inexplicable error message when using out-of-scope type variable in pattern type signature -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Poor/confusing | Test Case: error message | typecheck/should_compile/T13881 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged in 2755f23919f7429668a933374f2a4ca14a9966b6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13881#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC