So moving from (BASELINE) to (PARGEN) would be a breaking change, but only in rather obscure circumstances. I am intensely relaxed about that
#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): * I agree that (PARGEN) is a breaking change. But, I'll quote Simon's comment from the wiki page, which I fully agree with: particular backward-compatibility problem! * Non-recursive bindings should behave the same as recursive ones. This means that `NR` would be rejected due to the side condition. == Closed type families == (PARGEN) (including the side condition) should work out just fine. Here would be the declarative typing rule: {{{ k2 = forall fkv(k1). k1[k'1 .. k'n/_] fkv(k1) \not\in k'j forall i: G, F:k2 |- (F ps_i = t_i) ok k3 = gen(G, k2) --------------------------------------------------- G |- type family F :: k1 where { F ps_i = t_i } : k3 }}} This is very similar to the declarative typing rule for `letrec` given on the [GhcKinds/KindInference wiki page]. Here, I am ignoring issues with arity/saturation and using a syntax where the kind signature of a type family is given as `k1` with blanks, instead of the tyvarbndr syntax used in source code. This is in fact an improvement over the current state of affairs, which is essentially this rule ''without'' the side condition. Because of the omitted side condition, we don't have principal types! For example, {{{ type family X (a :: k) where X True = False }}} `X` could be `X :: k -> k` or `X :: k -> Bool`. Neither is more general than the other. GHC chooses `X :: k -> Bool`, but it's not principled. This is what I get for implementing kind inference for closed type families without writing out declarative rules! In any case, the solution to this problem (closed type families) seems to be the same as the solution for datatypes and classes, quite happily: add the side condition. == Using (PARTIAL) == I'm still quite strongly against (PARTIAL). Let's ignore the backward compatibility problem, for now. With (PARTIAL), we have a very different story about kind polymorphism than we do about type polymorphism. GHC tries to be as polymorphic as possible with types: writing `foo x = x` gives `foo :: forall a. a -> a`, ''not'' `foo : () -> ()`. It seems very odd to me to not do the same in kinds. Yet, (PARTIAL) would say that `data Foo x = MkFoo (Foo x)` would get `Foo :: * -> *` instead of `Foo :: forall k. k -> k`. Especially as we're inching toward dependent types, this seems like a step backward. And, though I defer to Edward's experience, I tend to think the backward compatibility problem would be annoying for what may seem like a dubious benefit (polymorphic recursion in the presence of partial kind signatures). == Conclusion == I ''am'' worried that (PARGEN) has a strange surface area, and I think that any error messages that the side condition produces should include a URL for further reading. (I actually think that links to further reading would helpful in several error messages!) But, if this surface area is deemed too bumpy, I personally would prefer to go back to (BASELINE) than to go to (PARTIAL). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9200#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler