#15352: False kind errors with implicitly bound kinds in GHC 8.6 -------------------------------------+------------------------------------- Reporter: aaronvargo | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This could be related to #15343. The following code fails to compile with GHC 8.6.0.20180627, but does compile with 8.4: {{{#!hs {-# 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: {{{#!hs -- 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: {{{#!hs 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: {{{#!hs 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15352 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler