#15343: Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here's a smaller example: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind data HEq :: forall j k. j -> k -> Type where HRefl :: HEq a a data Sing :: forall j k (a :: j) (b :: k). HEq a b -> Type where SHRefl :: Sing HRefl elimSing :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (p :: forall (z :: Type) (y :: z). HEq a y -> Type) (r :: HEq a b). Sing r -> p HRefl -> p r elimSing SHRefl pHRefl = pHRefl data WhySym (a :: j) :: forall (y :: z). HEq a y -> Type -- data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type -- The version above does NOT panic hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: HEq a b). Sing r -> WhySym a r hsym singEq = elimSing @j @k @a @b @(WhySym a) @r singEq undefined }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15343#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15343: Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): Simplification: {{{ #!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind elimSing :: forall (p :: forall z. z). p elimSing = undefined data WhySym :: Type -> Type hsym = elimSing @WhySym }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15343#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15343: Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"aedbf7f1c402ecbcb5ff192d5fb4dd6dd4771bf8/ghc" aedbf7f1/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="aedbf7f1c402ecbcb5ff192d5fb4dd6dd4771bf8" Fix decompsePiCos and visible type application Trac #15343 was caused by two things First, in TcHsType.tcHsTypeApp, which deals with the type argment in visible type application, we were failing to call solveLocalEqualities. But the type argument is like a user type signature so it's at least inconsitent not to do so. I thought that would nail it. But it didn't. It turned out that we were ended up calling decomposePiCos on a type looking like this (f |> co) Int where co :: (forall a. ty) ~ (t1 -> t2) Now, 'co' is insoluble, and we'll report that later. But meanwhile we don't want to crash in decomposePiCos. My fix involves keeping track of the type on both sides of the coercion, and ensuring that the outer shape matches before decomposing. I wish there was a simpler way to do this. But I think this one is at least robust. I suppose it is possible that the decomposePiCos fix would have cured the original report, but I'm leaving the one-line tcHsTypeApp fix in too because it just seems more consistent. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15343#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15343: Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: high | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | dependent/should_fail/T15343 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => dependent/should_fail/T15343 Comment: I'd like Richard to check these patches, if he has time, but they are outright bugs and should probably move to the branch -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15343#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler