#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 goldfire): By "2) Allow more flexible partial kind signatures", I meant that, under (NEWCUSK), the kind of un-annotated type variables ''can'' unify with lexically-scoped kind variables, allowing the following to type-check: {{{ data Q f (a :: k) where MkQ :: f a -> Q f a -- fails under (PARTIAL) and (PARGEN) -- succeeds under (BASELINE) and (NEWCUSK) }}} If partial type signatures on terms are so useful (and I think they will be), then partial kind signatures, like the one on `Q`, would be, too. Yes, I am agreed with the examples in comment:21. (NEWCUSK) description was already on wiki page, and I have now added rules for closed type families. These rules are a breaking change from today's closed type families, but a "good" breakage, in that it tightens up the specification from the current wonky state of affairs. See the example from comment:18, which would no longer type-check. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler