[GHC] #11520: GHC falls into a hole

#11520: GHC falls into a hole -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-} module Play where import GHC.Types hiding (TyCon) data TyCon (a :: k) = TyCon data TypeRep (a :: k) where TypeCon :: forall (a :: k). TyCon a -> TypeRep k -> TypeRep a TypeApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). TypeRep a -> TypeRep b -> TypeRep (a b) class Typeable k => Typeable (a :: k) where typeRep :: TypeRep a data Compose (f :: k1 -> *) (g :: k2 -> k1) (a :: k2) = Compose (f (g a)) composeTyCon :: TyCon Compose composeTyCon = TyCon Fingerprint "Compose" instance (Typeable f, Typeable (g :: k), Typeable k) => Typeable (Compose f g) where typeRep = TypeApp (TypeApp (TypeCon composeTyCon typeRep) typeRep) typeRep instance (Typeable f, Typeable g, Typeable a) => Typeable (Compose f g a) where typeRep = TypeApp (TypeApp (TypeApp (TypeCon composeTyCon typeRep) typeRep) typeRep) typeRep }}} fails with {{{ λ> :load Bug.hs [1 of 1] Compiling Play ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.1.20160122 for x86_64-unknown-linux): fvProv falls into a hole {abet} Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * failure: None/Unknown => Incorrect warning at compile-time @@ -0,0 +1,2 @@ + This non-sense, + New description: This non-sense, {{{#!hs {-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-} module Play where import GHC.Types hiding (TyCon) data TyCon (a :: k) = TyCon data TypeRep (a :: k) where TypeCon :: forall (a :: k). TyCon a -> TypeRep k -> TypeRep a TypeApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). TypeRep a -> TypeRep b -> TypeRep (a b) class Typeable k => Typeable (a :: k) where typeRep :: TypeRep a data Compose (f :: k1 -> *) (g :: k2 -> k1) (a :: k2) = Compose (f (g a)) composeTyCon :: TyCon Compose composeTyCon = TyCon Fingerprint "Compose" instance (Typeable f, Typeable (g :: k), Typeable k) => Typeable (Compose f g) where typeRep = TypeApp (TypeApp (TypeCon composeTyCon typeRep) typeRep) typeRep instance (Typeable f, Typeable g, Typeable a) => Typeable (Compose f g a) where typeRep = TypeApp (TypeApp (TypeApp (TypeCon composeTyCon typeRep) typeRep) typeRep) typeRep }}} fails with {{{ λ> :load Bug.hs [1 of 1] Compiling Play ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.1.20160122 for x86_64-unknown-linux): fvProv falls into a hole {abet} Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole if given incorrect kind signature -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by bgamari: @@ -1,1 +1,2 @@ - This non-sense, + If one provides an incorrect kind signature GHC throws up. For instance, + this non-sense, @@ -11,2 +12,0 @@ - data TyCon (a :: k) = TyCon - @@ -14,1 +13,1 @@ - TypeCon :: forall (a :: k). TyCon a -> TypeRep k -> TypeRep a + TypeCon :: forall (a :: k). String -> TypeRep k -> TypeRep a @@ -25,3 +24,1 @@ - composeTyCon :: TyCon Compose - composeTyCon = TyCon Fingerprint "Compose" - + -- Note how the kind signature on g is incorrect @@ -30,2 +27,1 @@ - typeRep = TypeApp (TypeApp (TypeCon composeTyCon typeRep) typeRep) - typeRep + typeRep = undefined @@ -33,4 +29,0 @@ - instance (Typeable f, Typeable g, Typeable a) => Typeable (Compose f g a) - where - typeRep = TypeApp (TypeApp (TypeApp (TypeCon composeTyCon typeRep) - typeRep) typeRep) typeRep New description: If one provides an incorrect kind signature GHC throws up. For instance, this non-sense, {{{#!hs {-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-} module Play where import GHC.Types hiding (TyCon) data TypeRep (a :: k) where TypeCon :: forall (a :: k). String -> TypeRep k -> TypeRep a TypeApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). TypeRep a -> TypeRep b -> TypeRep (a b) class Typeable k => Typeable (a :: k) where typeRep :: TypeRep a data Compose (f :: k1 -> *) (g :: k2 -> k1) (a :: k2) = Compose (f (g a)) -- Note how the kind signature on g is incorrect instance (Typeable f, Typeable (g :: k), Typeable k) => Typeable (Compose f g) where typeRep = undefined }}} fails with {{{ λ> :load Bug.hs [1 of 1] Compiling Play ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.1.20160122 for x86_64-unknown-linux): fvProv falls into a hole {abet} Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole if given incorrect kind signature -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by bgamari: @@ -12,6 +12,1 @@ - data TypeRep (a :: k) where - TypeCon :: forall (a :: k). String -> TypeRep k -> TypeRep a - TypeApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). - TypeRep a - -> TypeRep b - -> TypeRep (a b) + data TypeRep (a :: k) @@ -28,1 +23,0 @@ - New description: If one provides an incorrect kind signature GHC throws up. For instance, this non-sense, {{{#!hs {-# LANGUAGE RankNTypes, PolyKinds, TypeInType, GADTs, UndecidableSuperClasses #-} module Play where import GHC.Types hiding (TyCon) data TypeRep (a :: k) class Typeable k => Typeable (a :: k) where typeRep :: TypeRep a data Compose (f :: k1 -> *) (g :: k2 -> k1) (a :: k2) = Compose (f (g a)) -- Note how the kind signature on g is incorrect instance (Typeable f, Typeable (g :: k), Typeable k) => Typeable (Compose f g) where typeRep = undefined }}} fails with {{{ λ> :load Bug.hs [1 of 1] Compiling Play ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.1.20160122 for x86_64-unknown-linux): fvProv falls into a hole {abet} Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole if given incorrect kind signature -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): The trouble here is this: * The kind error is indeed found and reported (i.e. collected in the bag of errors in the monad) * But we continue anyway into `checkValidInstance` * The latter calls `fvProv` to check for something like the size of instance * Which fails because the unsolved constraint has left a hole in the type Really we should not even attempt `checkValidInstance` if we fail to kind- check the type. We could use a `checkNoErrs` in `TcHsTye.TcHsClsInstType`. But there are many other uses of `solveEqualities` all of which in principle have the same concern. So I thought about adding `checkNoErrs` to `solveEqualities`. But there I see {{{ -- | Type-check a thing that emits only equality constraints, then -- solve those constraints. Emits errors -- but does not fail -- -- if there is trouble. solveEqualities :: TcM a -> TcM a }}} '''Richard''': why did you want the "...but does not fail..." bit? What goes wrong if it fais on error? In effect it always used to! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole if given incorrect kind signature -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType * priority: normal => highest Comment: Highest prio because I think the fix is easy and an outright crash is bad. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole if given incorrect kind signature -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The `but does not fail` bit is just to accurately describe the function. As usual, failing is fine, but it means you get fewer error messages at a go. In other words, we can just change the behavior. But I much favor just fixing `fvProv` to do something other than panic on a coercion hole, like return an empty list. There are a bunch of these panics on coercion holes where I thought coercion holes should never be seen. But I've learned that erroneous code can make GHC take paths I hadn't considered. So I'll remove all of these panics and replace them with something that won't crash GHC. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole if given incorrect kind signature -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'd like to try wrapping `solveEqualities` in `checkNoErrs`. Yes, we fail more, but let's see if that worsens behaviour. My reasoning: if we take a type signature that has kind errors in it, and proceed onwards with a kind-incorrect type, we are likely to get hard-to- explain knock-on errors down the line. Let's fail faster. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole if given incorrect kind signature
-------------------------------------+-------------------------------------
Reporter: bgamari | Owner:
Type: bug | Status: new
Priority: highest | Milestone: 8.0.1
Component: Compiler (Type | Version: 8.0.1-rc1
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
warning at compile-time | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones

#11520: GHC falls into a hole if given incorrect kind signature -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: merge Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: warning at compile-time | polykinds/T11520 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge * testcase: => polykinds/T11520 Comment: Ha! That worked. One fix closes four tickets. Merge to 8.0 branch. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11520: GHC falls into a hole if given incorrect kind signature -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: closed Priority: highest | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: warning at compile-time | polykinds/T11520 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged as d0010d749f80b405f991e88e0e953a21d54a744d -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11520#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC