[GHC] #15076: Typed hole causes GHC to panic (No skolem info)

newer
[GHC] #15825: Core Lint error from...

GHC

22 Apr 2018 22 Apr '18

10:18 a.m.

#15076: Typed hole causes GHC to panic (No skolem info) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: TypedHoles, | Operating System: Unknown/Multiple TypeInType | Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: #14040 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Spun out from https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2, which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy newtype S (f :: k1 -> k2) = MkS (forall t. Proxy t -> Proxy (f t)) foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). S f -> () foo (MkS (sF :: _)) = () }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180420: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:15:17: error:ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180420 for x86_64-unknown-linux): No skolem info: [a1_a1Cb[sk:1]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Show replies by date

GHC

22 Apr 22 Apr

10:22 a.m.

#15076: Typed hole causes GHC to panic (No skolem info) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: TypedHoles, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14040 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Echoing simonpj's comments in https://ghc.haskell.org/trac/ghc/ticket/14040#comment:7, we can see from `-ddump-tc-trace` that: {{{ reportUnsolved (after zonking): Free tyvars: (t_a1TL[tau:2] :: Proxy x_a1TC[sk:2]) a_a1Sj[sk:1] Tidy env: ([ESf9Q :-> 1, ESfa3 :-> 1, ESfWb :-> 2, ESgJA :-> 1], [a1Sj :-> a1_a1Sj[sk:1], a1TC :-> x_a1TC[sk:2], a1TD :-> a_a1TD[sk:2], a1TL :-> t0_a1TL[tau:2]]) Wanted: WC {wc_impl = Implic { TcLevel = 2 Skolems = (x_a1TC[sk:2] :: a_a1Sj[sk:1]) a_a1TD[sk:2] (f_a1TE[sk:2] :: forall (x :: a_a1TD[sk:2]). Proxy x -> *) No-eqs = True Status = Unsolved Given = Wanted = WC {wc_simple = [D] _ {0}:: Proxy t_a1TL[tau:2] -> Proxy (f_a1TE[sk:2] x_a1TC[sk:2] t_a1TL[tau:2]) (CHoleCan: TypeHole(_))} Binds = EvBindsVar<a1TM> Needed inner = [] Needed outer = [] the type signature for: foo :: forall (x :: a_a1Sj[sk:1]) a (f :: forall (x :: a). Proxy x -> *). S (f x) -> () }} ... Adding error:ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180420 for x86_64-unknown-linux): No skolem info: [a1_a1Sj[sk:1]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors }}} Here, `a1_a1Sj` is not bound by any implication. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

10:29 a.m.

...

Spun out from https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2, which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward:

{{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} module Bug where

import Data.Kind import Data.Proxy

newtype S (f :: k1 -> k2) = MkS (forall t. Proxy t -> Proxy (f t))

foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). S f -> () foo (MkS (sF :: _)) = () }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180420: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted )

Bug.hs:15:17: error:ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180420 for x86_64-unknown-linux): No skolem info: [a1_a1Cb[sk:1]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors }}}

New description: Spun out from https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2, which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy newtype S (f :: k1 -> k2) = MkS (Proxy f) foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). S f -> () foo (MkS (sF :: _)) = () }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180420: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:14:17: error:ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180420 for x86_64-unknown-linux): No skolem info: [a_a1Ca[sk:1]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

2:07 p.m.

New subject: [GHC] #15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info) (was: Typed hole causes GHC to panic (No skolem info))

...

Spun out from https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2, which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward:

{{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} module Bug where

import Data.Kind import Data.Proxy

newtype S (f :: k1 -> k2) = MkS (Proxy f)

foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). S f -> () foo (MkS (sF :: _)) = () }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180420: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted )

Bug.hs:14:17: error:ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180420 for x86_64-unknown-linux): No skolem info: [a_a1Ca[sk:1]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors }}}

New description: Spun out from https://ghc.haskell.org/trac/ghc/ticket/14040#comment:2, which was different enough from the original program in #14040 to warrant its own ticket. The following program panics on every version of GHC from 8.0.2 onward: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). Proxy f -> () foo (_ :: _) = () }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:12:11: error:ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180420 for x86_64-unknown-linux): No skolem info: [a_aZo[sk:1]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

2:33 p.m.

New subject: [GHC] #15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info)

GHC

23 Apr 23 Apr

12:20 p.m.

New subject: [GHC] #15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info)

#15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: TypedHoles, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14040, #14880 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): If you don't use a typed hole: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind import Data.Proxy foo :: forall (a :: Type) (f :: forall (x :: a). Proxy x -> Type). Proxy f -> () foo _ = () }}} Then it compiles. However, it fails with a Core Lint error: {{{ $ /opt/ghc/8.4.2/bin/ghc Bug.hs -dcore-lint [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Desugar (after optimization) *** <no location info>: warning: In the type ‘forall (x :: a) a (f :: forall (x :: a). Proxy x -> *). Proxy (f x) -> ()’ @ a_aZi[sk:1] is out of scope *** Offending Program *** foo :: forall (x :: a) a (f :: forall (x :: a). Proxy x -> *). Proxy (f x) -> () [LclIdX] foo = \ (@ (x_a1e5 :: a_aZi[sk:1])) (@ a_a1e6) (@ (f_a1e7 :: forall (x :: a). Proxy x -> *)) _ [Occ=Dead] -> () $trModule :: Module [LclIdX] $trModule = Module (TrNameS "main"#) (TrNameS "Bug"#) *** End of Offense *** <no location info>: error: Compilation had errors }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

26 Apr 26 Apr

11:59 a.m.

New subject: [GHC] #15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info)

#15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: TypedHoles, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14040, #14880 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): This is another example of #14880 The problem in comment:5 comes because when we kind-check foo's type signature, we generate this: {{{ foo :: forall {xx :: a}. forall (a :: Type) (f :: forall (x::a). Proxy @Type x -> Type) Proxy @(Proxy @a xx -> Type) (f @xx) -> () }}} Note that the `f` in `Proxy f` gets elaborated to `Proxy @.. (f @xx)`; that is `f` is instantiated with a fresh unification variable `xx`. But now we kind-generalise the result and put `xx` at the front. But `xx`'s kind mentions `a` -- disaster. Solution proposed for #14880: do not generalise over `xx`; instead default it to `Any`. So we'd get {{{ foo :: forall {xx :: a}. forall (a :: Type) (f :: forall (x::a). Proxy @Type x -> Type) Proxy @(Proxy @a (Any a) -> Type) (f @(Any a)) -> () }}} which is probably fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

31 May 31 May

11:10 a.m.

New subject: [GHC] #15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info)

#15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: TypedHoles, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14040, #14880 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Another example of this bug, discovered in https://github.com/goldfirere/ghc/issues/57 : {{{#!hs {-# LANGUAGE PolyKinds, MultiParamTypeClasses, GADTs, ScopedTypeVariables, TypeOperators #-} {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} module Super where import Data.Proxy import GHC.Prim class (a ~ b) => C a b data SameKind :: k -> k -> * where SK :: SameKind a b bar :: forall (a :: *) (b :: *). C a b => Proxy a -> Proxy b -> () bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

GHC

29 Oct 29 Oct

6:41 a.m.

New subject: [GHC] #15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info)

GHC

12:37 p.m.

New subject: [GHC] #15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info)

GHC

12:38 p.m.

New subject: [GHC] #15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info)

2397

Age (days ago)

2587

Last active (days ago)

List overview

Download

10 comments

1 participants

[GHC] #15076: Typed hole causes GHC to panic (No skolem info)

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)