Opened 7 months ago
Last modified 2 months ago
#14040 new bug
Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]
Reported by: | RyanGlScott | Owned by: | goldfire |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.0.2 |
Keywords: | TypeInType, TypeFamilies, PartialTypeSignatures | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #13877 | Differential Rev(s): | |
Wiki Page: |
Description
(Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
{-# 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.)
Change History (5)
comment:1 Changed 7 months ago by
comment:2 Changed 4 months ago by
Another program with a similar structure and error message:
{-# 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
comment:3 Changed 2 months ago by
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?
comment:4 Changed 2 months ago by
Owner: | set to goldfire |
---|
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)
OK I understand the problem. Consider the type signature (abbreviated from the one written)
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 thisThese 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 kindWeirdList z
, andz
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").