[GHC] #15629: "No skolem info" panic (GHC 8.6 only)
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1-beta1 (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: -------------------------------------+------------------------------------- The following program: {{{#!hs {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind import Data.Proxy import GHC.Generics data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: forall k. k -> Type newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } singFun1 :: forall f. (forall t. Sing t -> Sing (Apply f t)) -> Sing f singFun1 f = SLambda f data From1Sym0 :: forall k (f :: k -> Type) (a :: k). f a ~> Rep1 f a data To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where (f :. g) x = Apply f (Apply g x) data (.@#@$$$) :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c) type instance Apply (f .@#@$$$ g) x = (f :. g) x (%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a). Sing f -> Sing g -> Sing x -> Sing ((f :. g) x) (sf %. sg) sx = applySing sf (applySing sg sx) (%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a). Sing f -> Sing g -> Sing (f .@#@$$$ g) sf %.$$$ sg = singFun1 (sf %. sg) f :: forall (m :: Type -> Type) x. Proxy (m x) -> () f _ = () where sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab) sFrom1Fun = undefined sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab) sTo1Fun = undefined sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab) sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun }}} Panics on GHC 8.6: {{{ $ /opt/ghc/8.6.1/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:50:39: error: • Expected kind ‘m z ~> Rep1 m ab1’, but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’ • In the first argument of ‘(.@#@$$$)’, namely ‘(From1Sym0 :: m z ~> Rep1 m z)’ In the first argument of ‘Sing’, namely ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)’ In the type signature: sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab) | 50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Bug.hs:51:20: error:ghc: panic! (the 'impossible' happened) (GHC version 8.6.0.20180823 for x86_64-unknown-linux): No skolem info: [ab_a1UW[sk:1]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors }}} But merely errors on GHC 8.4.3: {{{ $ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:50:39: error: • Expected kind ‘m z ~> Rep1 m ab2’, but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’ • In the first argument of ‘(.@#@$$$)’, namely ‘(From1Sym0 :: m z ~> Rep1 m z)’ In the first argument of ‘Sing’, namely ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)’ In the type signature: sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab) | 50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Bug.hs:51:20: error: • Couldn't match type ‘ab1’ with ‘z1’ because type variable ‘z1’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0) at Bug.hs:50:5-112 Expected type: Sing From1Sym0 Actual type: Sing From1Sym0 • In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’ In the expression: sFrom1Fun %.$$$ sTo1Fun In an equation for ‘sFrom1To1Fun’: sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun • Relevant bindings include sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0) (bound at Bug.hs:51:5) | 51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun | ^^^^^^^^^ Bug.hs:51:36: error: • Couldn't match type ‘ab’ with ‘z1’ because type variable ‘z1’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0) at Bug.hs:50:5-112 Expected type: Sing To1Sym0 Actual type: Sing To1Sym0 • In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’ In the expression: sFrom1Fun %.$$$ sTo1Fun In an equation for ‘sFrom1To1Fun’: sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun • Relevant bindings include sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0) (bound at Bug.hs:51:5) | 51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun | ^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1-beta1 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): Blimey, it looks like this has been fixed on GHC HEAD: {{{ $ /opt/ghc/head/bin/ghci Bug.hs GHCi, version 8.7.20180827: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:50:39: error: • Expected kind ‘m z ~> Rep1 m ab’, but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’ • In the first argument of ‘(.@#@$$$)’, namely ‘(From1Sym0 :: m z ~> Rep1 m z)’ In the first argument of ‘Sing’, namely ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)’ In the type signature: sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab) | 50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Bug.hs:51:20: error: • Couldn't match type ‘z’ with ‘ab’ ‘z’ is a rigid type variable bound by the type signature for: sFrom1To1Fun :: forall z1 ab1. Sing (From1Sym0 .@#@$$$ To1Sym0) at Bug.hs:50:5-112 ‘ab’ is a rigid type variable bound by the type signature for: sFrom1To1Fun :: forall z1 ab1. Sing (From1Sym0 .@#@$$$ To1Sym0) at Bug.hs:50:5-112 Expected type: Sing (From1Sym0 .@#@$$$ To1Sym0) Actual type: Sing (From1Sym0 .@#@$$$ To1Sym0) • In the expression: sFrom1Fun %.$$$ sTo1Fun In an equation for ‘sFrom1To1Fun’: sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun In an equation for ‘f’: f _ = () where sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab) sFrom1Fun = undefined sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab) sTo1Fun = undefined .... • Relevant bindings include sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0) (bound at Bug.hs:51:5) | 51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun | ^^^^^^^^^^^^^^^^^^^^^^^ }}} I'm dying to know what fixed this... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1-beta1 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): Interesting! I'm sure you are bisecting as we speak. It'd be good to add a regression test regardless. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15629: "No skolem info" panic (GHC 8.6 only)
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.6.1-beta1
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):
Found it. It's commit 042df603cbb5a77ec13ccfec2ce7bad2bb940aae:
{{{
From 042df603cbb5a77ec13ccfec2ce7bad2bb940aae Mon Sep 17 00:00:00 2001
From: Richard Eisenberg
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1-beta1 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): Oh my, hand on. Everything should work if the eager unifier does NOTHING. Indeed, I'd love to have a flag `-fno-eager-unifier` which switches off the eager unifier in order to stress the constraint solver. It'd b easy: in `TcUnify.uType`, test the flag and call `uType_defer` immediately if `-fno-eager-unifier` is set. I bet this shows up lots of bugs, so I partly fear to suggest it :-). For this one, does the `No skolem` come back? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1-beta1 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): In a quick hack, I added a `-fno-eager-unifier` flag: {{{#!diff diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 9f0ba57..a2f269d 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -557,6 +557,7 @@ data GeneralFlag | Opt_OptimalApplicativeDo | Opt_VersionMacros | Opt_WholeArchiveHsLibs + | Opt_NoEagerUnifier -- copy all libs into a single folder prior to linking binaries -- this should elivate the excessive command line limit restrictions -- on windows, by only requiring a single -L argument instead of @@ -3017,6 +3018,7 @@ dynamic_flags_deps = [ , make_ord_flag defGhcFlag "dhex-word-literals" (NoArg (setGeneralFlag Opt_HexWordLiterals)) + , make_ord_flag defGhcFlag "ghcversion-file" (hasArg addGhcVersionFile) , make_ord_flag defGhcFlag "main-is" (SepArg setMainIs) , make_ord_flag defGhcFlag "haddock" (NoArg (setGeneralFlag Opt_Haddock)) @@ -4003,7 +4005,8 @@ fFlagsDeps = [ flagSpec "show-warning-groups" Opt_ShowWarnGroups, flagSpec "hide-source-paths" Opt_HideSourcePaths, flagSpec "show-loaded-modules" Opt_ShowLoadedModules, - flagSpec "whole-archive-hs-libs" Opt_WholeArchiveHsLibs + flagSpec "whole-archive-hs-libs" Opt_WholeArchiveHsLibs, + flagSpec "no-eager-unifier" Opt_NoEagerUnifier ] ++ fHoleFlags diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 045132e..fb937b7 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -1348,7 +1348,11 @@ uType_defer t_or_k origin ty1 ty2 -------------- uType t_or_k origin orig_ty1 orig_ty2 - = do { tclvl <- getTcLevel + = do { no_eager <- goptM Opt_NoEagerUnifier + ; if no_eager + then uType_defer t_or_k origin orig_ty1 orig_ty2 + else do + { tclvl <- getTcLevel ; traceTc "u_tys" $ vcat [ text "tclvl" <+> ppr tclvl , sep [ ppr orig_ty1, text "~", ppr orig_ty2] @@ -1357,7 +1361,7 @@ uType t_or_k origin orig_ty1 orig_ty2 ; if isReflCo co then traceTc "u_tys yields no coercion" Outputable.empty else traceTc "u_tys yields coercion:" (ppr co) - ; return co } + ; return co } } where go :: TcType -> TcType -> TcM CoercionN -- The arguments to 'go' are always semantically identical }}} However, the panic does //not// reappear if you compile the original program with `-fno-eager-unifier`. The only differences I could observe were minor variations in error quality. With `-fno-eager-unifier` enabled, you don't see any of the "`‘z’ is a rigid type variable bound by`..." stuff, for instance. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1-beta1 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): OK -- that's good! If the flag stays, it should probably be `-feager- unifier` (on by default) because we have generic `-fnoxxx` machinery. I'm still very suspicious that the Real Bug is not fixed, just somehow hidden by the patch. So I'm a bit reluctant to declare victory and close. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1-beta1 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): For what it's worth, here is a slightly more minimal version of the original program: {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug (f) where import Data.Kind import Data.Proxy data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family F x :: Type -> Type data F1Sym :: forall x a. x ~> F x a data F2Sym :: forall x a. F x a ~> x data Comp :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c) sg :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a). Proxy f -> Proxy g -> Proxy (Comp f g) sg _ _ = Proxy f :: forall (x :: Type). Proxy x -> () f _ = () where g :: forall ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) g = sg Proxy Proxy }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.6.1-beta1 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): Well, I devoted a few mins to trying to see what caused the crash in ghc 8.6, but it doesn't look related to the patch you identify in comment:3. Still, since it is working, I'm disinclined to invest more effort in debugging 8.6! I'll add a regression test and close this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15629: "No skolem info" panic (GHC 8.6 only)
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.6.1-beta1
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
#15629: "No skolem info" panic (GHC 8.6 only) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.6.1-beta1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_fail/T15629 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * testcase: => typecheck/should_fail/T15629 * resolution: => fixed * milestone: 8.6.1 => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15629#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC