`Illegal type synonym family application` when promoting a function on singleton-indexed types

[fpringle]

I'm trying to define a fixed-length vector type, indexed by Peano numbers, then promote the vector, and define an append operation on that vector, both at the type and the value level. I need the defunctionalisation symbols because I'm going to use this family later in a more complicated function, which I'll also want to promote.

{-# LANGUAGE TemplateHaskell #-}

import Data.Singletons.TH
import Data.Singletons.TH.Options

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

        (++) :: N -> N -> N
        Z ++ m = m
        S n ++ m = S (n ++ m)

        type Vec :: N -> Type -> Type
        data Vec n a where
          VNil :: Vec 'Z a
          (:.) :: a -> Vec n a -> Vec ('S n) a
        |]
 )

$( singletons
    [d|
      (+++) :: Vec n a -> Vec m a -> Vec (n ++ m) a
      VNil +++ ys = ys
      (x :. xs) +++ ys = x :. (xs +++ ys)
      |]
 )

GHC refuses to compile the second splice, with the following error:

src/Lambda/TypeLevel/Example.hs:24:2: error: [GHC-73138]
    • Illegal type synonym family application ‘n ++ m’ in instance:
        Apply
          @(Vec n a)
          @(Vec m a ~> Vec (n ++ m) a)
          ((+++@#@$) @n @a @m)
          a6989586621679086404
    • In the type instance declaration for ‘Apply’
   |
24 | $( singletons
   |  ^^^^^^^^^^^^...

The generated code (cleaned up) is:

(+++) :: Vec n a -> Vec m a -> Vec (n ++ m) a
(+++) VNil ys = ys
(+++) (x :. xs) ys = x :. (xs +++ ys)

type (+++@#@$) :: (~>) (Vec n a) ((~>) (Vec m a) (Vec (n ++ m) a))
data (+++@#@$) :: (~>) (Vec n a) ((~>) (Vec m a) (Vec (n ++ m) a)) where
  (:+++@#@$###) ::
    (SameKind (Apply (+++@#@$) arg) ((+++@#@$$) arg)) => (+++@#@$) a

type instance Apply (+++@#@$) v1 = (+++@#@$$) v1

instance SuppressUnusedWarnings (+++@#@$) where
  suppressUnusedWarnings = snd ((,) (:+++@#@$###) ())

type (+++@#@$$) ::
  Vec n a ->
  (~>) (Vec m a) (Vec (n ++ m) a)
data (+++@#@$$) (v1 :: Vec n a) :: (~>) (Vec m a) (Vec (n ++ m) a) where
  (:+++@#@$$###) ::
    (SameKind (Apply ((+++@#@$$) v1) arg) ((+++@#@$$$) v1 arg)) =>
    (+++@#@$$) v1 v2

type instance Apply ((+++@#@$$) v1) v2 = (+++) v1 v2

instance SuppressUnusedWarnings ((+++@#@$$) v1) where
  suppressUnusedWarnings = snd ((,) (:+++@#@$$###) ())

type (+++@#@$$$) :: Vec n a -> Vec m a -> Vec (n ++ m) a
type family (+++@#@$$$) (v1 :: Vec n a) (v2 :: Vec m a) :: Vec (n ++ m) a where
  (+++@#@$$$) v1 v2 = (+++) v1 v2

type (+++) :: Vec n a -> Vec m a -> Vec (n ++ m) a
type family (+++) (a_abqp :: Vec n a) (a_abqq :: Vec m a) :: Vec (n ++ m) a where
  (+++) 'VNil ys = ys
  (+++) ('(:.) x xs) ys = Apply (Apply (:.@#@$) x) (Apply (Apply (+++@#@$) xs) ys)

(%+++) ::
  ( forall
      (t1 :: Vec n a)
      (t2 :: Vec m a).
    Sing t1 ->
    Sing t2 ->
    Sing (Apply (Apply (+++@#@$) t1) t2 :: Vec (n m) a) ::
      Type
  )
(%+++) SVNil (sYs :: Sing ys) = sYs
(%+++) ((:%.) (sX :: Sing x) (sXs :: Sing xs)) (sYs :: Sing ys) =
  applySing
    (applySing (singFun2 @(:.@#@$) (:%.)) sX)
    (applySing (applySing (singFun2 @(+++@#@$) (%+++)) sXs) sYs)

instance SingI ((+++@#@$) :: (~>) (Vec n a) ((~>) (Vec m a) (Vec (n ++ m) a))) where
  sing = singFun2 @(+++@#@$) (%+++)

instance
  (SingI v) =>
  SingI ((+++@#@$$) (v :: Vec n a) :: (~>) (Vec m a) (Vec (n ++ m) a))
  where
  sing =
    singFun1
      @((+++@#@$$) (v :: Vec n a))
      ((%+++) (sing @v))

instance SingI1 ((+++@#@$$) :: Vec n a -> (~>) (Vec m a) (Vec (n ++ m) a)) where
  liftSing (s :: Sing (v :: Vec n a)) =
    singFun1
      @((+++@#@$$) (v :: Vec n a))
      ((%+++) s)

This feels like a fairly fundamental thing to want to do with singletons. Is there a standard way of getting round this problem?

[RyanGlScott]

This is another version of the same problem observed in #580. As noted there, the problem is that singletons wants to generate class instances and type family instances, but GHC refuses to allow type families (such as the promoted (++) type family) to appear in the heads of these instances. That is a GHC problem, and one that seems unlikely to go away any time soon: see https://gitlab.haskell.org/ghc/ghc/-/issues/12564.

Unfortunately, I don't really see a good way to work around this. The generated instances that mention type families in their heads are the Apply instances, and you really do need to define those instances in order to make defunctionalization work. I would suggest hand-writing this definition in a way that avoids the need for defunctionalization, but you specifically cite the need to have defunctionalization symbols, so we're at an impasse.

[fpringle]

Hi Ryan, thanks for providing the links to the relevant issues. Shame that this doesn't seem to be a solveable problem for now. I considered making (++) an actual constructor of the N type, with a corresponding Vec constructor, but that doesn't seem to solve much.

Yes, I think the defunctionalisation symbols are definitely needed in my case. I have other types that are indexed by Vec, which then have functions on them that need to be promoted too. I'll see how far I can get by writing these manually, but I think I'm going to continue running into this problem.

[fpringle]

I found some more primtive cases which gave similar (but varying) error messages.

This compiles:

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

        constZ :: N -> N
        constZ _ = Z 

        type Vec :: N -> Type -> Type
        data Vec n a where
          VNil :: Vec 'Z a
          (:.) :: a -> Vec n a -> Vec ('S n) a
        |]  
 )

$( singletons
    [d| 
      constVNil :: Vec n N -> Vec (ConstZ n) N
      constVNil _ = VNil
      |]  
 )

This doesn't (only difference is the pattern matching in constZ:

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

        constZ :: N -> N
        constZ Z = Z
        constZ (S _) = Z

        type Vec :: N -> Type -> Type
        data Vec n a where
          VNil :: Vec 'Z a
          (:.) :: a -> Vec n a -> Vec ('S n) a
        |]
 )

$( singletons
    [d|
      constVNil :: Vec n N -> Vec (ConstZ n) N
      constVNil _ = VNil
      |]
 )

{-                                                                                                                                                 
    • Couldn't match kind ‘ConstZ n’ with ‘Z’                                                                                                                                                                       
      Expected kind ‘Vec (ConstZ n) N’, but ‘VNilSym0’ has kind ‘Vec Z N’                                                                                                                                           
    • In the type ‘VNilSym0’                                                                                                                                                                                        
      In the type family declaration for ‘ConstVNil’
-}

This also does not, but with a different error message (difference is pattern matching in constVNil):

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

        constZ :: N -> N
        constZ Z = Z
        constZ (S _) = Z

        type Vec :: N -> Type -> Type
        data Vec n a where
          VNil :: Vec 'Z a
          (:.) :: a -> Vec n a -> Vec ('S n) a
        |]
 )

$( singletons
    [d| 
      constVNil :: Vec n N -> Vec (ConstZ n) N
      constVNil VNil = VNil
      constVNil (_ :. _) = VNil
      |]
 )

{-
    • Illegal type synonym family application ‘ConstZ n’ in instance:                                                                                                                                               
        Apply                                                                                                                                                                                                       
          @(Vec n N)                                                                                                                                                                                                
          @(Vec (ConstZ n) N)                                                                                                                                                                                       
          (ConstVNilSym0 @n)                                                                                                                                                                                        
          a6989586621679129191                                                                                                                                                                                      
    • In the type instance declaration for ‘Apply’
-}

[RyanGlScott]

For what it's worth, I'm not sure that I would call these "primitive"—these are quite advanced uses of singletons! By and large, the singletons library works best when you promote "vanilla" Haskell code, where "vanilla" means "free of GADTs or type families" in this context. Making singletons work with non-vanilla Haskell code pushes GHC to its current limits, as you've seen.

This doesn't (only difference is the pattern matching in constZ:

Yes, this is because ConstZ n doesn't reduce to Z on its own, which is somewhat a somewhat counterintuitive property of how type families are implemented in GHC. In order to reduce, GHC must be able to tell that n is specifically equal to N or S n' (for some n'), and GHC can't know this from the kind signature forall n. Vec n N -> Vec (ConstZ n) N alone.

This also does not, but with a different error message (difference is pattern matching in constVNil):

This solves the problem in the previous example by explicitly pattern-matching on SVNil/(:%.), which is enough to make GHC's typechecker realize that n equals N or S n', respectively. It doesn't solve the problem of a type family appearing the head of the Apply instance, however.

[fpringle]

I found sort of a workaround, which is based on your comment here.

{-# LANGUAGE TemplateHaskell #-}

import Data.Singletons.TH
import Data.Singletons.TH.Options

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

        data Add m n r where
          AddZ :: Add Z m m
          AddS :: Add m n r -> Add (S m) n (S r)

        (++) :: N -> N -> N
        Z ++ n = n
        S m ++ n = S (m ++ n)

        type Vec :: N -> Type -> Type
        data Vec n a where
          VNil :: Vec 'Z a
          (:.) :: a -> Vec n a -> Vec ('S n) a
        |]
 )

$( singletons
    [d|
      append :: Add m n r -> Vec m a -> Vec n a -> Vec r a
      append AddZ VNil ys = ys
      append (AddS a) (x :. xs) ys = x :. append a xs ys
      |]
 )

type MkAdd :: forall m -> forall n -> Add m n (m ++ n)
type family MkAdd m n where
  MkAdd Z n = AddZ
  MkAdd (S m) n = AddS (MkAdd m n)

mkAddI :: forall m n. (SingI m) => Add m n (m ++ n)
mkAddI = mkAdd sing

mkAdd :: forall m n. Sing m -> Add m n (m ++ n)
mkAdd SZ = AddZ
mkAdd (SS m) = AddS (mkAdd m)

mkSAdd :: forall m n. Sing m -> Sing (MkAdd m n)
mkSAdd SZ = SAddZ
mkSAdd (SS m) = SAddS (mkSAdd m)

(+++) :: (SingI m) => Vec m a -> Vec n a -> Vec (m ++ n) a
(+++) = append mkAddI

type (+++) :: Vec m a -> Vec n a -> Vec (m ++ n) a
type (+++) (xs :: Vec m a) (ys :: Vec n a) = Append (MkAdd m n) xs ys

(%+++) ::
  forall m n a (vm :: Vec m a) (vn :: Vec n a).
  (SingI m) =>
  SVec vm ->
  SVec vn ->
  SVec (vm +++ vn)
(%+++) = sAppend (mkSAdd $ sing @m)

Downstream code that requires vector concatenation can then use Append, AppendSym0 etc in place of (+++) - making them promotion-friendly.
Helper functions can be defined converting the TH-generated code (using Add) into more friendly code (using ++) using the MkAdd machinery (e.g. in the term-level functions (+++) and (%+++), or the type-level function (+++).

Seeing as there's a direct correspondance between the cases of the original (++) function and the constructors of Add, I wonder if this could be automated somehow...

[RyanGlScott]

Nice! I'm pleasantly surprised at how useful that workaround is :)

[fpringle]

Me too :)

I also had to use a simliar datatype for working with the vectors:

$( withOptions defaultOptions {genSingKindInsts = False}
    $ singletons
      [d|
        type AddV :: Vec m a -> Vec n a -> Vec r a -> Type
        data AddV m n r where
          AddVZ :: AddV 'VNil r r
          AddVS :: forall t m n r. AddV m n r -> AddV (t :. m) n (t :. r)

        addVecs :: Add n m r -> Vec n a -> Vec m a -> Vec r a
        addVecs AddZ VNil ys = ys
        addVecs (AddS a) (x :. xs) ys = x :. addVecs a xs ys
        |]
 )