[GHC] #14873: GHC HEAD regression (piResultTy)
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler | Version: 8.5 (Type checker) | Keywords: | 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: -------------------------------------+------------------------------------- (Originally noticed [https://travis- ci.org/goldfirere/singletons/jobs/347945148#L1179 here].) The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind (Type) data family Sing (a :: k) newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 class SingI (a :: k) where sing :: Sing a data ColSym1 :: f a -> a ~> Bool type instance Apply (ColSym1 x) y = Col x y class PColumn (f :: Type -> Type) where type Col (x :: f a) (y :: a) :: Bool class SColumn (f :: Type -> Type) where sCol :: forall (x :: f a) (y :: a). Sing x -> Sing y -> Sing (Col x y :: Bool) instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where sing = SLambda (sCol (sing @_ @x)) }}} {{{ $ /opt/ghc/head/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.5.20180201 for x86_64-unknown-linux): piResultTy k_aZU[tau:1] (a_aW8[sk:1] |> <*>_N) Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: 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 RyanGlScott): * cc: simonpj (added) Comment: This regression was introduced in commit 0a12d92a8f65d374f9317af2759af2b46267ad5c (`Further improvements to well- kinded types`). -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: 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): Urk! Patch coming -- but validation is not complete and I have to go home, so probably Monday. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: 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:"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/14873#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: 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 Comment: OK done. Richard: could you have a look, to check my work? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TypeInType -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 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 goldfire): I think we need these invariants: 1. If `ty <- tc_hs_type ... exp_kind`, then `typeKind ty == exp_kind`. 2. If `(ty, ki) <- tc_infer_hs_type ...`, then `typeKind ty == ki`. 3. If `(ty, ki) <- tc_infer_hs_type ...`, then `zonk ki == ki`. 4. If `(ty, ki) <- tcTyVar ...`, then `typeKind ty == ki`. 5. If `(ty, ki) <- tcTyVar ...`, then `zonk ki == ki`. All of these appear to be true now, except I'm worried about the `tcTyVar` case for `TcTyCon`s -- I ''think'' `TcTyCon` kinds can have unzonked metavariables, if the `TcTyCon` comes from the non-CUSK case in `kcLHsQTyVars`. Do you also think this is possible? If so, we need to zonk the kind and wrap the (knot-tied) type in a reflexive coercion (with `mkNakedCastTy`) to fix its kind. Do you agree? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: => 8.6.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: highest | 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 Richard Eisenberg <rae@…>): In [changeset:"cf67e59a90bcaba657a9f5db3d5defb6289c274f/ghc" cf67e59a/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="cf67e59a90bcaba657a9f5db3d5defb6289c274f" Expand and implement Note [The tcType invariant] Read that note -- it's necessary to make sure that we can always call typeKind without panicking. As discussed on #14873, there were more checks and zonking to do, implemented here. There are no known bugs fixed by this patch, but there are likely unknown ones. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | 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: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge Comment: This ticket just had some documentation needs to sort out, but along the way, I found places where a few zonks were necessary. I see no reason not to merge. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: GHC HEAD regression (piResultTy) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | 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 simonpj): Richard, I'm beginning to wonder if the pain of `Note [The well-kinded type invariant]` is worth the gain. It's all very delicate. Here's a possible alternative 1. Define `tcTypeKind :: TcType -> TcM TcKind` which zonks, if necessary, on the fly. This would be dead easy to write. 2. Call `tcTypeKind` instead of `typeKind` in ... well, in various places. Anywhere in the type checker where un-zonked kinds might be floating about. For (2) there are two difficulties * Which calls, exactly, would need to be in the monad? * Are there any calls that don't have the `TcM` monad conveniently to hand? For example `eqType` calls `typeKind`, so we'd really need a `tcEqType` variant that calls `tcTypeKind`. Advantages: (a) redundant Refls disappear much earlier; this is Good (b) less delicate invariants. What do you think? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: The well-kinded type invariant (in TcType) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | 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: | -------------------------------------+------------------------------------- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: The well-kinded type invariant (in TcType) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | 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 <simonpj@…>): In [changeset:"e24da5edb4709bdb050c8d0676f302d0b87b8446/ghc" e24da5e/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="e24da5edb4709bdb050c8d0676f302d0b87b8446" Better Note [The well-kinded type invariant] c.f. Trac #14873 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: The well-kinded type invariant (in TcType) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | 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 goldfire): I've wondered about this, too. If we had `TcType` separate from `Type`, then we this would be very easy to find. I suppose we could smoke it out: put an `ASSERT` in the `typeKind` case for `TyVarTy` that the tyvar isn't a `TcTyVar`. Do the same with `eqType`. Then we'd catch (almost) all the cases. I wonder what the performance implications would be. (+) We don't have to zonk unnecessarily just to maintain the invariant. (-) When we do zonk, we don't memorialize this in the type -- only in the kind. (-) Is monadic code slower than pure code? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: The well-kinded type invariant (in TcType) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: merge Priority: highest | 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 simonpj): Another thing that came up yesterday: there are some calls to `eqType` where we know for sure the the kinds are the same, so checking the kinds as well is redundant. e.g. the use of `eqType` in `checkExpectedKinds`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: The well-kinded type invariant (in TcType) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | 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: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: goldfire => (none) * status: merge => new Comment: comment:8 merged in 634c07dc2bd9b2be53d707d613df9e7100d543aa. Leaving open due to comment:14. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14873: The well-kinded type invariant (in TcType) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: highest | Milestone: 8.8.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: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.6.1 => 8.8.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14873#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC