[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

#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

#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

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