#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