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

28 Jan 2015

      #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