singletons generates ill-kinded type signature for class method

[RyanGlScott]

The following code fails to single with singletons-2.4.1 and HEAD:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind
import Data.Singletons.TH

$(singletons [d|
  class C (f :: k -> Type) where
    method :: f a
  |])

$(singletons [d|
  instance C [] where
    method = []
  |])

$ /opt/ghc/8.4.3/bin/ghc Bug.hs -ddump-splices
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
Bug.hs:(13,3)-(16,4): Splicing declarations
    singletons
      [d| class C_a2X8 (f_a3qK :: k_a2Xa -> Type) where
            method_a2X9 :: f_a3qK a_a3qL |]
  ======>
    class C_a6d2 (f_a6d5 :: k_a6d4 -> Type) where
      method_a6d3 :: f_a6d5 a_a6d6
    type MethodSym0 = Method
    class PC (f_a6d5 :: k_a6d4 -> Type) where
      type Method :: f_a6d5 a_a6d6
    class SC (f_a6d5 :: k_a6d4 -> Type) where
      sMethod :: Sing (MethodSym0 :: f_a6d5 a_a6d6)
Bug.hs:(18,3)-(21,4): Splicing declarations
    singletons
      [d| instance C [] where
            method = [] |]
  ======>
    instance C GHC.Types.[] where
      method = []
    type family Method_6989586621679034099_a6k4 :: [a_a6d6] where
      Method_6989586621679034099_a6k4 = '[]
    type Method_6989586621679034099Sym0 =
        Method_6989586621679034099_a6k4
    instance PC [] where
      type Method = Method_6989586621679034099Sym0
    instance SC [] where
      sMethod ::
        forall (a_a6d6 :: []). Sing (MethodSym0 :: f_a6d5 a_a6d6)
      sMethod = singletons-2.4.1:Data.Singletons.Prelude.Instances.SNil

Bug.hs:18:3: error:
    • Expecting one more argument to ‘[]’
      Expected a type, but ‘[]’ has kind ‘* -> *’
    • In the kind ‘[]’
      In the type signature:
        sMethod :: forall (a_a6d6 :: []).
                   Sing (MethodSym0 :: f_a6d5 a_a6d6)
      In the instance declaration for ‘SC []’
   |
18 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

Two important things to note:

• This relies on the declaration for instance C [] instance being in a separate splice from the declaration for class C f. In other words, the bug appears to have something to do with the way that singletons is reifying SC.
• f having kind k -> Type is also important, because changing it to Type -> Type makes the bug go away.

[RyanGlScott]

Ugh, this turns out to be very tricky to fix.

First, an explanation of why this bug occurs in the first place. When singling a class instance, we look up the type signature of each singled class method. For sMethod, this gives us:

sMethod :: forall k (f :: k -> Type). SC f => forall (a :: k). Sing (MethodSym0 :: f a)

Next, we need to figure out which types to substitute from the class head:

instance SC [] where ...

Here, there is (seemingly) only one type from the instance head. We this form a substitution roughly like so:

1. Take the tyvar binders from the front of the type signature for sMethod (everything before the SC f => ... part). Call these cls_tvbs.
2. Take the arguments to the class in the instance head. Call these inst_tys.
3. Form a substitution from zip cls_tvbs inst_tys.

It's step (3) where things go awry. Normally, the lengths of cls_tvbs and inst_tys are the same. However, SC is polykinded, which means that we have cls_tvbs = [ k, (f :: k -> Type) ]. However, we only have inst_tys = [ [] ]—the length of cls_tvbs exceeds that of inst_tys! This causes the substitution to erroneously map from k to [] in the type that we pick for sMethod in the resulting instance:

instance SC [] where
  -- Before substitution
  sMethod :: forall (a :: k). Sing (MethodSym0 :: f a)

  -- After substitution
  sMethod :: forall (a :: []). Sing (MethodSym0 :: f a)

And that's how we end up with the nonsensical results in the original post.

How do we fix this problem? It's not clear at all to me. The problem is that it's not easy in general to know what k should map to, since k is an implicit argument to C. In theory, we could somehow calculate the kind of [] to figure out k |-> Type, but that strongly resembles type inference, which is a direction that we have steadfastly avoided taking.

[goldfirere]

Instead of slurping the cls_tvbs from the quantified variables, can we look at the arguments to, e.g., SC? That would seem to work in all cases, I think.

[RyanGlScott]

I'm not sure what you mean by "look at the arguments". Can you give a more detailed example of how this would work?

[goldfirere]

We have

sMethod :: forall k (f :: k -> Type). SC f => forall (a :: k). Sing (MethodSym0 :: f a)

Currently, you're describing that we consider (wrongly) k and f to be the cls_tvbs because they're quantified before the constraint. However, we can look at the constraint SC f and know that SC's arguments are the cls_tvbs. (I know they're not tvbs there, but we can easily extract the variables.)

Or have I missed something?

[RyanGlScott]

Even if we actually mapped f |-> [] correctly, that still wouldn't be enough to generate something which kind-checked. We'd instead generate:

sMethod :: forall (a :: k). Sing (MethodSym0 :: [a])

Here, the kind of a is too general (it should actually be Type).

[goldfirere]

Ah, yes. Perhaps @mynguyenbmc's work on visible kind application (which includes an update to TH) will solve the problem. I believe she'll be posting her work for review soon.

[RyanGlScott]

Now that I think about it, I have to wonder: why are we giving singled instance methods type signatures in the first place? As far as I can tell, they're completely unnecessary, since GHC is more than capable of inferring these types by itself. Plus, it's not like we're using them to bring type variables into scope, since that's a role that's already served by pattern signatures.

As evidence for this claim, I commented out singled instance method type signatures in Data.Singletons.Single, and all the tests still pass (modulo generating less code). Oh, and it also fixes the original program, which is nice too.

[goldfirere]

Well, it sounds like you've solved this then. I think we needed the signatures before TH could deal with pattern signatures that bound variables.

[RyanGlScott]

This is indeed encouraging. However, even after removing these instance method type signatures, it turns out that we're still using the aforementioned erroneous substitution in other parts of the code, which makes me worry that there's still a bug lurking. Let me see if it's possible to flush it out.

[RyanGlScott]

Welp, time for disappointing news: my plan of just ditching the instance method type signatures won't work. Here's a counterexample:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

import Data.Kind
import Data.Singletons.TH

$(singletons [d|
  class C (f :: Type -> Type) where
    method :: forall a. (f :: Type -> Type) a -> f a

  instance C [] where
    method x =
      case x of
        _ -> x
  |])

Normally, this generated the following SC [] instance:

    instance SC [] where
      sMethod ::
        forall a_a6Ev (t_a6EW :: ([] :: Type -> Type) a_a6Ev).
        Sing t_a6EW -> Sing (Apply MethodSym0 t_a6EW :: [a_a6Ev])
      sMethod (sX :: Sing x_a6EL)
        = case sX of { _ -> sX } ::
            Sing (Case_6989586621679035384_a6EN x_a6EL x_a6EL :: [a_a6Ev])

Notice that the kind variable a_a6Ev is being used in the return kind of Case_6989586621679035384_a6EN x_a6EL x_a6EL :: [a_a6Ev]. It turns out that if you remove the type signature for sMethod, then this fails to typecheck:

../Bug.hs:13:3: error:
    • Expected kind ‘[a0]’,
        but ‘Case_6989586621679066592 x_aeM7 x_aeM7’ has kind ‘[a]’
    • In the first argument of ‘Sing’, namely
        ‘(Case_6989586621679066592 x_aeM7 x_aeM7 :: [a_aeLV])’
      In an expression type signature:
        Sing (Case_6989586621679066592 x_aeM7 x_aeM7 :: [a_aeLV])
      In the expression:
          (case sX of { _ -> sX }) ::
            Sing (Case_6989586621679066592 x_aeM7 x_aeM7 :: [a_aeLV])
    • Relevant bindings include
        sX :: Sing t (bound at ../Bug.hs:13:3)
        sMethod :: Sing t -> Sing (Apply MethodSym0 t)
          (bound at ../Bug.hs:13:3)
   |
13 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

../Bug.hs:13:3: error:
    • Couldn't match type ‘a1’ with ‘a’
      ‘a1’ is a rigid type variable bound by
        an expression type signature:
          forall a1. Sing (Case_6989586621679066592 t t)
        at ../Bug.hs:(13,3)-(21,4)
      ‘a’ is a rigid type variable bound by
        the type signature for:
          sMethod :: forall a (t :: [a]). Sing t -> Sing (Apply MethodSym0 t)
        at ../Bug.hs:(13,3)-(21,4)
      Expected type: Sing (Case_6989586621679066592 t t)
        Actual type: Sing t
    • In the expression: sX
      In a case alternative: _ -> sX
      In the expression:
          (case sX of { _ -> sX }) ::
            Sing (Case_6989586621679066592 x_aeM7 x_aeM7 :: [a_aeLV])
    • Relevant bindings include
        sX :: Sing t (bound at ../Bug.hs:13:3)
        sMethod :: Sing t -> Sing (Apply MethodSym0 t)
          (bound at ../Bug.hs:13:3)
   |
13 | $(singletons [d|
   |   ^^^^^^^^^^^^^^...

[goldfirere]

Ugh. It looks like we need to be able to bind type variables explicitly....

[RyanGlScott]

Indeed. My next thought was "well what if we just use kinds in the pattern signatures"? Something like:

    instance SC [] where
      sMethod (sX :: Sing (x :: a))
        = case sX of { _ -> sX } ::
            Sing (Case x x :: [a])

Would work for that example, I think, but that only works because a happens to be mentioned in the first (explicit) argument in the type of method. If there was a variable that was only mentioned in the result type of method, I'm worried that this approach might fall down somewhere.

I agree that in order to fix this robustly, we'll likely need visible type variable patterns. I'll go ahead and park this ticket for now pending further developments on GHC's side.

[goldfirere]

Agreed on all fronts.

[RyanGlScott]

To answer my earlier question about whether the erroneous substitution was causing other bugs, the answer is currently no (but with an emphasis on "currently").

There are only two other places that use this substitution:

1. For substituting into the context of the method type signature. But this only matters for generating SingI instances for defunctionalization symbols, and we don't do this for class instances anyway, so this is a non-issue.
2. For substituting into the return type of the method type signature. This is potentially a threat, since this type is used to annotate the right-hand side of the method's implementation in certain cases (e.g., for case expressions), but due to an amusing set of circumstances, this is unlikely to ever happen:

• If the type signature for the class method is reified locally (i.e., if we grab it using withLocalDeclarations), then due to Locally reified class methods don't explicitly quantify kind variables th-desugar#88, the number of type variable binders at the front of the type signature will always be in correspondence with those in the class head. (If we fix Locally reified class methods don't explicitly quantify kind variables th-desugar#88, though, this assumption will no longer hold true.)
• If the type signature for the class method is not reified locally (i.e., if we successly qReify it), then we will only grab the return type for later use if the singled return type is of the form Sing (foo :: return_type). But 99% of the time, calling qReify will actually give you just Sing foo, since round-tripping through Template Haskell destroys the :: return_type part. So we end up not using the return type anyway, which avoids the issue.

[RyanGlScott]

Hold on, I just thought of another approach which might bypass this issue entirely. I was so caught up in trying to remove InstanceSigs that I never thought to wonder "what if I add more InstanceSigs"? In particular, if you wrote:

$(singletons [d|
  instance C [] where
    method :: [a]
    method = []
  |])

Then instead of trying to look up the type of method elsewhere, we could simply single the method :: [a] instance signature directly and use that. This way, we can have fine-tuned control over the kinds of each type variable, and avoid the dreaded bogus substitution entirely!

Of course, this wouldn't be a fix for the underlying bogus substitution. But it is a workaround, and a pretty solid one too. Plus, we'd be able to support another GHC language feature, which is a nice bonus.

Does that sound like a reasonable approach? I have a working prototype of this feature at the moment (that I'm currently testing on my upstream code which originally triggered this issue), so if you like what you see here, then we can get it in before the final 2.5 release.

[goldfirere]

Could I summarize your proposal as "Every instance of a poly-kinded type class must have signatures on all methods" (if we are to single it)? That's a cheap-and-cheerful way to make quick progress, and it's easy to specify and conform to.