[GHC] #15787: GHC panic using kind application
#15787: GHC panic using kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple TypeApplications | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Using GHC head at diff [https://phabricator.haskell.org/D5229 Visible kind application D5229] (#12045), bug goes away if you remove `@ob`. {{{#!hs {-# Language RankNTypes #-} {-# Language TypeApplications #-} {-# Language DataKinds #-} {-# Language PolyKinds #-} {-# Language GADTs #-} {-# Language TypeFamilies #-} import Data.Kind class Ríki (ob :: Type) where type Hom :: ob -> ob -> Type data Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where Kl :: k -> Kl_kind @ob (m) k type family UnKl (kl :: Kl_kind m k) = (res :: k) where UnKl (Kl a) = a }}} {{{ $ ghci -ignore-dot-ghci 543_bug.hs GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 543_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181017 for x86_64-unknown-linux): ASSERT failed! Type-correct unfilled coercion hole {co_a1yH} 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/TcHsSyn.hs:1805:99 in ghc:TcHsSyn Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15787> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15787: GHC panic using kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: mnguyen (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15787#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15787: GHC panic using kind application -------------------------------------+------------------------------------- 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: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: mnguyen (removed) * keywords: TypeApplications => TypeInType Comment: Also not My's fault. The following code panics similarly in HEAD: {{{#!hs {-# Language RankNTypes #-} {-# Language TypeApplications #-} {-# Language DataKinds #-} {-# Language PolyKinds #-} {-# Language GADTs #-} {-# Language TypeFamilies #-} import Data.Kind class Ríki (ob :: Type) where type Hom :: ob -> ob -> Type data Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where Kl :: k -> Kl_kind (m :: ob -> ob) k type family UnKl (kl :: Kl_kind m k) = (res :: k) where UnKl (Kl a) = a }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15787#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15787: GHC panic using kind application -------------------------------------+------------------------------------- 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): Phab:D5275 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * differential: => Phab:D5275 Comment: Patch posted. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15787#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15787: GHC panic using kind application -------------------------------------+------------------------------------- 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): Phab:D5275 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"4427315a65b25db22e1754d41b43dd4b782b022f/ghc" 4427315/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="4427315a65b25db22e1754d41b43dd4b782b022f" Fix #15787 by squashing a coercion hole. In type-incorrect code, we can sometimes let a coercion hole make it through the zonker. If this coercion hole then ends up in the environment (e.g., in the type of a data constructor), then it causes trouble later. This patch avoids trouble by substituting the coercion hole for its representative CoVar. Really, any coercion would do, but the CoVar was very handy. test case: polykinds/T15787 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15787#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15787: GHC panic using kind application -------------------------------------+------------------------------------- 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: | polykinds/T15787 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5275 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => polykinds/T15787 Comment: Should be easy to merge this one. If it isn't, no worries, as I think it's only an assertion failure. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15787#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15787: GHC panic using kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.2 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15787 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5275 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: => 8.6.2 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15787#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15787: GHC panic using kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.2 Component: Compiler | Version: 8.6.1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | polykinds/T15787 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5275 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: This was merged for 8.6.2 in 7a439e7b13f350e1ac6163f1bfa60e30924dbeea. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15787#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC