#15788: Core Lint error, from visible kind applications -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.1 Resolution: | Keywords: #12045 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is really #15743 in deep disguise. GHC correctly infers `A :: forall {k1} (k :: k1). Type`. We have `MkA :: A @p` (I've changed the variable name). Currently, the kind application branch has a bug that means we don't skip Inferred variables when instantiating. So, the `p` instantiates the `k1`. But, the kind of a data constructor has kind `Type`, while `A @p :: forall (k :: p). Type`. So we instantiate with a metavariable, getting `A @p @alpha`, where `alpha :: p`. Then, we try to generalize, skolemizing `alpha := a`.. Generalization tries putting Inferred things before Specified things, and so we get `forall (a :: p) p. A p a`, which is clearly hogwash. I hope that once my Phab:D5208 patch lands, this will be fixed. Meanwhile, My will fix the forgetting-to-skip-Inferred variables bug. (See point (4) in https://phabricator.haskell.org/D5229#144361 .) Keeping this open, as we should test that it all works in the end. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15788#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler