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

GHC ghc-devs at haskell.org
Wed Jan 28 15:38:16 UTC 2015


#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


More information about the ghc-tickets mailing list