[GHC] #15796: Core Lint error
#15796: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 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: -------------------------------------+------------------------------------- This gives a Core Lint error {{{#!hs {-# Language QuantifiedConstraints #-} {-# Language TypeApplications #-} {-# Language TypeOperators #-} {-# Language PolyKinds #-} {-# Language FlexibleInstances #-} {-# Language DataKinds #-} {-# Language TypeFamilies #-} {-# Language MultiParamTypeClasses #-} {-# Language ConstraintKinds #-} {-# Language UndecidableInstances #-} {-# Language GADTs #-} {-# Options_GHC -dcore-lint #-} import Data.Kind type Cat ob = ob -> ob -> Type class Ríki (obj :: Type) where type (-->) :: Cat obj class Varpi (f :: dom -> cod) newtype (··>) :: Cat (a -> b) where Natu :: Varpi f => (forall xx. f xx --> f' xx) -> (f ··> f') instance Ríki cod => ------------- Ríki (dom -> cod) where type (-->) = (··>) @dom @cod }}} {{{ $ ghci -ignore-dot-ghci 568_bug.hs GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 568_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181017 for x86_64-unknown-linux): Core Lint error <no location info>: warning: In the type ‘(··>)’ Found TcTyCon: ··>[tc] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
:q Leaving GHCi. }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeApplications Comment: This is related to Visible Kind Application, correct? Which is not yet committed to HEAD? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12045 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: mnguyen (added) * related: => #12045 Comment: Yes. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | TypeApplications Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12045 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Yes it is Simon this uses [https://phabricator.haskell.org/D5229 D5229 (Visible kind application)]. Here is another program that triggers a similar error {{{#!hs {-# Language DataKinds #-} {-# Language TypeOperators #-} {-# Language PolyKinds #-} {-# Language GADTs #-} {-# Language TypeFamilies #-} {-# Options_GHC -dcore-lint #-} import qualified GHC.TypeLits as TypeLits import Data.Kind data OP a = Op a type family UnOp (op_a :: OP a) :: a where UnOp (Op a) = a class Ríki (obj :: Type) where type (-->) :: OP obj -> obj -> Type data (<=) :: OP TypeLits.Nat -> TypeLits.Nat -> Type where LessThan :: TypeLits.KnownNat (UnOp op_a) => op_a <= b instance Ríki TypeLits.Nat where type (-->) = (<=) }}} {{{ $ ghci -ignore-dot-ghci 572_bug.hs GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 572_bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.7.20181017 for x86_64-unknown-linux): Core Lint error <no location info>: warning: In the type ‘(<=)’ Found TcTyCon: <=[tc] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error with visible kind application -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * cc: mnguyen (removed) * keywords: TypeApplications => TypeInType * related: #12045 => Comment: Can be triggered without visible kind application: {{{#!hs {-# Language QuantifiedConstraints #-} {-# Language TypeApplications #-} {-# Language TypeOperators #-} {-# Language PolyKinds #-} {-# Language FlexibleInstances #-} {-# Language DataKinds #-} {-# Language TypeFamilies #-} {-# Language MultiParamTypeClasses #-} {-# Language ConstraintKinds #-} {-# Language UndecidableInstances #-} {-# Language GADTs #-} {-# Options_GHC -dcore-lint #-} import Data.Kind type Cat ob = ob -> ob -> Type class Ríki (obj :: Type) where type (-->) :: Cat obj class Varpi (f :: dom -> cod) newtype (··>) :: Cat (a -> b) where Natu :: Varpi f => (forall xx. f xx --> f' xx) -> (f ··> f') instance Ríki cod => ------------- Ríki (dom -> cod) where type (-->) = ((··>) :: Cat (dom -> cod)) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error with invalid newtype declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: | Keywords: TypeFamilies 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 => TypeFamilies * failure: None/Unknown => Compile-time crash or panic * component: Compiler => Compiler (Type checker) * milestone: => 8.8.1 Comment: Even simpler example: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} module Bug where newtype N a where MkN :: Show a => a -> N a type family T a type instance T (N a) = N a }}} {{{ $ /opt/ghc/8.6.1/bin/ghci Bug.hs -dcore-lint GHCi, version 8.6.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.6.1 for x86_64-unknown-linux): Core Lint error <no location info>: warning: In the type ‘N a_a1P7’ Found TcTyCon: N[tc] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/typecheck/FamInst.hs:171:31 in ghc:FamInst }}} The culprit appears to be the invalid `Show a` context in the `MkN` newtype constructor, as removing that makes the Core Lint error go away. Note that this only happens in GHC 8.6.1 and later. In earlier versions of GHC, this simply gives an error message: {{{ $ /opt/ghc/8.4.4/bin/ghc Bug.hs -dcore-lint [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:6:3: error: • A newtype constructor cannot have a context in its type MkN :: forall a. Show a => a -> N a • In the definition of data constructor ‘MkN’ In the newtype declaration for ‘N’ | 6 | MkN :: Show a => a -> N a | ^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error with invalid newtype declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: | Keywords: TypeFamilies 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'm pretty sure I know what's happening: * The newtype declaration is bogus. It kind-checks, but then fails the validity check. * If a declaration fails a validity check, we manufacture a "recovery tycon", which is a `TcTyCon`. See `Note [Recover from validity error]` in TcTyClsDecls. * When we create a type family instance, we (optionally) do a quick core- lint check on it, as there's no other time we ever do so. * Core lint falls over when it sees a `TcTyCon`, which should never make it past the type checker. I don't want to remove this last check. And I don't want to abolish recovery tycons, as they produce nice error messages. Maybe we tell core- lint (in a new parameter) that it's being called in the type checker? Maybe we skip this check if there are errors? Yes, that seems sensible. Patch incoming. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error with invalid newtype declaration
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.8.1
Component: Compiler (Type | Version: 8.6.1
checker) |
Resolution: | Keywords: TypeFamilies
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
#15796: Core Lint error with invalid newtype declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T15796 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => typecheck/should_fail/T15796 Comment: This is easy to merge. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error with invalid newtype declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.2 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T15796 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * milestone: 8.8.1 => 8.6.2 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15796: Core Lint error with invalid newtype declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.2 Component: Compiler (Type | Version: 8.6.1 checker) | Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T15796 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: This was merged for 8.6.2 in 41f0f6c2f571ea05c49f9f6ed64beebdc5a9f9fc. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15796#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC