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