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

[GHC]

#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
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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.)

New description:

 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler