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       |
-------------------------------------+-------------------------------------

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