[GHC] #7939: RHS of associated type not kind-checked

[GHC]

#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