#9200: Milner-Mycroft failure at the kind level ----------------------------------------------+---------------------------- Reporter: ekmett | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by simonpj): I'm not quite ready to declare victory. Some technical questions: * See `T1a` and `T4` under (PARGEN). These are unexpected failures. The tricky side condition means that you must declare ''all'' the polymorphism involving `k`, or ''none'', but nothing in between. * What is the rule for non-recursive bindings? Specifically: {{{ data NR f (a::k) = MkNR (f a) }}} Is this accepted (as now), or rejected by the "tricky side condition". If the former that gives an uncomfortable difference between recursive and non-recursive bindings. * I'd like to see a rule written down for closed type families, and a sketch of the accompanying algorithm. And finally, at a non-technical level, I'm not convinced that (PARTIAL) is untenable. * Yes, people using kind polymorphism might need to add some kind signatures, but that would arguably improve their code. * We could issue a warning for one release cycle. * The tricky side condition becomes simple: all kind polymorphism must be declared. * And sometimes kind polymorphism might even trip you up: {{{ foo :: forall f a. f a -> f a foo = ... where g :: f Int -> Int }}} This will, I think, fail. Because `foo`'s signature actually means {{{ foo :: forall k. forall (f:k->*) (a:k). f a -> f a }}} so the `(f Int)` application is ill-kinded. Edward is an example of a high-end kind-polymorphism user. How bad would (PARTIAL) be? Implementation. Re `NonSkolemTv`, I'd hate to pollute `MetaInfo` for such a corner case. We can simply test the side condition at the end, just as the rule suggests. Generating a helpful error message is quite a challenge! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler