#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