[GHC] #14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 (Type checker) | Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies, | PartialTypeSignatures | Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: #13877 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- (Originally spun off from #13877.) The following program gives a somewhat decent error message in GHC 8.0.1: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind data family Sing (a :: k) data WeirdList :: Type -> Type where WeirdNil :: WeirdList a WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a data instance Sing (z :: WeirdList a) where SWeirdNil :: Sing WeirdNil SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws) elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil elimWeirdList (SWeirdCons (x :: Sing (x :: z)) (xs :: Sing (xs :: WeirdList (WeirdList z)))) pWeirdNil pWeirdCons = pWeirdCons @z @x @xs x xs (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) }}} {{{ $ /opt/ghc/8.0.1/bin/ghci Foo.hs GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Foo.hs, interpreted ) Foo.hs:34:8: error: • Cannot apply expression of type ‘Sing wl -> (forall y. p x0 t3 'WeirdNil) -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p (WeirdList z) t2 xs -> p z t1 ('WeirdCons x xs)) -> p a t0 wl’ to a visible type argument ‘WeirdList z’ • In the sixth argument of ‘pWeirdCons’, namely ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ In the expression: pWeirdCons @z @x @xs x xs (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) In an equation for ‘elimWeirdList’: elimWeirdList (SWeirdCons (x :: Sing (x :: z)) (xs :: Sing (xs :: WeirdList (WeirdList z)))) pWeirdNil pWeirdCons = pWeirdCons @z @x @xs x xs (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) }}} But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees: {{{ $ /opt/ghc/8.0.2/bin/ghci Foo.hs GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Foo.hs, interpreted ) Foo.hs:24:41: error: • Found type wildcard ‘_’ standing for ‘t0’ Where: ‘t0’ is an ambiguous type variable ‘x0’ is an ambiguous type variable To use the inferred type, enable PartialTypeSignatures • In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl • Relevant bindings include elimWeirdList :: Sing wl -> (forall y. p x0 t0 'WeirdNil) -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p (WeirdList z) t1 xs -> p z t2 ('WeirdCons x xs)) -> p a t3 wl (bound at Foo.hs:29:1) Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened) (GHC version 8.0.2 for x86_64-unknown-linux): No skolem info: z_a13X[sk] }}} {{{ $ /opt/ghc/8.2.1/bin/ghci Foo.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Foo.hs, interpreted ) Foo.hs:21:18: error: • The kind of variable ‘wl1’, namely ‘WeirdList a1’, depends on variable ‘a1’ from an inner scope Perhaps bind ‘wl1’ sometime after binding ‘a1’ • In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... Foo.hs:24:41: error: • Found type wildcard ‘_’ standing for ‘w0’ Where: ‘w0’ is an ambiguous type variable ‘x0’ is an ambiguous type variable To use the inferred type, enable PartialTypeSignatures • In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 24 | -> (forall (y :: Type). p _ WeirdNil) | ^ Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened) (GHC version 8.2.1 for x86_64-unknown-linux): No skolem info: z_a1sY[sk:2] 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/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors }}} (The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK I understand the problem. Consider the type signature (abbreviated from the one written) {{{ -- Sing :: forall (a:*). WeirdList a -> * elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -- p @ (WeirdList z) (_ :: WeirdList z) xs -> p _ (WeirdCons x xs)) -> p _ wl }}} I have written ou the explicitly kind application needed in the application `(p _ xs)`. Now remember that a signature with wildcards is like a template imposed on type inference. The `_` wildcards are replaced with unification variables. So it's like this {{{ alpha1 :: kappa1 alpha2 :: kappa2 alpha3 :: kappa3 elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p alpha1 xs -- p @ (WeirdList z) (alpha1 :: WeirdList z) xs -> p alpha2 (WeirdCons x xs)) -> p alpah3 wl }}} These unification variables are at the "top" of the type. Once you see this it is clear that simply kind-checking this type should fail, becuase `alpha` must have kind `WeirdList z`, and `z` is bound by that inner forall. Yikes! This is all happening because we aren't generating an implication constraint when we kind-check a forall. In fact, there are other symptoms of the same problem: see #14066. Let's cure that first, and then come back to this one (which might "just work"). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Another program with a similar structure and error message: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data Proxy a = Proxy data family Sing (a :: k) data SomeSing k where SomeSing :: Sing (a :: k) -> SomeSing k class SingKind k where type Demote k :: Type fromSing :: Sing (a :: k) -> Demote k toSing :: Demote k -> SomeSing k data instance Sing (x :: Proxy k) where SProxy :: forall (a :: k). Sing ('Proxy :: Proxy a) instance SingKind (Proxy k) where type Demote (Proxy k) = Proxy k fromSing SProxy = Proxy toSing Proxy = SomeSing SProxy data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) } instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where type Demote (k1 ~> k2) = Demote k1 -> Demote k2 fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing sFun y) toSing = undefined dapp :: forall (a :: Type) (f :: forall (x :: a). Proxy x ~> Type) (x :: a). Sing f -> Sing x -> f @@ ('Proxy :: Proxy x) dapp f x = case f of SLambda (sF :: _) -> undefined }}} This time, all GHCs from 8.0.1 on give a similar panic: {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:56:28: error: • Found type wildcard ‘_’ standing for ‘Singghc: panic! (the 'impossible' happened) (GHC version 8.2.1 for x86_64-unknown-linux): No skolem info: a1_a1tE[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/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Interestingly, the original program no longer panics on GHC HEAD, but the program in comment:2 still panics, this time with a slightly different panic: {{{ GHCi, version 8.5.20171205: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:56:28: error:ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20171205 for x86_64-unknown-linux): No skolem info: [a1_a1yY[sk:1]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable pprPanic, called at compiler/typecheck/TcErrors.hs:2892:5 in ghc:TcErrors Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} Is it worth adding a regression test for the original program, or should I wait until the program in comment:2 has been fixed as well? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, PartialTypeSignatures Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: (none) => goldfire Comment: By all means add a regression test, thanks. The more the better. Richard is actively working on a "solveEqualities" patch that will (I hope) fix this bug among many others (e.g. #14066) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: goldfire
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type | Version: 8.0.2
checker) | Keywords: TypeInType,
Resolution: | TypeFamilies, PartialTypeSignatures
Operating System: Unknown/Multiple | Architecture:
Type of failure: Compile-time | Unknown/Multiple
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: #13877 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: TypeInType, TypeFamilies, PartialTypeSignatures => TypeInType, TypeFamilies, PartialTypeSignatures, TypedHoles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I regret to report that even after Richard's "solveEqualties" patch #14066, the example in comment:2 yields {{{ T14040.hs:91:28: error:ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180402 for x86_64-unknown-linux): No skolem info: [a1_aWV[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 }}} This arises during the error-report-generation stage. The residual constraint is this {{{ reportUnsolved (after zonking): Free tyvars: (t_a1e3[tau:2] :: Proxy x_a1dP[sk:2]) a_aWV[sk:1] Tidy env: ([ESf6y :-> 1, ESf7a :-> 1, ESfO0 :-> 2, ESgiS :-> 1], [aWV :-> a1_aWV[sk:1], a1dP :-> x_a1dP[sk:2], a1dQ :-> a_a1dQ[sk:2], a1e3 :-> t0_a1e3[tau:2]]) Wanted: WC {wc_impl = Implic { TcLevel = 2 Skolems = (x_a1dP[sk:2] :: a_aWV[sk:1]) a_a1dQ[sk:2] (f_a1dR[sk:2] :: forall (x :: a_a1dQ[sk:2]). Proxy x ~> *) (x_a1dS[sk:2] :: a_a1dQ[sk:2]) No-eqs = True Status = Unsolved Given = Wanted = WC {wc_simple = [D] _ {0}:: Sing t_a1e3[tau:2] -> Sing (Apply (f_a1dR[sk:2] x_a1dP[sk:2]) t_a1e3[tau:2]) (CHoleCan: TypeHole(_))} Binds = EvBindsVar<a2gv> Needed inner = [a2hM :-> co_a2hM, a2hN :-> co_a2hN, a2hO :-> co_a2hO, a2hQ :-> co_a2hQ, a2hR :-> co_a2hR, a2hS :-> co_a2hS, a2i2 :-> $dIP_a2i2] Needed outer = [a2hM :-> co_a2hM, a2hN :-> co_a2hN, a2hO :-> co_a2hO, a2hQ :-> co_a2hQ, a2hR :-> co_a2hR, a2hS :-> co_a2hS] the type signature for: dapp :: forall (x :: a_aWV[sk:1]) a (f :: forall (x :: a). Proxy x ~> *) (x :: a). Sing (f x) -> Sing x -> f x @@ 'Proxy } }}} And indeed you can see that the skolem `a1_aWV` is not bound by any implication. This must be a bug. Richard? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Well I'll be danged—it looks like this no longer panics on GHC HEAD! {{{ $ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180413: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:21:18: error: • Couldn't match type ‘k0’ with ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x. x -> WeirdList x -> *). Sing wl -> (forall y. p k0 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs)) -> p k3 w3 wl at Bug.hs:(21,18)-(28,23) Expected type: Sing wl -> (forall y. p k1 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs)) -> p k3 w3 wl Actual type: Sing wl -> (forall y. p k1 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs)) -> p k3 w3 wl • In the ambiguity check for ‘elimWeirdList’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... Bug.hs:34:8: error: • Cannot apply expression of type ‘Sing wl -> (forall y. p k0 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs)) -> p k3 w3 wl’ to a visible type argument ‘(WeirdList z)’ • In the sixth argument of ‘pWeirdCons’, namely ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ In the expression: pWeirdCons @z @x @xs x xs (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) In an equation for ‘elimWeirdList’: elimWeirdList (SWeirdCons (x :: Sing (x :: z)) (xs :: Sing (xs :: WeirdList (WeirdList z)))) pWeirdNil pWeirdCons = pWeirdCons @z @x @xs x xs (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) | 34 | (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} I'll confirm which commit caused this and add a regression test. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Never mind, I'm an idiot. I was looking at the original program, not the program in comment:2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #13877 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here is a much simpler way to trigger the panic in comment:2: {{{#!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 }}} But it now appears that this bug is of a different nature than the original program. I'll close this ticket in favor of a new one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: partial- crash or panic | sigs/should_fail/T14040a Blocked By: | Blocking: Related Tickets: #13877, #15076 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => partial-sigs/should_fail/T14040a * status: new => closed * resolution: => fixed * related: #13877 => #13877, #15076 * milestone: => 8.6.1 Comment: Closing in favor of #15076. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: fixed | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: partial- crash or panic | sigs/should_fail/T14040a Blocked By: | Blocking: Related Tickets: #13877, #15076 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): There's still something wrong here, in the original program. Even if we write {{{ elimWeirdList x = error "urk" }}} GHC HEAD still complains mysteriously about the type signature {{{ T14040a.hs:21:18: error: • Couldn't match type ‘k0’ with ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: elimWeirdList :: forall a1 (wl :: WeirdList a1) (p :: forall x. x -> WeirdList x -> *). Sing wl -> (forall y. p k0 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p k1 w1 xs -> p k2 w2 ('WeirdCons x xs)) -> p k3 w3 wl at T14040a.hs:(21,18)-(28,23) Expected type: Sing wl -> (forall y. p k1 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs)) -> p k3 w3 wl Actual type: Sing wl -> (forall y. p k1 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p k0 w1 xs -> p k2 w2 ('WeirdCons x xs)) -> p k3 w3 wl • In the ambiguity check for ‘elimWeirdList’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... T14040a.hs:29:1: error: Can't quantify over ‘a’ bound by the partial type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 29 | elimWeirdList x = error "urk" | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ T14040a.hs:29:1: error: Can't quantify over ‘wl’ bound by the partial type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 29 | elimWeirdList x = error "urk" | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ T14040a.hs:29:1: error: Can't quantify over ‘p’ bound by the partial type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 29 | elimWeirdList x = error "urk" | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: partial- crash or panic | sigs/should_fail/T14040a Blocked By: | Blocking: Related Tickets: #13877, #15076 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * owner: goldfire => (none) * resolution: fixed => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: partial- crash or panic | sigs/should_fail/T14040a Blocked By: | Blocking: Related Tickets: #13877, #15076 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): simonpj, isn't it expected that GHC would complain if you implemented `elimWeirdList` as `elimWeirdList x = error "urk"`? After all, `elimWeirdList` contains higher-rank arguments, and trying to instantiate them with `error "urk" :: forall a. a` would require instantiating `a` with a polytype, which is impredicative. Also, it's worth noting that on GHC HEAD, you get one fewer error than you do in comment:12: {{{ GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:37:1: error: Can't quantify over ‘a’ bound by the partial type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 37 | elimWeirdList x = error "urk" | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Bug.hs:37:1: error: Can't quantify over ‘wl’ bound by the partial type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 37 | elimWeirdList x = error "urk" | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Bug.hs:37:1: error: Can't quantify over ‘p’ bound by the partial type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 37 | elimWeirdList x = error "urk" | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: partial- crash or panic | sigs/should_fail/T14040a Blocked By: | Blocking: Related Tickets: #13877, #15076 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The error message has changed once again in GHC HEAD (as of commit 2257a86daa72db382eb927df12a718669d5491f8): {{{ $ inplace/bin/ghc-stage2 --interactive ../Bug.hs GHCi, version 8.7.20181129: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( ../Bug.hs, interpreted ) ../Bug.hs:34:8: error: • Cannot apply expression of type ‘Sing wl0 -> (forall y. p0 w0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p0 w1 xs -> p0 w2 ('WeirdCons x xs)) -> p0 w3 wl0’ to a visible type argument ‘(WeirdList z)’ • In the sixth argument of ‘pWeirdCons’, namely ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’ In the expression: pWeirdCons @z @x @xs x xs (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) In an equation for ‘elimWeirdList’: elimWeirdList (SWeirdCons (x :: Sing (x :: z)) (xs :: Sing (xs :: WeirdList (WeirdList z)))) pWeirdNil pWeirdCons = pWeirdCons @z @x @xs x xs (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) | 34 | (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: partial- crash or panic | sigs/should_fail/T14040a Blocked By: | Blocking: Related Tickets: #13877, #15076 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): The error message for the `error "urk"` version has changed once again in GHC HEAD. Simon, can you spot-check this to see if this looks correct? (Modulo wildcard pretty-printing, of course.) {{{ $ ~/Software/ghc4/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.7.20190212: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:24:41: error: • Found type wildcard ‘_’ standing for ‘_1 :: x0’ Where: ‘x0’ is an ambiguous type variable ‘_1’ is an ambiguous type variable To use the inferred type, enable PartialTypeSignatures • In the first argument of ‘p’, namely ‘_’ In the type ‘Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl’ In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 24 | -> (forall (y :: Type). p _ WeirdNil) | ^ Bug.hs:26:44: error: • Found type wildcard ‘_’ standing for ‘GHC.Types.Any :: WeirdList z’ Where: ‘z’ is a rigid type variable bound by ‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’ at Bug.hs:25:27 To use the inferred type, enable PartialTypeSignatures • In the first argument of ‘p’, namely ‘_’ In the type ‘Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl’ In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 26 | Sing x -> Sing xs -> p _ xs | ^ Bug.hs:27:24: error: • Found type wildcard ‘_’ standing for ‘GHC.Types.Any :: z’ Where: ‘z’ is a rigid type variable bound by ‘forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)’ at Bug.hs:25:27 To use the inferred type, enable PartialTypeSignatures • In the first argument of ‘p’, namely ‘_’ In the type ‘Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl’ In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 27 | -> p _ (WeirdCons x xs)) | ^ Bug.hs:28:20: error: • Found type wildcard ‘_’ standing for ‘_0 :: a’ Where: ‘a’ is an ambiguous type variable ‘_0’ is an ambiguous type variable To use the inferred type, enable PartialTypeSignatures • In the first argument of ‘p’, namely ‘_’ In the type ‘Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl’ In the type signature: elimWeirdList :: forall (a :: Type) (wl :: WeirdList a) (p :: forall (x :: Type). x -> WeirdList x -> Type). Sing wl -> (forall (y :: Type). p _ WeirdNil) -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs)) -> p _ wl | 28 | -> p _ wl | ^ Bug.hs:37:19: error: • Cannot instantiate unification variable ‘a0’ with a type involving foralls: (forall y. p _1 'WeirdNil) -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p GHC.Types.Any xs -> p GHC.Types.Any ('WeirdCons x xs)) -> p _0 wl GHC doesn't yet support impredicative polymorphism • In the expression: error "urk" In an equation for ‘elimWeirdList’: elimWeirdList x = error "urk" • Relevant bindings include x :: Sing wl (bound at Bug.hs:37:15) elimWeirdList :: Sing wl -> (forall y. p _1 'WeirdNil) -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p GHC.Types.Any xs -> p GHC.Types.Any ('WeirdCons x xs)) -> p _0 wl (bound at Bug.hs:37:1) | 37 | elimWeirdList x = error "urk" | ^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14040: Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2] -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: TypeInType, Resolution: | TypeFamilies, | PartialTypeSignatures, TypedHoles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: partial- crash or panic | sigs/should_fail/T14040a Blocked By: | Blocking: Related Tickets: #13877, #15076 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): The original program now reports just one error {{{ T14040.hs:41:8: error: • Cannot apply expression of type ‘Sing wl0 -> (forall y. p0 _0 'WeirdNil) -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)). Sing x -> Sing xs -> p0 _1 xs -> p0 _2 ('WeirdCons x xs)) -> p0 _3 wl0’ to a visible type argument ‘(WeirdList z)’ }}} And that's right: the signature for `elimWierdList` is a partial signature, so we do ''inference'' on the definition. So at the recursive call to `elimWierdList`, the function is a monotype, and can't be applied to type arguments. However, for the `elimWierdList x = error "urk"` version I get {{{ WARNING: file compiler/types/TyCoRep.hs, line 3033 in_scope InScope {a_a10j wl_a10k p_a10l} tenv [aX1 :-> a_a10j[tyv:1], aX2 :-> wl_a10k[tyv:1], aX4 :-> p_a10l[tyv:1]] cenv [] tys [Sing wl_aX2[tyv:1] -> (forall y. p_aX4[tyv:1] __aZo[tau:2] 'WeirdNil) -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)). Sing x -> Sing xs -> p_aX4[tyv:1] __aZL[tau:2] xs -> p_aX4[tyv:1] __aZP[tau:2] ('WeirdCons x xs)) -> p_aX4[tyv:1] __aZW[tau:1] wl_aX2[tyv:1]] cos [] needInScope {z_aX6[sk:2], x_aZm[tau:2], __aZo[tau:2], __aZL[tau:2], __aZP[tau:2], __aZW[tau:1]} Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1211:29 in ghc:Outputable warnPprTrace, called at compiler/types/TyCoRep.hs:3027:6 in ghc:TyCoRep checkValidSubst, called at compiler/types/TyCoRep.hs:3050:29 in ghc:TyCoRep substTy, called at compiler/typecheck/TcSigs.hs:507:49 in ghc:TcSigs ghc-stage1: panic! (the 'impossible' happened) (GHC version 8.7.20190215 for x86_64-unknown-linux): ASSERT failed! 2 0 __a23h[tau:0] Any Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1159:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1220:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcMType.hs:805:54 in ghc:TcMType Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug }}} So there is still stuff wrong here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14040#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC