Re: [GHC] #10041: Instance signatures (InstanceSigs) don't accept '[] :: [ĸ]

[GHC]

#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