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.

changed weight to 3

added Tbug Trac import typechecker labels

changed the description

Ick.

The problem boils down to the fact that type signatures are meant to be self-standing -- that is, a type signature is understood in a vacuum, without looking around.

Let's look here:

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

I'll rewrite with all kind variables made explicit. (By the way, you'll get more sensible error messages with -fprint-explicit-kinds.)

instance SingI k1 ('[] k1) where
  sing :: forall k2. Sing k2 ('[] k2)
  sing k2(?) = SNil k2

We can see here why the instance signature is rejected. When GHC sees a signature Sing '[], it chooses a fresh kind variable, doesn't find anything constraining that kind variable, and thus generalizes over it. But that's not what you want! You want k1. GHC doesn't know this.

Let's look at your working example, again with explicit kinds:

instance SingI k1 ('[] k1) where
  sing k1 = tmp k1 where      -- NB: it *must* be k1
    tmp :: forall k2. Sing k2 ('[] k2)
    tmp k2 = SNil k2

Here, we have no problem, because GHC generalizes tmp and then instantiates it at the right kind. It has no such flexibility with a direct signature.

So the fix, I believe, would be to match the instance signature before it is generalized.

mentioned in commit 0f75a3f0

closed

Happily, some work I did on instance signatures (yes it was #9582 (closed)) seems to have cured this. At least, HEAD is fine. And the 7.10 branch is fine too.

Thanks for reporting. I've added a regression tests.

Simon

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	→ polykinds/T10041

added Plow label

mentioned in issue #19017