[GHC] #12686: Attempt to promote a value to a type results in an internal error
#12686: Attempt to promote a value to a type results in an internal error -------------------------------------+------------------------------------- Reporter: johnleo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Trying to compile {{{#!hs {-# LANGUAGE GADTs, DataKinds, KindSignatures #-} data Nat = Zero | Succ Nat data Vec :: * -> Nat -> * where Nil :: Vec a 'Zero Cons :: a -> Vec a n -> Vec a ('Succ n) data Bad = Bad { a :: Nat, b :: Vec Int a} }}} results in `error: Not in scope: type variable ‘a’`. Change the last structure to {{{#!hs data Bad = Bad { a :: Nat, b :: Vec Int 'a} }}} and the result is {{{ • GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [r15Y :-> ATcTyCon Bad, r17P :-> APromotionErr RecDataConPE] • In the second argument of ‘Vec’, namely ‘a’ In the type ‘Vec Int a’ In the definition of data constructor ‘Bad’ }}} The user is attempting to promote a value to a type, which cannot be done, but the error message should be more informative. Reproduces in 8.0.1 and 8.1.20160916. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12686 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12686: Attempt to promote a value to a type results in an internal error -------------------------------------+------------------------------------- Reporter: johnleo | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by johnleo: @@ -38,1 +38,1 @@ - Reproduces in 8.0.1 and 8.1.20160916. + Reproduces in 8.0.1 and 8.1.20161010. New description: Trying to compile {{{#!hs {-# LANGUAGE GADTs, DataKinds, KindSignatures #-} data Nat = Zero | Succ Nat data Vec :: * -> Nat -> * where Nil :: Vec a 'Zero Cons :: a -> Vec a n -> Vec a ('Succ n) data Bad = Bad { a :: Nat, b :: Vec Int a} }}} results in `error: Not in scope: type variable ‘a’`. Change the last structure to {{{#!hs data Bad = Bad { a :: Nat, b :: Vec Int 'a} }}} and the result is {{{ • GHC internal error: ‘a’ is not in scope during type checking, but it passed the renamer tcl_env of environment: [r15Y :-> ATcTyCon Bad, r17P :-> APromotionErr RecDataConPE] • In the second argument of ‘Vec’, namely ‘a’ In the type ‘Vec Int a’ In the definition of data constructor ‘Bad’ }}} The user is attempting to promote a value to a type, which cannot be done, but the error message should be more informative. Reproduces in 8.0.1 and 8.1.20161010. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12686#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12686: Attempt to promote a value to a type results in an internal error
-------------------------------------+-------------------------------------
Reporter: johnleo | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#12686: Attempt to promote a value to a type results in an internal error -------------------------------------+------------------------------------- Reporter: johnleo | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | rename/should_fail/T12686 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => rename/should_fail/T12686 * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12686#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12686: Attempt to promote a value to a type results in an internal error
-------------------------------------+-------------------------------------
Reporter: johnleo | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: fixed | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
| rename/should_fail/T12686
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by goldfire):
Replying to [comment:2 Simon Peyton Jones
I chose to squash this in the renamer.
In contrast, I would choose to squash this by implementing dependent types. :) But that would have taken longer. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12686#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC