GitLab

The following will successfully typecheck:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}

data CInst

data G (b :: ()) = G 

class C a where
  type family F a
  
class (C a) => C' a where
  type family F' a (b :: F a)

-- data CInst

instance C CInst where
  type F CInst = ()

instance C' CInst where
type F' CInst (b :: F CInst) = G b

But if the data CInst declaration is moved to where it is currently commented out, typechecking fails with this error:

Test.hs:23:18: error:
    • Expected kind ‘F CInst’, but ‘b’ has kind ‘()’
    • In the second argument of ‘F'’, namely ‘(b :: F CInst)’
      In the type instance declaration for ‘F'’
      In the instance declaration for ‘C' CInst’
   |
23 |   type F' CInst (b :: F CInst) = G b
   | 

However, the data declaration //can// be in the lower position if the kind annotation for its argument is instead written as data G (b :: F CInst) = G.

This behavior is also exhibited when G is a type family (I believe the sort of type family does not matter, but I know for sure closed and open type families).

I was using GHC 8.2.2 when I discovered this, but user erisco on #haskell confirmed for 8.2.1 as well.

Trac metadata

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