#15076: Typed hole with higher-rank kind causes GHC to panic (No skolem info) -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: TypedHoles, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14040, #14880 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): This is another example of #14880 The problem in comment:5 comes because when we kind-check foo's type signature, we generate this: {{{ foo :: forall {xx :: a}. forall (a :: Type) (f :: forall (x::a). Proxy @Type x -> Type) Proxy @(Proxy @a xx -> Type) (f @xx) -> () }}} Note that the `f` in `Proxy f` gets elaborated to `Proxy @.. (f @xx)`; that is `f` is instantiated with a fresh unification variable `xx`. But now we kind-generalise the result and put `xx` at the front. But `xx`'s kind mentions `a` -- disaster. Solution proposed for #14880: do not generalise over `xx`; instead default it to `Any`. So we'd get {{{ foo :: forall {xx :: a}. forall (a :: Type) (f :: forall (x::a). Proxy @Type x -> Type) Proxy @(Proxy @a (Any a) -> Type) (f @(Any a)) -> () }}} which is probably fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15076#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler