[GHC] #14174: GHC panic with TypeInType and type family
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler | Version: 8.2.1 (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: -------------------------------------+------------------------------------- This rather simple type family, {{{#!hs {-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-} module GenWhoops where import GHC.Generics type family GenComp k (x :: k) (y :: k) :: Ordering where GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y }}} produces the following panic: {{{ ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170828 for x86_64-unknown-linux): piResultTy k_a1LK[tau:1] p_a1Lz[sk:1] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type }}} This happens with both GHC 8.2.1 and something very close to HEAD. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.2.1 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 dfeuer): This really should just be an error, I imagine. It's an (accidental) non- linear pattern where the two types have different kinds. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.2.1 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 Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.2.1 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): Here is a simpler way to trigger the same panic {{{ {-# LANGUAGE TypeInType, RankNTypes, KindSignatures, PolyKinds #-} module Foo where data T k (x :: k) = MkT data S x = MkS (T (x Int) x) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.1 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 bgamari): * milestone: 8.2.2 => 8.2.3 Comment: It looks like this won't be fixed in 8.2.2. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.1 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): This might be another occurrence of this bug: {{{#!hs {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ data FunArrow = (:->) | (:~>) class FunType (arr :: FunArrow) where type Fun (k1 :: Type) arr (k2 :: Type) :: Type class FunType arr => AppType (arr :: FunArrow) where type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 type family ElimBool (p :: Bool -> Type) (z :: Bool) (pFalse :: p False) (pTrue :: p True) :: p z where -- Commenting out the line below makes the panic go away ElimBool p z pFalse pTrue = ElimBoolPoly (:->) p z pFalse pTrue type family ElimBoolTyFun (p :: Bool ~> Type) (z :: Bool) (pFalse :: p @@ False) (pTrue :: p @@ True) :: p @@ z where ElimBoolTyFun p z pFalse pTrue = ElimBoolPoly (:~>) p z pFalse pTrue type family ElimBoolPoly (arr :: FunArrow) (p :: (Bool -?> Type) arr) (z :: Bool) (pFalse :: App Bool arr Type p False) (pTrue :: App Bool arr Type p True) :: App Bool arr Type p z where ElimBoolPoly _ _ False pFalse _ = pFalse ElimBoolPoly _ _ True _ pTrue = pTrue }}} {{{ $ /opt/ghc/8.2.1/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.2.1 for x86_64-unknown-linux): piResultTy k0_a1Zd[tau:1] z_aS3[sk:1] Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:948:35 in ghc:Type }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.1 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 <simonpj@…>): In [changeset:"8b36ed129652df07af22b5e2a2e57b1df8cfbbc9/ghc" 8b36ed1/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="8b36ed129652df07af22b5e2a2e57b1df8cfbbc9" Build only well-kinded types in type checker During type inference, we maintain the invariant that every type is well-kinded /without/ zonking; and in particular that typeKind does not fail (as it can for ill-kinded types). But TcHsType.tcInferApps was not guaranteeing this invariant, resulting in Trac #14174 and #14520. This patch fixes it, making things better -- but it does /not/ fix the program in Trac #14174 comment:5, which still crashes. So more work to be done. See Note [Ensure well-kinded types] in TcHsType }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | polykinds/T14174.hs, T14174a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => polykinds/T14174.hs, T14174a Comment: Still open because I need to fix the example in comment:5 (which is `T14174a`). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | polykinds/T14174.hs, T14174a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"0a12d92a8f65d374f9317af2759af2b46267ad5c/ghc" 0a12d92a/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="0a12d92a8f65d374f9317af2759af2b46267ad5c" Further improvements to well-kinded types The typechecker has the invariant that every type should be well-kinded as it stands, without zonking. See Note [The well-kinded type invariant] in TcType. That invariant was not being upheld, which led to Trac #14174. I fixed part of it, but T14174a showed that there was more. This patch finishes the job. * See Note [The tcType invariant] in TcHsType, which articulates an invariant that was very nearly, but not quite, true. One place that falisified it was the HsWildCardTy case of tc_hs_type, so I fixed that. * mkNakedCastTy now makes no attempt to eliminate casts; indeed it cannot lest it break Note [The well-kinded type invariant]. The prior comment suggested that it was crucial for performance but happily it seems not to be. The extra Refls are eliminated by the zonker. * I found I could tidy up TcHsType.instantiateTyN and instantiateTyUntilN by eliminating one of its parameters. That led to a cascade of minor improvements in TcTyClsDecls. Hooray. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | polykinds/T14174.hs, T14174a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => fixed Comment: OK, finally fixed I believe. Hurrah. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | polykinds/T14174.hs, T14174a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"3d252037234ce48f9bdada7d5c9b1d8eba470829/ghc" 3d252037/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="3d252037234ce48f9bdada7d5c9b1d8eba470829" Respect Note [The tcType invariant] I tried to do this with commit 0a12d92a8f65d374f9317af2759af2b46267ad5c Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Wed Dec 13 12:53:26 2017 +0000 Further improvements to well-kinded types The typechecker has the invariant that every type should be well- kinded as it stands, without zonking. See Note [The well-kinded type invariant] in TcType. That invariant was not being upheld, which led to Trac #14174. I fixed part of it, but T14174a showed that there was more. This patch finishes the job. But I didn't get it quite right as Trac #14873 showed. This patch fixes the problem; although I am still a bit unhappy. (See "A worry" in the HsApp case of tc_infer_hs_type.) }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14174: GHC panic with TypeInType and type family -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.2.3 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | polykinds/T14174.hs, T14174a Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"5067b205a8abb5a9f98335d3a929f647c88c0aa2/ghc" 5067b20/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="5067b205a8abb5a9f98335d3a929f647c88c0aa2" Add nakedSubstTy and use it in TcHsType.tcInferApps This was a tricky one. During type checking we maintain TcType: Note [The well-kinded type invariant] That is, types are well-kinded /without/ zonking. But in tcInferApps we were destroying that invariant by calling substTy, which in turn uses smart constructors, which eliminate apparently-redundant Refl casts. This is horribly hard to debug beause they really are Refls and so it "ought" to be OK to discard them. But it isn't, as the above Note describes in some detail. Maybe we should review the invariant? But for now I just followed it, tricky thought it is. This popped up because (for some reason) when I fixed Trac #15343, that exposed this bug by making test polykinds/T14174a fail (in Trac #14174 which indeed has the same origin). So this patch fixes a long standing and very subtle bug. One interesting point: I defined nakedSubstTy in a few lines by using the generic mapType stuff. I note that the "normal" TyCoRep.substTy does /not/ use mapType. But perhaps it should: substTy has lots of $! strict applications in it, and they could all be eliminated just by useing the StrictIdentity monad. And that'd make it much easier to experiment with switching between strict and lazy versions. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14174#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC