[GHC] #15352: False kind errors with implicitly bound kinds in GHC 8.6

7 Jul 2018


      #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