Opened 19 months ago

Last modified 4 weeks ago

#12922 new bug

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 (8)

comment:1 Changed 19 months ago by Tritlo

Description: modified (diff)

comment:2 Changed 19 months ago by Tritlo

Description: modified (diff)

comment:3 Changed 19 months 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 19 months ago by Tritlo

Description: modified (diff)

comment:5 Changed 19 months 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 19 months 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 19 months ago by Iceland_jack

Welcome Tritlo!

comment:8 Changed 4 weeks ago by RyanGlScott

Keywords: TypeInType added
Note: See TracTickets for help on using tickets.