[GHC] #9161: Pattern synonyms interact badly with data kinds
#9161: Pattern synonyms interact badly with data kinds -------------------------------------------------+------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler | Version: Keywords: renamer, pattern synonyms, | 7.8.2 data kinds | Operating System: Architecture: Unknown/Multiple | Linux Difficulty: Unknown | Type of failure: Blocked By: | None/Unknown Related Tickets: | Test Case: | Blocking: -------------------------------------------------+------------------------- If we define a pattern `A` and use it as a type: {{{ {-# LANGUAGE PatternSynonyms, DataKinds #-} pattern A = () b :: A b = undefined }}} we get the following error: {{{ Prelude> :load tmp.XDGqzccOAV.hs [1 of 1] Compiling Main ( /tmp/tmp.XDGqzccOAV.hs, interpreted ) /tmp/tmp.XDGqzccOAV.hs:5:9: GHC internal error: ‘A’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [] In the type signature for ‘blah’: blah :: A Failed, modules loaded: none. }}} Also occurs with different arities of `A` (the arity of the pattern and type can differ) and defining it as an operator (enabling the `TypeOperators` pragma). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds -------------------------+------------------------------------------------- Reporter: | Owner: cactus Iceland_jack | Status: new Type: bug | Milestone: Priority: | Version: 7.8.2 lowest | Keywords: renamer, pattern synonyms, Component: | data kinds Compiler | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Linux | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | -------------------------+------------------------------------------------- Changes (by simonpj): * cc: cactus (added) * owner: => cactus Comment: Probably we should not promote pattern synonyms to the type level, so the program should be rejected with "you can't use a pattern synonym as a type, even with !DataKinds" error. Gergo might you look at this? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: cactus Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: renamer, pattern Resolution: | synonyms, data kinds Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: Compile-time | Difficulty: Unknown crash | Blocked By: Test Case: | Related Tickets: Blocking: | -------------------------------------+------------------------------------- Changes (by cactus): * failure: None/Unknown => Compile-time crash * component: Compiler => Compiler (Type checker) * os: Linux => Unknown/Multiple Comment: This one is tricky... One would expect in this scenario roughly the same code path as if you write {{{ {-# LANGUAGE DataKinds #-} data TYPE = CON wrongLift :: CON wrongLift = undefined }}} which BTW results in a reasonable error message: {{{ Expected a type, but ‘CON’ has kind ‘TYPE’ In the type signature for ‘wrongLift’: wrongLift :: CON }}} However, since pattern synonyms are internally handled as binds, not `TyClDecl`s, they are not yet in scope during kind checking (which is done by `tcTyClsInstDecls`) - hence the crash. How do we even get to trying to kindcheck them? `OccName.demoteOccName` handles data constructor names and type constructor names the same way, since we don't differentiate between the two there. So I think our best bet would be to have a bespoke internal kind for pattern synonyms, inject pattern synonyms at that kind before doing kind checking, and then barf on types of that kind with a meaningful error message. Simon, does that sound like a good plan of action? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: cactus Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: renamer, pattern Resolution: | synonyms, data kinds Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: Compile-time | Difficulty: Unknown crash | Blocked By: Test Case: | Related Tickets: Blocking: | -------------------------------------+------------------------------------- Comment (by simonpj): Basically yes. I suggest one of two things: * Add pattern synonyms as `AGlobal (AConLike (PatSynCon (panic "...")))`. Apart from the panic, this is exactly how ''imported'' pattern synonyms will appear, and `TcHsType.tcTyVar` will call `wrongThingErr` on it. It would make sense for ''local'' pattern synonmys to behave the same way. The panic won't be looked at because `TcEnv.wrongThingErr` doesn't look at the payload. * Short cut: don't extend the environment. Instead, in the "no in scope during type checking" error, test for `DataName` and instead complain about using a pattern synonym in a type. Better: do this only in the context of `tcTyVar`, by replicating a certain amount of the `tcLookup` code. This is bit of a hack; I'd rather not do it. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: cactus Type: bug | Status: merge Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: renamer, pattern Resolution: | synonyms, data kinds Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: Compile-time | Difficulty: Unknown crash | Blocked By: Test Case: | Related Tickets: Blocking: | -------------------------------------+------------------------------------- Changes (by cactus): * status: new => merge -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: cactus Type: bug | Status: merge Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: renamer, pattern Resolution: | synonyms, data kinds Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: Compile-time | Difficulty: Unknown crash | Blocked By: Test Case: | Related Tickets: Blocking: | -------------------------------------+------------------------------------- Comment (by cactus): Fixed using Simon's approach #1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: cactus
Type: bug | Status: merge
Priority: lowest | Milestone:
Component: Compiler (Type | Version: 7.8.2
checker) | Keywords: renamer, pattern
Resolution: | synonyms, data kinds
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: Compile-time | Difficulty: Unknown
crash | Blocked By:
Test Case: | Related Tickets:
Blocking: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
The actual commit is
{{{
commit aa3166f42361cb605e046f4a063be3f9e1f48015
Author: Dr. ERDI Gergo
---------------------------------------------------------------
aa3166f42361cb605e046f4a063be3f9e1f48015 compiler/typecheck/TcBinds.lhs | 23 ++++++++++++++++------- compiler/typecheck/TcHsType.lhs | 1 - testsuite/tests/patsyn/should_fail/T9161-1.hs | 7 +++++++ testsuite/tests/patsyn/should_fail/T9161-1.stderr | 4 ++++ testsuite/tests/patsyn/should_fail/T9161-2.hs | 9 +++++++++ testsuite/tests/patsyn/should_fail/T9161-2.stderr | 5 +++++ testsuite/tests/patsyn/should_fail/all.T | 2 ++ 7 files changed, 43 insertions(+), 8 deletions(-) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: cactus
Type: bug | Status: merge
Priority: lowest | Milestone:
Component: Compiler (Type | Version: 7.8.2
checker) | Keywords: renamer, pattern
Resolution: | synonyms, data kinds
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: Compile-time | Difficulty: Unknown
crash | Blocked By:
Test Case: | Related Tickets:
Blocking: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#9161: Pattern synonyms interact badly with data kinds -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: cactus Type: bug | Status: merge Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: renamer, pattern Resolution: | synonyms, data kinds Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: Compile-time | Difficulty: Unknown crash | Blocked By: Test Case: | Related Tickets: Blocking: | -------------------------------------+------------------------------------- Comment (by cactus): Thanks for that note, which explains it much better than my original comment. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: cactus Type: bug | Status: closed Priority: lowest | Milestone: 7.8.3 Component: Compiler (Type | Version: 7.8.2 checker) | Keywords: renamer, pattern Resolution: fixed | synonyms, data kinds Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: Compile-time | Difficulty: Unknown crash | Blocked By: Test Case: | Related Tickets: Blocking: | -------------------------------------+------------------------------------- Changes (by thoughtpolice): * status: merge => closed * resolution: => fixed * milestone: => 7.8.3 Comment: This was merged into GHC 7.8 for 7.8.3 (part of fixing #9175). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9161: Pattern synonyms interact badly with data kinds -------------------------------------+------------------------------------- Reporter: | Owner: cactus Iceland_jack | Status: closed Type: bug | Milestone: 7.8.3 Priority: lowest | Version: 7.8.2 Component: Compiler | Keywords: renamer, (Type checker) | PatternSynonyms, data kinds Resolution: fixed | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: Compile- | Related Tickets: time crash | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by cactus): * keywords: renamer, pattern synonyms, data kinds => renamer, PatternSynonyms, data kinds -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9161#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC