#10041: Instance signatures (InstanceSigs) don't accept '[] :: [ĸ] -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: Resolution: | Architecture: x86 Operating System: Linux | Test Case: Type of failure: GHC rejects | Blocking: valid program | Differential Revisions: Blocked By: | Related Tickets: #9582 #9833 | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10041#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler