#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): OK, so (NEWCUSK) is precisely (BASELINE) with a slightly expanded definition of CUSK (c.f. the [http://www.haskell.org/ghc/docs/latest/html/users_guide/kind- polymorphism.html#complete-kind-signatures current definition in the user manual]). I'm all for that; I quite liked (BASELINE): it's pretty simple and lines up precisely with the term-level story (a la Mark Jones). Just to check, though, let's be sure we agree: {{{ data T1 f a = MkT1 (f a) -- No CUSK -- Gets T1 :: forall k. (k->*) -> k -> * -- The generalisation takes place in the third bullet of step 3 of (BASELINE) data T2 a b :: * -- Presumably a nullary data type -- No CUSK -- Gets T2 :: forall k1 k2. k1 -> k2 -> * -- Very similar to T1 }}} I have no idea what you mean by "2) Allow more flexible partial kind signatures" in comment:19. Could you update the wiki page with: * (NEWCUSK) (= (BASELINE) + revised defn of CUSK) * the typing rules for closed type families Thanks! Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler