#7939: RHS of associated type not kind-checked ------------------------------------------+--------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Os: Unknown/Multiple | Architecture: Unknown/Multiple Failure: GHC accepts invalid program | Difficulty: Unknown Testcase: ghci/scripts/T7939 | Blockedby: Blocking: | Related: ------------------------------------------+--------------------------------- Comment(by simonpj): Concerning the dark corner, there is a reason that classes are by-default kind-polymorphic: there are some visible uses of the type variable to constraint it. Consider {{{ class C a where { opc :: a -> a } class D f b where { opd :: f b -> f b } }}} Then, just as in a data type declaration, we look at the uses of type variables `a`, `f`, `b`, and get these kinds: {{{ C :: * -> Constraint D :: (k -> *) -> k -> Constraint }}} This is good. It is very different for a top-level open type family {{{ type family F a b }}} Here there are no uses, and hence no kind constraints, on `a` and `b`, and there can't be. But it seems over-kill to assume maximal polymorphism, so our plan is to default to *, thus {{{ F :: * -> * -> * }}} Now, with the associated type you give, there's a mixture of the two: {{{ class Foo a where type Bar a b op :: a -> a }}} Here there probably ''are'' some constraints on `a` (from the class methods as usual), but there can be none on `b`. So my suggestion would be to default `b` to `*`, just like for top-level ones, but to constrain `a` by the way it is used in class methods and superclasses. That's a bit more complicated in a way, but there is a principled reason: * If there is some "scope" for the variable, infer the kind from its uses * If there is no "scope", use `*`, unless there's a kind annotation. Simon -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7939#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler