[GHC] #10041: Instance signatures (InstanceSigs) don't accept '[] :: [ĸ]
#10041: Instance signatures (InstanceSigs) don't accept '[] :: [ĸ] -------------------------------------+------------------------------------- Reporter: | Owner: Iceland_jack | Status: new Type: bug | Milestone: Priority: low | Version: 7.8.3 Component: Compiler | Operating System: Linux (Type checker) | Type of failure: GHC rejects Keywords: | valid program Architecture: x86 | Blocked By: Test Case: | Related Tickets: #9582 #9833 Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- The following doesn't compile with 7.8.3: {{{#!hs {-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-} {-# LANGUAGE TypeOperators, GADTs, InstanceSigs #-} data family Sing (a :: ĸ) 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 '[]`): {{{#!hs /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: {{{#!hs instance SingI '[] where sing = tmp where tmp :: Sing '[] tmp = SNil }}} This is '''not''' a problem for other data kinds such as `Bool` though: {{{#!hs 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 i 7.10 but unfortunately I don't have a more recent version of GHC to check. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10041 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
The following doesn't compile with 7.8.3:
{{{#!hs {-# LANGUAGE PolyKinds, TypeFamilies, DataKinds #-} {-# LANGUAGE TypeOperators, GADTs, InstanceSigs #-}
data family Sing (a :: ĸ) 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 '[]`):
{{{#!hs /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:
{{{#!hs instance SingI '[] where sing = tmp where tmp :: Sing '[] tmp = SNil }}}
This is '''not''' a problem for other data kinds such as `Bool` though:
{{{#!hs 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 i 7.10 but unfortunately I don't have a more recent version of GHC to check.
New description: The following doesn't compile with 7.8.3: {{{#!hs {-# 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 '[]`): {{{#!hs /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: {{{#!hs instance SingI '[] where sing = tmp where tmp :: Sing '[] tmp = SNil }}} This is '''not''' a problem for other data kinds such as `Bool` though: {{{#!hs 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 i 7.10 but unfortunately I don't have a more recent version of GHC to check. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10041#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
The following doesn't compile with 7.8.3:
{{{#!hs {-# 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 '[]`):
{{{#!hs /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:
{{{#!hs instance SingI '[] where sing = tmp where tmp :: Sing '[] tmp = SNil }}}
This is '''not''' a problem for other data kinds such as `Bool` though:
{{{#!hs 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 i 7.10 but unfortunately I don't have a more recent version of GHC to check.
New description: The following doesn't compile with 7.8.3: {{{#!hs {-# 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 '[]`): {{{#!hs /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: {{{#!hs instance SingI '[] where sing = tmp where tmp :: Sing '[] tmp = SNil }}} This is '''not''' a problem for other data kinds such as `Bool` though: {{{#!hs 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 i 7.10 but unfortunately I don't have a more recent version of GHC to check. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10041#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
The following doesn't compile with 7.8.3:
{{{#!hs {-# 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 '[]`):
{{{#!hs /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:
{{{#!hs instance SingI '[] where sing = tmp where tmp :: Sing '[] tmp = SNil }}}
This is '''not''' a problem for other data kinds such as `Bool` though:
{{{#!hs 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 i 7.10 but unfortunately I don't have a more recent version of GHC to check.
New description: The following doesn't compile with 7.8.3: {{{#!hs {-# 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 '[]`): {{{#!hs /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: {{{#!hs instance SingI '[] where sing = tmp where tmp :: Sing '[] tmp = SNil }}} This does '''not''' appear to be a problem for other data kinds such as `'True :: Bool` or `'False :: Bool` though: {{{#!hs 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10041#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
The following doesn't compile with 7.8.3:
{{{#!hs {-# 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 '[]`):
{{{#!hs /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:
{{{#!hs instance SingI '[] where sing = tmp where tmp :: Sing '[] tmp = SNil }}}
This does '''not''' appear to be a problem for other data kinds such as `'True :: Bool` or `'False :: Bool` though:
{{{#!hs 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.
New description: The following doesn't compile with 7.8.3: {{{#!hs {-# 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 '[]`): {{{#!hs /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: {{{#!hs 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: {{{#!hs 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. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10041#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 Simon Peyton Jones
#10041: Instance signatures (InstanceSigs) don't accept '[] :: [ĸ] -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: closed Priority: low | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: Resolution: fixed | Architecture: x86 Operating System: Linux | Test Case: Type of failure: GHC rejects | polykinds/T10041 valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: #9582 #9833 | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => polykinds/T10041 * resolution: => fixed Comment: 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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10041#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC