Singling Nat-indexed GADT with addition?

[bgamari]

The following genSingletons application fails:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module Main where

import GHC.TypeLits
import Data.Kind
import Data.Singletons.TH
import Data.Singletons.TH.Options

type RegLayout :: Nat -> Type
data RegLayout len where
    Both  :: forall len1 len2. RegLayout len1 -> RegLayout len2 -> RegLayout (len1 + len2)

$(withOptions (defaultOptions {genSingKindInsts=False}) $ genSingletons [ ''RegLayout ])

The problem appears to be the application of the (+) type family in the result type of Both. I suppose such family usage is just expecting too much of poor singletons?

• singletons-th-3.1
• singletons-3.0.1

[RyanGlScott]

The problem is that genSingletons will generate instances that mention the (+) type family, and GHC simply doesn't allow this, e.g.,

Main.hs:23:2: error: [GHC-73138]
    * Illegal type synonym family application `len1
                                               + len2' in instance:
        SingI @{RegLayout (len1 + len2)} (Both @len1 @len2 n n1)
    * In the instance declaration for
        `SingI ('Both (n_a2K3 :: RegLayout len1_X0) (n_a2K4 :: RegLayout len2_X1))'
   |
23 | $(withOptions (defaultOptions {genSingKindInsts=False}) $ genSingletons [ ''RegLayout ])
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

<snip>

Off the top of my head, the generated instances that are affected by this are:

1. SingI
2. SuppressUnusedWarnings
3. Apply (for defunctionalization symbols)

The first two, while nice to have, are not really essential to making singletons-th-generated code typecheck, and I could imagine adding configuration options to disable generating them (similar to the existing genSingKindInsts option). The generated Apply instances are much more important, as singletons-th relies on them to generate code in a compositional way. Without Apply instances, singletons-th wouldn't be able to promote or single any code that uses Both in an expression position.

On the other hand, this might be an acceptable compromise. Perhaps you don't actually want to promote or single code that uses Both as an expression. Instead, perhaps you only want singletons-th to generate SRegLayout (the singled version of RegLayout) so that you can write code involving SRegLayout by hand? If that is the case, then you could get away without using Apply or any defunctionalization symbols, so having singletons-th not generate them would be fine.

Is this an accurate summary of what you are trying to do? If so, I could add additional configuration options to singletons-th to disable generating these instances (with the corresponding caveats about what you'd be missing if you do).