Fix test case Singletons.ReturnFunc

[goldfirere]

See test case.

[jstolarek]

The correct version of type signature for sReturnFunc is:

sReturnFunc ::
  forall (t_aG2q :: Nat_aG2c) (t_aG2r :: Nat_aG2c).
  Sing t_aG2q -> Sing t_aG2r -> Sing (Apply (ReturnFunc t_aG2q) t_aG2r)
sReturnFunc _ = SSucc

Notice how ReturnFunc gets its first parameter normally (ie. a normal function application), but then the over-saturated argument is applied with Apply (because ReturnFunc t_aG2q is a TyFun). That's tricky. I'm not touching this until we settle what to do with #12.

[goldfirere]

This doesn't seem so bad, actually. What if all singleton types just use Apply in their return type? Then, this one would work nicely, and the others would likely continue to work, no?

[jstolarek]

What if all singleton types just use Apply in their return type?

I'm afraid I don't understand what you mean by that. We already use Apply in singletonized return types:

    sZipWith ::
      forall (t :: TyFun a (TyFun b c -> *) -> *) (t :: [a]) (t :: [b]).
      (forall (t :: a) (t :: b).
       Data.Proxy.Proxy t
       -> Sing t -> Sing t -> Sing (Apply (Apply t t) t))
      -> Sing t -> Sing t -> Sing (ZipWith t t t)

Do you mean to always use Apply, so that ZipWith t1 t2 t3 becomes Apply (Apply (Apply ZipWith0 t1) t2) t3)?

[goldfirere]

Yes, that's exactly what I mean. Do you see a problem with that approach?

[jstolarek]

If that's possible I'd go for it. It would allow to remove horrible introduceApply function.

[goldfirere]

Yes... I was wondering why that function was necessary...

[jstolarek]

Yes... I was wondering why that function was necessary..

This function introduces Apply in the return Sing of a singletonized signature. It was implemented long before I implemented type-level symbols. However, I am not sure if it will be possible to remove it. When we promote RHSs of function definitions we can safely replace every AppE with call to Apply but with a type signature I think we still need to be selective - there's a lot of AppTs that are supposed to remain AppTs.

[jstolarek]

After looking at the code I don't see an elegant way of dealing with this. I only see a very inelegant way: after singletonizing the type signature we can unravel it, take the return value, unwrap the Sing, promote the remaining Sing parameter to use symbols and Apply, then wrap it back in Sing and ravel the type. Does that sound acceptable? Do you think there are situations when this would fail?

[goldfirere]

Wouldn't changing this line do the trick? We could just put a use of Apply there, and I think the problem is solved...

[jstolarek]

Hm... maybe? I'd have to try this out.

[jstolarek]

I made a few quick attempts at changing this line but with no success. Inserting Apply instead of normal application does not work, because f is a type, not a type level symbol. Adding a simple function that changes f to a symbol:

foo :: Type -> Type
foo (ConT n) = ConT $ promoteTySym n 0
foo t = t

leads to lots of compilation errors. Here's one of them:

src/Data/Singletons/List.hs:63:3:                                                                                             [108/1926]
    Could not deduce (ZipWith a0 b0 c0 t2 n1 n3
                      ~ ZipWith a0 b0 c0 t0 n1 n3)
    from the context (t3 ~ (':) a0 n n1)
      bound by a pattern with constructor
                 SCons :: forall (a_12 :: BOX)
                                 (z_ahrf :: [a_12])
                                 (n_ahrg :: a_12)
                                 (n_ahrh :: [a_12]).
                          z_ahrf ~ (':) a_12 n_ahrg n_ahrh =>
                          Sing a_12 n_ahrg -> Sing [a_12] n_ahrh -> Sing [a_12] z_ahrf,
               in an equation for `sZipWith'
      at src/Data/Singletons/List.hs:(63,3)-(98,4)
    or from (t4 ~ (':) b0 n2 n3)
      bound by a pattern with constructor
                 SCons :: forall (a_12 :: BOX)
                                 (z_ahrf :: [a_12])
                                 (n_ahrg :: a_12)
                                 (n_ahrh :: [a_12]).
                          z_ahrf ~ (':) a_12 n_ahrg n_ahrh =>
                          Sing a_12 n_ahrg -> Sing [a_12] n_ahrh -> Sing [a_12] z_ahrf,
               in an equation for `sZipWith'
      at src/Data/Singletons/List.hs:(63,3)-(98,4)
    NB: `ZipWith' is a type function, and may not be injective
    The type variable `t0' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Expected type: Sing
                     [c0]
                     (Apply
                        [c0]
                        [b0]
                        (Apply
                           (TyFun [b0] [c0] -> *)
                           [a0]
                           (Apply
                              (TyFun [a0] (TyFun [b0] [c0] -> *) -> *)
                              (TyFun a0 (TyFun b0 c0 -> *) -> *)
                              (ZipWithSym0 a0 b0 c0)
                              t2)
                           t3)
                        t4)
      Actual type: Sing
                     [c0]
                     ((':)
                        c0
                        (Apply c0 b0 (Apply (TyFun b0 c0 -> *) a0 t2 n) n2)
                        (ZipWith a0 b0 c0 t0 n1 n3))
    In the return type of a call of `SCons'
    In the expression:
      SCons (f_apQR x_apQS y_apQU) (sZipWith f_apQR xs_apQT ys_apQV)
    In an equation for `sZipWith':
        sZipWith f_apQR (SCons x_apQS xs_apQT) (SCons y_apQU ys_apQV)
          = SCons (f_apQR x_apQS y_apQU) (sZipWith f_apQR xs_apQT ys_apQV)

Perhaps this can be fixed easily, but at the moment I plan to focus on drafting the paper.

[goldfirere]

ReturnFunc now works.