Opened 2 years ago

Closed 6 months ago

Last modified 6 months ago

#12922 closed bug (wontfix)

Kind classes compile with PolyKinds

Reported by: Tritlo Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by Tritlo)

I was asking around on #haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds.

To study it, I was working with the following small example:

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds #-}
module Main where

-- Define a Type for the natural numbers, zero and a successor
data Nat = Z | S Nat

class Addable k where
  type (a :: k) + (b :: k) :: k

instance Addable Nat where
  type (Z + a) = a
  type (S a) + b = S (a + b)

main :: IO ()
main = putStrLn "Shouldn't this need TypeInType?"

(for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930)

Since according to a responder on #haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds.

As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it.

Change History (11)

comment:1 Changed 2 years ago by Tritlo

Description: modified (diff)

comment:2 Changed 2 years ago by Tritlo

Description: modified (diff)

comment:3 Changed 2 years ago by RyanGlScott

For a simpler example, this compiles in GHC 8.0.1 (but probably shouldn't) without TypeInType:

{-# LANGUAGE PolyKinds #-}

type KindOf (a :: k) = k

comment:4 Changed 2 years ago by Tritlo

Description: modified (diff)

comment:5 Changed 2 years ago by simonpj

Without thinking too deeply

  • TypeInType should imply PolyKinds.
  • PolyKinds should be enough for kind classes, if by "kind classes" you mean polymorphism over types of kind Constraint.

comment:6 Changed 2 years ago by goldfire

Owner: set to goldfire

But look at the OP's

class Addable k where
  type (a :: k) + (b :: k) :: k

where the class variable k is used as a kind. This indeed should not be allowed unless TypeInType is on. I'll put this in my queue.

comment:7 in reply to:  6 Changed 2 years ago by Iceland_jack

Welcome Tritlo!

comment:8 Changed 7 months ago by RyanGlScott

Keywords: TypeInType added

comment:9 Changed 6 months ago by monoidal

Resolution: wontfix
Status: newclosed

We no longer distinguish between TypeInType and PolyKinds, so I'm closing this ticket.

See https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst and #15195 for more details.

comment:10 Changed 6 months ago by RyanGlScott

Hm... I wonder if we should convert the TypeInType Trac keyword to PolyKinds as well?

comment:11 Changed 6 months ago by monoidal

Technically TypeInType also covers DataKinds. I wouldn't worry about this.

Note: See TracTickets for help on using tickets.