On generating singletons for Idx (a.k.a. Fin)

[RyanGlScott]

This isn't a bug report so much as a response to a challenge you posed during your Chalmers FP talk. And who am I to back down from a challenge? :)

If I understood you correctly, the reason that VarTy is defined like it is below:

challenge/debruijn/src/Poly.hs

Line 11 in e9ef4d4

data Ty = IntTy | Ty :-> Ty | VarTy Idx | PolyTy Ty

Is due to a restriction in singletons. That is, VarTy uses a "simply typed" Idx (which is just a synonym for Nat) since it promoted/singles more easily using singletons' TH machinery. The drawback of this approach is that VarTy doesn't track the scope of type variables in Tys. This would be possible if a "richly typed" version of Idx were used instead:

challenge/debruijn/src/SubstScoped.hs

Lines 15 to 17 in e9ef4d4

	data Idx :: Nat -> Type where
	FZ :: Idx (S n)
	FS :: Idx n -> Idx (S n)

However, this doesn't play nicely with singletons' TH machinery out of the box, making it inconvenient to use. (Did I summarize that accurately? If not, that makes the rest of this moot.)

The good news is that singletons-2.7 (which requires GHC 8.10 or later) has a configurable setting that makes automatically promoting/singling Idx possible. The challenge with handling GADTs is that the TH machinery will try to generate an instance of the SingKind class. Unfortunately, SingKind's current design isn't well suited to dealing with GADTs. Luckily, you can disable the generation of SingKind instances altogether by using Data.Singletons.TH.Options, like so:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Idx where

import Control.Monad.Trans.Class
import Data.Kind
import Data.Singletons.TH
import Data.Singletons.TH.Options

$(withOptions defaultOptions{genSingKindInsts = False} $
  singletons $ lift [d|
    data Nat = Z | S Nat

    data Idx :: Nat -> Type where
        FZ :: Idx (S n)
        FS :: Idx n -> Idx (S n)
  |])

Not having a SingKind instance for Idx n may impact your library, however, since the toSing method of SingKind is used in a couple of places. If so, you can always roll your own version of toSing fairly easily:

toSIdx :: Idx n -> SomeSing (Idx n)
toSIdx FZ     = SomeSing SFZ
toSIdx (FS n) =
  case toSIdx n of
    SomeSing sn -> SomeSing (SFS sn)

I haven't attempted to use the "richly typed" version of Idx in VarTy, as I'm unclear what sort of repercussions that would have on the rest of the design. But this should hopefully demonstrate that it is at least possible!

[sweirich]

Thanks. I made a branch for experimenting called promote-fin.

The file that has the definition for Idx is SubstScoped.hs. I had trouble defining Idx separately from Nat, I was getting these errors:

src/SubstScoped.hs:17:3: error:
    Not in scope: type constructor or class ‘SZSym0’
src/SubstScoped.hs:17:3: error:
    Not in scope: type constructor or class ‘SSSym0’
src/SubstScoped.hs:17:3: error:
    Not in scope: data constructor ‘SSZ’
src/SubstScoped.hs:17:3: error:
    Not in scope: data constructor ‘SSS’

Should Nat produce them? Or do I need another option?

[RyanGlScott]

Interesting. If I'm reading that correctly, the issue is not due to Idx itself, but rather the various functions in SubstScope that use SNats, such as these:

challenge/debruijn/src/SubstScoped.hs

Lines 42 to 48 in b5bb206

	-- Identity substitution, leaves all variables alone
	nilSub :: Sub a n n
	nilSub = Inc SZ
	-- Increment, shifts all variables by one
	incSub :: Sub a n (S n)
	incSub = Inc (SS SZ)

In order to produce singled versions of these functions, we need to single the SZ and SS constructors. singletons assumes you have done this already and boldly generates code involving SSZ and SSS (that's a lot of Ss!), but since these aren't defined anywhere, havoc ensues. A quick-and-dirty way to make GHC happy is to manually single SNat:

diff --git a/debruijn/src/SubstScoped.hs b/debruijn/src/SubstScoped.hs
index aae6be4..092a61b 100644
--- a/debruijn/src/SubstScoped.hs
+++ b/debruijn/src/SubstScoped.hs
@@ -14,6 +14,9 @@ import Data.Singletons.TH.Options
 -- are used to describe the number of free variables allowed in 
 -- a term.    
 
+$(withOptions defaultOptions{genSingKindInsts = False} $
+  genSingletons [''SNat])
+
 $(withOptions defaultOptions{genSingKindInsts = False} $
   singletons $ lift [d|

(As a side note, it would be great if we didn't have to generate singletons for singletons. See goldfirere/singletons#460 for a discussion on how this might be improved.)

Unfortunately, that doesn't solve all of our problems. While the old error messages should go away, new ones take their place. They all have the same general shape:

[16 of 18] Compiling SubstScoped      ( src/SubstScoped.hs, interpreted )

...

src/SubstScoped.hs:20:3: error:
    • Illegal type synonym family application ‘Plus m n’ in instance:
        SingI @{SNat m ~> (Idx n ~> Idx (Plus m n))} (AddSym0 @m @n)
    • In the instance declaration for
        ‘SingI (AddSym0 :: (~>) (Sing m_aOGY) ((~>) (Idx n_aOGZ) (Idx (Plus m_aOGY n_aOGZ))))’
   |
20 | $(withOptions defaultOptions{genSingKindInsts = False} $
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

src/SubstScoped.hs:20:3: error:
    • Illegal type synonym family application ‘Plus m n’ in instance:
        SuppressUnusedWarnings
          @(TyFun (SNat m) (Idx n ~> Idx (Plus m n)) -> Type) (AddSym0 @m @n)
    • In the instance declaration for ‘SuppressUnusedWarnings AddSym0’
   |
20 | $(withOptions defaultOptions{genSingKindInsts = False} $
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

src/SubstScoped.hs:20:3: error:
    • Illegal type synonym family application ‘Plus m n’ in instance:
        Apply
          @(SNat m)
          @(Idx n ~> Idx (Plus m n))
          (AddSym0 @m @n)
          a6989586621679204769
    • In the type instance declaration for ‘Apply’
   |
20 | $(withOptions defaultOptions{genSingKindInsts = False} $
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

...

The root cause of these errors is that the type of add mentions Plus, a type family. As a result, the kind of the promoted Add type family also mentions Plus, but GHC freaks out if you attempt to define a type class instance (or type family instance) that mentions a type family in the head. singletons attempts to define three instances for AddSym0 (a defunctionalization symbol for Add), all of which mention the type family Plus in a kind argument, which GHC rejects.

Unfortunately, I don't have a quick-and-dirty fix this time, so I suppose this means that I have failed the challenge. Oh well. At this point, I can only speculate on ways that I could improve singletons to make a better attempt at solving these problems.

Just as I added an option to disable generating SingKind instances, I could likely add options to disable generating instances of SingI, SuppressUnusedWarnings, and Apply. The SingI AddSym0 instance, while nice to have, is not really essential to the way singletons works, and it could be safely omitted. The SuppressUnusedWarnings AddSym0 instance is only there to prevent GHC from emitting spurious warnings, so it too could be omitted without negative consequences.

The Apply AddSym0 instance is definitely the trickiest. In theory, you should only need it if you attempt to invoke Add in higher-order settings. That being said, the internals of singletons use defunctionalization symbols pervasively whenever dealing with function applications. For example, f x y = add x y will promote to type family F x y where F x y = AddSym0 `Apply` x `Apply` y. While this greatly simplifies the internals of singletons, a consequence of this design choice is that you cannot safely omit defunctionalization symbols in general. And indeed, you would find yourself needing AddSym0 if you attempted to promote this line of code:

challenge/debruijn/src/SubstScoped.hs

Line 67 in b5bb206

applySub (Inc m) x = var (add m x)

Is there any hope of supporting type-family-returning functions in today's singletons? Perhaps not with the way it is currently designed. But improvements to GHC might make better designs feasible:

• If UnsaturatedTypeFamilies were implemented, we would no longer need defunctionalization symbols, which would make all of these AddSym0-like issues moot.
• Even if we don't have UnsaturatedTypeFamilies, we might be able to improve the current state of affairs by making GHC less picky about having type families appear in type family instances. GHC#12564 describes a problem very similar to the AddSym0-related problems above, and this comment sketches a possible solution.

---

I apologize if that was more information than you wanted. This turned out to be much trickier than I expected it would be! (That makes it a good challenge, I suppose.)

[sweirich]

Thanks, Ryan this is fascinating. Is there a way to rewrite SubstScoped so that it plays better with singletons?

[RyanGlScott]

Is there a way to rewrite SubstScoped so that it plays better with singletons?

I don't know what this code will look like when it's finished, so I don't know how detailed of an answer I can give. I can at least give some generic advice that I have used in the past to deal with especially fancy singletons code. My usual workaround is to:

1. Identify which declarations within a $(singletons [d| ... |]) block absolutely must be promoted, and move everything else out. (It may be the case that everything in this block of code really must be promoted. If so, then I pre-emptively apologize—it's hard to tell from a glance.)
2. For those declarations that you really must promote but $(singletons) just won't let you, try to carve out the relevant bits that you need from the TH machinery. In other words, compile the $(singletons [d| ... |]) block with -ddump-splices enabled, remove the problematic definitions from the block, and then replace them with the relevant parts of the resulting debugging output. This is a bit of slog, but it still beats writing out all of the code by hand.

Using singletons to promote functions that return type families is hard, and I don't see an easy way to rewrite your code to avoid the TH machinery's current limitations (short of radical, whole-program refactorings like this one). But the advice above may let you get over the finish line. Alternatively, you may decide that the race isn't worth running, which is a perfectly valid response as well :)

[sweirich]

Thanks Ryan. I'll close this now as I don't see a way forward.