[GHC] #15859: Dependent quantification, GHC panic
#15859: Dependent quantification, GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- While exploring [https://gist.github.com/RyanGlScott/ded669b5ae3db1ce38c4b6021f144776 Ryan's gist for term-level] `f :: forall a -> a -> Type`. {{{#!hs {-# Language PolyKinds #-} {-# Language TypeApplications #-} {-# Language ImpredicativeTypes #-} import Data.Kind data A k :: k -> Type f :: KindOf A f a = undefined type KindOf (a :: k) = k a = f @Int }}} gives {{{ $ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot- ghci 630_bug.hs GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 630_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181029 for x86_64-unknown-linux): ASSERT failed! KindOf A forall k -> k -> * k_a1xQ[sk:0] k_a1xQ[sk:0] -> * k_a1xQ[sk:0] [req] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcExpr.hs:1336:94 in ghc:TcExpr Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15859> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15859: Dependent quantification, GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType 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 Iceland_jack): minimized {{{#!hs {-# Language PolyKinds #-} {-# Language TypeApplications #-} {-# Language ImpredicativeTypes #-} import Data.Kind data A k :: k -> Type type KindOf (a :: k) = k a = (undefind :: KindOf A) @Int }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15859#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15859: Dependent quantification, GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType 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 Richard Eisenberg <rae@…>): In [changeset:"72b82343b79365dc74ffafb345dd33499a7fd394/ghc" 72b82343/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="72b82343b79365dc74ffafb345dd33499a7fd394" Fix #15859 by checking, not assuming, an ArgFlag We thought that visible dependent quantification was impossible in terms, but Iceland Jack discovered otherwise in #15859. This fixes an ASSERT failure that arose. test case: dependent/should_fail/T15859 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15859#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15859: Dependent quantification, GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T15859 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => dependent/should_fail/T15859 Comment: No reason not to merge, if we're still working on 8.6. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15859#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15859: Dependent quantification, GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T15859 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: => 8.6.3 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15859#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15859: Dependent quantification, GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T15859 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"5693ddd071033516a1804420a903cb7e3677682b/ghc" 5693ddd0/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="5693ddd071033516a1804420a903cb7e3677682b" Actually add test for #15859. Oops. Forgot to `git add`. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15859#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15859: Dependent quantification, GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T15859 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"0ce66be953becf7c9de3cbea406953306b4db3b1/ghc" 0ce66be9/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="0ce66be953becf7c9de3cbea406953306b4db3b1" Comments adding to the fix for Trac #15859 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15859#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15859: Dependent quantification, GHC panic -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.3 Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | dependent/should_fail/T15859 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged with 2594ea25641e4b27327449d40c5dd2d46d837af1. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15859#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC