[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]
#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
#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
participants (1)
-
GHC