[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

#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

#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

#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