Skip to content

Ordering of declarations can cause typechecking to fail

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information