Opened 5 years ago

Closed 5 years ago

#10041 closed bug (fixed)

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

Reported by: Iceland_jack Owned by:
Priority: low Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: Cc:
Operating System: Linux Architecture: x86
Type of failure: GHC rejects valid program Test Case: polykinds/T10041
Blocked By: Blocking:
Related Tickets: #9582 #9833 Differential Rev(s):
Wiki Page:

Description (last modified by Iceland_jack)

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 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.

Change History (7)

comment:1 Changed 5 years ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 5 years ago by Iceland_jack

Description: modified (diff)

comment:3 Changed 5 years ago by Iceland_jack

Description: modified (diff)

comment:4 Changed 5 years ago by Iceland_jack

Description: modified (diff)

comment:5 Changed 5 years ago by goldfire

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.

comment:6 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

comment:7 Changed 5 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: polykinds/T10041

Happily, some work I did on instance signatures (yes it was #9582) 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

Note: See TracTickets for help on using tickets.