Skip to content

Instance signatures (InstanceSigs) don't accept '[] :: [ĸ]

The following doesn't compile with 7.8.3:

{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-}
{-# LANGUAGE TypeOperators, GADTs, InstanceSigs #-}

data family Sing (a :: k)
data instance Sing (xs :: [k]) where
  SNil :: Sing '[]

class SingI (a :: ĸ) where 
  sing :: Sing a

instance SingI '[] where
  sing :: Sing '[]
  sing = SNil

and the error message suggests the very type provided (Sing '[]):

/tmp/Error.hs:11:11:
    Method signature does not match class; it should be
      sing :: Sing '[]
    In the instance declaration for SingI '[]
Failed, modules loaded: none.

Creating a local variable with the same type signature works fine:

instance SingI '[] where
  sing = tmp where
    tmp :: Sing '[]
    tmp = SNil

This does not appear to be a problem for other types of kind Bool such as 'True or 'False though:

data instance Sing (xs :: Bool) where
  STrue  :: Sing True
  SFalse :: Sing False

instance SingI True where
  sing :: Sing True
  sing = STrue

instance SingI False where
  sing :: Sing False
  sing = SFalse

This resembles #9582 (closed) but I don't believe it is the same error, it has possibly been fixed in 7.10 but unfortunately I don't have a more recent version of GHC to check.

Edited by Icelandjack
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information