False kind errors with implicitly bound kinds in GHC 8.6

This could be related to #15343 (closed).

The following code fails to compile with GHC 8.6.0.20180627, but does compile with 8.4:

{-# LANGUAGE TypeInType #-} -- or PolyKinds
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind

class C (x :: Type) (y :: k) where
  type F y

    • Expected a type, but ‘k’ has kind ‘k’
    • In the kind ‘k’
  |
7 | class C (x :: Type) (y :: k) where
  |                       ^

Yet all of the following slightly different examples still do compile:

-- remove `x`
class C0 (y :: k) where type F0 y

-- remove `F`
class C1 (x :: Type) (y :: k)

-- remove the kind annotation from `x`
class C2 x (y :: k) where type F2 y

-- switch the order of `x` and `y`
class C3 (y :: k) (x :: Type) where type F3 y

-- make `k` an explicit parameter, with or without a kind annotation
class C4 k (x :: Type) (y :: k) where type F4 y
class C5 (k :: Type) (x :: Type) (y :: k) where type F5 y

-- add a new parameter *with no kind annotation*
class C6 z (x :: Type) (y :: k) where type F6 y

Here's also my original example which failed to compile:

type Hom k = k -> k -> Type

type family Ob (p :: Hom k) :: k -> Constraint

class ( obP ~ Ob p
      , opP ~ Dom p
      , obQ ~ Ob q
      , opQ ~ Dom q
      , p ~ Dom f
      , q ~ Cod f
      ) => Functor' (obP :: i -> Constraint)
                    (opP :: Hom i)
                    (p :: Hom i)
                    (obQ :: j -> Constraint)
                    (opQ :: Hom j)
                    (q :: Hom j)
                    (f :: i -> j) where
  type Dom f :: Hom i
  type Cod f :: Hom j

    • Expected a type, but ‘j’ has kind ‘k’
    • In the first argument of ‘Hom’, namely ‘j’
      In the kind ‘Hom j’
   |
34 |   type Cod f :: Hom j
   |                     ^

The only way I can find to make this one compile is to make i and j explicit parameters with explicit kinds:

class ( obP ~ Ob p
      , opP ~ Dom p
      , obQ ~ Ob q
      , opQ ~ Dom q
      , p ~ Dom f
      , q ~ Cod f
      ) => Functor' (i :: Type)
                    (j :: Type)
                    (obP :: i -> Constraint)
                    (opP :: Hom i)
                    (p :: Hom i)
                    (obQ :: j -> Constraint)
                    (opQ :: Hom j)
                    (q :: Hom j)
                    (f :: i -> j) where
  type Dom f :: Hom i
  type Cod f :: Hom j

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

False kind errors with implicitly bound kinds in GHC 8.6

Child items ...

Activity