#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