[GHC] #16188: GHC HEAD-only panic (buildKindCoercion)
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler | Version: 8.7 (Type checker) | 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: -------------------------------------+------------------------------------- The following program compiles without issue on GHC 8.6.3: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind (Type) import Data.Type.Bool (type (&&)) data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: a ~> b) (x :: a) :: b data family Sing :: forall k. k -> Type data instance Sing :: Bool -> Type where SFalse :: Sing False STrue :: Sing True (%&&) :: forall (x :: Bool) (y :: Bool). Sing x -> Sing y -> Sing (x && y) SFalse %&& _ = SFalse STrue %&& a = a data RegExp :: Type -> Type where App :: RegExp t -> RegExp t -> RegExp t data instance Sing :: forall t. RegExp t -> Type where SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2) data ReNotEmptySym0 :: forall t. RegExp t ~> Bool type instance Apply ReNotEmptySym0 r = ReNotEmpty r type family ReNotEmpty (r :: RegExp t) :: Bool where ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2 sReNotEmpty :: forall t (r :: RegExp t). Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool) sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2 blah :: forall (t :: Type) (re :: RegExp t). Sing re -> () blah (SApp sre1 sre2) = case (sReNotEmpty sre1, sReNotEmpty sre2) of (STrue, STrue) -> () }}} However, it panics on GHC HEAD: {{{ $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20190114 for x86_64-unknown-linux): buildKindCoercion Any ReNotEmpty re2_a1hm Bool t_a1hg Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 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 what you get when you compile the program with `-dcore-lint`: {{{ $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs -dcore-lint [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Desugar (before optimization) *** <no location info>: warning: [RHS of ds_d1ur :: (Sing Any, Sing (ReNotEmpty re2_a1hm))] The type of this binder doesn't match the type of its RHS: ds_d1ur Binder's type: (Sing Any, Sing (ReNotEmpty re2_a1hm)) Rhs type: (Sing (Apply ReNotEmptySym0 re1_a1hl), Sing (ReNotEmpty re2_a1hm)) *** Offending Program *** <elided> blah :: forall t (re :: RegExp t). Sing re -> () [LclIdX] blah = \ (@ t_a1hg) (@ (re_a1hh :: RegExp t_a1hg)) (ds_d1uq :: Sing re_a1hh) -> let { ds_d1vi :: R:SingRegExp t_a1hg re_a1hh [LclId] ds_d1vi = ds_d1uq `cast` (D:R:SingRegExp0[0] <t_a1hg>_N <re_a1hh>_N :: Sing re_a1hh ~R# R:SingRegExp t_a1hg re_a1hh) } in case ds_d1vi of wild_00 { SApp @ re1_a1hl @ re2_a1hm co_a1hn sre1_aXI sre2_aXJ -> let { ds_d1ur :: (Sing Any, Sing (ReNotEmpty re2_a1hm)) [LclId] ds_d1ur = (sReNotEmpty @ t_a1hg @ re1_a1hl sre1_aXI, (sReNotEmpty @ t_a1hg @ re2_a1hm sre2_aXJ) `cast` (Sub (Sym (Sing <Bool>_N (Sym (D:R:ApplyRegExpBoolReNotEmptySym0r[0] <t_a1hg>_N <re2_a1hm>_N)))_N) :: Sing (Apply ReNotEmptySym0 re2_a1hm) ~R# Sing (ReNotEmpty re2_a1hm))) } in let { fail_d1v2 :: Void# -> () [LclId] fail_d1v2 = \ (ds_d1v3 [OS=OneShot] :: Void#) -> patError @ 'LiftedRep @ () "Bug.hs:(47,5)-(48,26)|case"# } in case ds_d1ur of wild_00 { (ds_d1uY, ds_d1uZ) -> let { ds_d1v0 :: R:SingBool Any [LclId] ds_d1v0 = ds_d1uY `cast` (D:R:SingBool0[0] <Any>_N :: Sing Any ~R# R:SingBool Any) } in case ds_d1v0 of wild_00 { __DEFAULT -> fail_d1v2 void#; STrue co_a1hA -> let { ds_d1v1 :: R:SingBool Any [LclId] ds_d1v1 = ds_d1uZ `cast` (D:R:SingBool0[0] <Any>_N :: Sing Any ~R# R:SingBool Any) } in case ds_d1v1 of wild_00 { __DEFAULT -> fail_d1v2 void#; STrue co_a1hD -> () } } } } }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 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 simonpj): Good catch. The culprit is here {{{ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 = case ev of ... CtWanted { ctev_dest = dest } -> do { traceTcS "canTCAppOk" (ppr bndrs $$ ppr (take 20 tc_roles) $$ ppr tys1 $$ ppr tys2) ; cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2 ; setWantedEq dest (mkTyConAppCo role tc cos) } ... where loc = ctEvLoc ev role = eqRelRole eq_rel tc_roles = tyConRolesX role tc -- the following makes a better distinction between "kind" and "type" -- in error messages bndrs = tyConBinders tc is_kinds = map isNamedTyConBinder bndrs is_viss = map isVisibleTyConBinder bndrs kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds vis_xforms = map (\is_vis -> if is_vis then id else flip updateCtLocOrigin toInvisibleOrigin) is_viss -- zipWith3 (.) composes its first two arguments and applies it to the third new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc) }}} The equality we are solving is somthing like {{{ [WD] hole{co_a1hC} {0}:: (Sing @Bool (Apply @(RegExp t_a1hn[sk:1]) @Bool (ReNotEmptySym0 @t_a1hn[sk:1]) re1_a1hs[ssk:2]) :: *) GHC.Prim.~# (Sing @Bool a_a1hg[tau:2] :: *) }}} Turns out that for `Sing`, * its `tyConBinders` is `[]` * so `bndrs` is `[]` * so `new_locs` is `[]` * so `cos` is `[]` and we make a coercion `Refl Sing`,ignoring the arguments to `Sing`!! Utterly bogus. The silent assumption of this code is that in `T ty1 .. tyn` then the `tyConBinders` of `T` has length at least `n`. But that's not true for this data family; and in any case it might not be true of `K (*->*->*) Int Bool Char` where `K :: forall k. * -> k`; the number of of args depends on how you instantiate it. The only comment on this code is that it makes a "better distinction between kind and type", and I have no clue how it works. Moreover, it looks terribly smelly: there's a `zipWith3` followed by a `zipWith4M`. We can't ''really'' have seven things we want to zip!! Moreover the `zipWith3` is zipping two lists both constructed by `map`; and the arguments of those maps are ... more maps ... over the same thing, namely `bndrs`. Lots of huff and puff to do very little. Richard: all this comes from {{{ commit fb752133f45f01b27240d7cc6bce2063a015e51b Author: Richard Eisenberg <rae@cs.brynmawr.edu> Date: Tue Jul 18 14:30:40 2017 -0400 Track visibility in TypeEqOrigin }}} Could you possibly fix the bug, perhaps en route cleaning up the code and adding a Note with a concrete example to explain what is going on? Thanks! It might also be wise to ASSERT that that `cos` has the same length as `tys1` and `tys2`, which themselves should have the same length. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: (none) => goldfire -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 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: #16204 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #16204 Comment: #16204 is possibly related. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 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: #16204 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): It's unclear to me if this is the same issue or not, but in this slightly modified version of the original program: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wincomplete-patterns #-} module Bug where import Data.Kind (Type) import Data.Type.Bool (type (&&)) import Data.Type.Equality ((:~:)(..)) data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: a ~> b) (x :: a) :: b data family Sing :: forall k. k -> Type data instance Sing :: Bool -> Type where SFalse :: Sing False STrue :: Sing True (%&&) :: forall (x :: Bool) (y :: Bool). Sing x -> Sing y -> Sing (x && y) SFalse %&& _ = SFalse STrue %&& a = a data RegExp :: Type -> Type where App :: RegExp t -> RegExp t -> RegExp t data instance Sing :: forall t. RegExp t -> Type where SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2) data ReNotEmptySym0 :: forall t. RegExp t ~> Bool type instance Apply ReNotEmptySym0 r = ReNotEmpty r type family ReNotEmpty (r :: RegExp t) :: Bool where ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2 sReNotEmpty :: forall t (r :: RegExp t). Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool) sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2 blah :: forall (t :: Type) (re :: RegExp t). Sing re -> (ReNotEmpty re :~: True) -> () blah (SApp sre1 sre2) Refl = case (sReNotEmpty sre1, sReNotEmpty sre2) of (STrue, STrue) -> () }}} You actually get different pattern-match coverage checker warnings on GHC 8.6 and HEAD! GHC 8.6 compiles with no warnings, whereas on GHC HEAD you get: {{{ $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:49:5: warning: [-Wincomplete-patterns] Pattern match(es) are non-exhaustive In a case alternative: Patterns not matched: (SFalse, _) | 49 | = case (sReNotEmpty sre1, sReNotEmpty sre2) of | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20190114 for x86_64-unknown-linux): buildKindCoercion Any ReNotEmpty re2_a1mg Bool t_a1ma Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable pprPanic, called at compiler/types/Coercion.hs:2427:9 in ghc:Coercion }}} It could just be that the types have become so screwed up (due to the explanation in comment:2) that the coverage checker becomes confused, but I thought this was worth pointing out nonetheless. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 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: #16204, #16225 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #16204 => #16204, #16225 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: patch Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 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: #16204, #16225 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/207 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => https://gitlab.haskell.org/ghc/ghc/merge_requests/207 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_compile/T16188 Blocked By: | Blocking: Related Tickets: #16204, #16225 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/207 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => merge * testcase: => typecheck/should_compile/T16188 Comment: Landed in [https://gitlab.haskell.org/ghc/ghc/commit/4a4ae70f09009c5d32696445a06eacb273... 4a4ae70f09009c5d32696445a06eacb273f364b5]. Please merge this into 8.8. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#16188: GHC HEAD-only panic (buildKindCoercion) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.7 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_compile/T16188 Blocked By: | Blocking: Related Tickets: #16204, #16225 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/207 -------------------------------------+------------------------------------- Comment (by Marge Bot <ben+marge-bot@…>): In [changeset:"4a4ae70f09009c5d32696445a06eacb273f364b5/ghc" 4a4ae70/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="4a4ae70f09009c5d32696445a06eacb273f364b5" Fix #16188 There was an awful lot of zipping going on in canDecomposableTyConAppOK, and one of the lists being zipped was too short, causing the result to be too short. Easily fixed. Also fixes #16204 and #16225 test case: typecheck/should_compile/T16188 typecheck/should_compile/T16204[ab] typecheck/should_fail/T16204c typecheck/should_compile/T16225 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16188#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC