[GHC] #10132: Inconsistent kind polymorphism for top-level and associated type families

3 Mar 2015

      #10132: Inconsistent kind polymorphism for top-level and associated type families
-------------------------------------+-------------------------------------
              Reporter:  simonpj     |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.8.4
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Consider this, with `-XPolyKinds`:
 {{{
 class C a where
   data D1 a
   type F1 a

 data D2 a
 type F2 a
 }}}
 You'd expect `D1` and `D2` to behave exactly the same; and similarly `F1`
 and `F2`.  But they don't:
 {{{
 D1 :: forall k (a:k). k -> *
 D2 :: * -> *

 F1 :: forall k (a:k). k -> *
 F2 :: * -> *
 }}}
 This seems odd.  Indeed, when I stumbled across it I thought it was a
 plain bug.  But I think there is some justification:

  * For associated types like `D1`, `F1` we make the class kind-polymorphic
 by default.  And hence the associated types really have to be also.

  * Should classes be by-default kind-polymorphic?  Well, data types are,
 so probably classes should be too.  The types of the methods of the class,
 or the constructors of the data type, usually give plenty of clues.

  * For top-level types like `D2`, `F2`, it seems perhaps overkill to make
 them kind polymorphic by default.  The difference is that they have no
 right hand side to get clues from, so they'll always have kind `k1 -> k2
 -> k3` if you go for maximal polymorphism.  You can declare the
 polymorphism with kind signatures.

  * Why does `F1` return `*`.  It could as well be kind-polymorphic in its
 result.  Again I think this is because there cannot be any clue as to its
 result kind so we default to `*`.

 Maybe this is all a good choice.  The principle seems to be: '''if the
 declaration has a "right hand side", infer kinds from that; if not,
 default to `*`'''.

 But even if that is the right principle, we should articulate it
 explicitly, in the user manual and a `Note` somewhere.

 (I reverse-engineered all this when looking at #9999 again, in the new
 `Typeable` branch.)

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10132
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler