Singled records can behave counterintuitively

[RyanGlScott]

For the longest time, something about the way record selectors are singled has felt slightly off to me. I think the best way to illustrate the unease I feel is to point to this example:

newtype Unit = MkUnit { runUnit :: () }
-- runUnit :: Unit -> ()

f :: Unit -> ()
f = runUnit

Surprisingly, this code successfully promotes, but doesn't single: sF will fail to typecheck. What is going on here? The heart of the matter is that this is the definition of sRunUnit:

data instance Sing :: Unit -> Type where
  SMkUnit :: { sRunUnit :: Sing u } -> Sing (MkUnit u)

In other words,

sRunUnit :: Sing (MkUnit u) -> Sing u

For the rest of this issue, I will refer to this style of singling record selectors as the "traditional" approach. This approach is actually quite distinct from how most definitions are singled. For instance, compare sRunUnit to an alternative way to define a "record selector" for MkUnit (I put "record selector" in quotes because it's not really one, but it's as close as I can get without using record syntax):

runUnit2 :: Unit -> ()
runUnit2 (MkUnit unit) = unit

When singled, this becomes:

sRunUnit2 :: Sing (unit :: Unit) -> Sing (RunUnit2 unit)

For the rest of this issue, I will refer to this as the "manual" approach to singling record selectors. Unlike the traditional approach, the manual approach does not constrain the type of its argument (beyond saying that it should be of kind Unit), and it incorporates a type family into its return type.

What's even more interesting is that using the traditional runUnit causes f = runUnit to fail to single, but swapping runUnit out the its manual equivalent, runUnit2, makes f single successfully. That's because in the traditional definition of f:

sF :: Sing (unit :: Unit) -> Sing (F unit)
sF = sRunUnit

There is no constraint in scope that unit ~ MkUnit u (for some u), so sRunUnit fails to typecheck. On the other hand, sRunUnit2 requires no such constraint, so it happily typechecks.

To make things even stranger, the traditional approach to singling records is somewhat at odds with the way records are promoted. Here is the promoted version of runUnit:

-- type RunUnit :: Unit -> ()
type family RunUnit (unit :: Unit) :: () where
  RunUnit (MkUnit unit) = unit

In spirit, this is actually closer to the manual approach than the traditional one!

That's not to say that the traditional approach is totally useless. While I've demonstrated some scenarios where the manual approach wins out, there are other situations where the traditional approach is better:

1. Only the traditional definition can be used with record syntax (record construction, record updates, pattern matching, etc.).

2. In some scenarios, traditional singled records can avoid partiality. If you were to single the following data type:

   data Vec :: Type -> Nat -> Type where
     VNil :: Vec a Z
     (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)

   Then if sVhead and sVtail were defined traditionally, they would be total functions, as their type signatures would require that the first argument have type Sing (x :# xs) (i.e., passing SVNil would be a type error). If they were defined manually, however, they would be partial.

This seems to indicate to me that perhaps singletons should be offering both forms of records. If nothing else, singletons' own code would benefit from having the manual versions available, as there are many times where we have to jump through hoops to single code which uses newtype record selectors. If we did this, though, we'd have to answer the following questions:

1. What should the naming conventions for traditional and manual singled record selectors be?
2. If the naming convention for manual records ends up being different from what singletons currently offers, should we change the naming conventions for promoted records to match that of manual singled records? (If we don't, we'd have a discrepancy between the two, despite the fact that manual singled records would use these promoted records in their return types.)

Another option is to just observe this weirdness in the README, and require that anyone who wants to write functions like f above will have to define manual record selectors, well, manually. Currently, the README is rather silent about this point—the only oddity about records that it makes note of concerns record updates, which is a rather different problem.

[goldfirere]

Good point. My instinct is to give record selectors the "manual" form all the time. What are the drawbacks? I refute the head/tail drawback, because those selectors really are partial. Sure, singletons can cleverly make them total, but I don't think it's our job to do so.

[RyanGlScott]

What are the drawbacks?

Aside from the partiality bit, the only thing I can think of is:

Only the traditional definition can be used with record syntax (record construction, record updates, pattern matching, etc.).

And this would only ever occur in situations where the user explicitly wrote definitions like this:

sBlah :: Sing (MkUnit u) -> Sing u
sBlah (SMkUnit { sRunUnit = su }) = su

singletons, AFAICT, never generates definitions like this one via Template Haskell, since th-desugar effectively sanitizes away any explicit uses of records. To test this hypothesis, I disabled singletons' generation of singled (traditional) record selectors, and observed that all of the tests pass—even the Records test!

I'm not sure how many people are using traditional singled records at the moment, so I have no way to quantify the breakage that would result from removing them. But I do think that that would pretty much be the only real breakage.

[goldfirere]

I suppose there's no better way than this ticket to poll users.

Would ghc-proposals/ghc-proposals#148 fix this? With that proposal implemented, I think we could assign the record selector the type we want... I think.

[RyanGlScott]

Would ghc-proposals/ghc-proposals#148 fix this?

I doubt it would, to be honest. Wouldn't that require that forall (unit :: Unit). Sing unit -> Sing (RunUnit unit) be a subtype of forall (u :: ()). Sing (MkUnit u) -> Sing u?

[RyanGlScott]

Another point in favor of using the manual approach over the traditional (current) approach is that only the manual approach works for this program:

$(singletons [d|
  data X = X1 {y :: Symbol} | X2 {y :: Symbol}
  |])

Why? With the traditional approach, we'd generate the following definition for SX:

data SX :: X -> Type where
  SX1 :: {sY :: Sing n} -> SX (X1 n)
  SX2 :: {sY :: Sing n} -> SX (X2 n)

Notice that sY is given both the type SX (X1 n) -> Sing n and the type SX (X2 n) -> Sing n, which are incompatible. As a result, GHC errors out:

error:
    • Constructors SX1 and SX2 have a common field ‘sY’,
        but have different result types
    • In the data type declaration for ‘SX’

This isn't a contrived program that I made up, either—someone actually filed a bug report about this program in #180. Granted, #180 only went as far as promoting, not singling, this program, but it is still a realistic thing that a user might try.

[RyanGlScott]

Moreover, we don't necessarily need to generate both the manual and traditional record selectors when singling. We could make generating manual record selectors the default and offer the ability to switch back to traditional record selectors through a field in Options for those who really want it.

[RyanGlScott]

Hold on, my comment in #364 (comment) was perhaps too hasty. It turns out that singletons used to possess the ability to single multiple constructors with the same record name after all. As proof, this program:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Foo where

import Data.Singletons.TH
import GHC.TypeLits

$(singletons [d|
  data X = X1 {y :: Bool} | X2 {y :: Bool}
  |])

Compiles with singletons-2.3.1 (GHC 8.2.2), but not with any subsequent version of singletons. Whether that change was intended or not is unclear to me, but I discovered this because there is in fact code in the wild that uses this sort of thing: the perst2 library. This library singles a data type that has two constructors with the same record name here. Moreover, it also demonstrates that people have, in fact, used singled record selectors in manually-written pattern matches—see here.

[RyanGlScott]

Speaking of hasty comments, the fact that the program in #364 (comment) ever compiled is a complete fluke. singletons-2.3.1 happened to single X like this:

data SX :: X -> Type where
  SX1 :: z ~ 'X1 n => { sY :: Sing n } -> SX z
  SY1 :: z ~ 'X2 n => { sY :: Sing n } -> SX z

If you write that out by hand, then you can verify that that will compile with GHC 8.2.2 and later. On the other hand, subsequent versions of singletons will generate this code when singling X:

data SX :: X -> Type where
  SX1 :: { sY :: Sing n } -> SX ('X1 n)
  SY1 :: { sY :: Sing n } -> SX ('X2 n)

That will fail to compile on every version of GHC, even back to 8.2.2. So the fact that this program "regressed" between singletons versions is simply the result of the generated code no longer exploiting a workaround that avoids GHC#8673/GHC#12159.

This is not to say that we should scramble to go back to the old style of code generation. I recently learned that singled record selectors are broken in other ways. Notably, they don't support record updates in the way you'd expect:

λ> let i = Identity True in i { runIdentity = False }
Identity False
λ> let si = SIdentity STrue in si { sRunIdentity = SFalse }

<interactive>:6:29: error:
    • Record update for insufficiently polymorphic field:
        sRunIdentity :: Sing n
    • In the expression: si {sRunIdentity = SFalse}
      In the expression:
        let si = SIdentity STrue in si {sRunIdentity = SFalse}
      In an equation for ‘it’:
          it = let si = SIdentity STrue in si {sRunIdentity = SFalse}

And even on singletons-2.3.1, where the program in #364 (comment) compiled, GHC is treading on thin ice. sY apparently doesn't have a principal type:

λ> :t sY

<interactive>:1:1: error:
    • Cannot use record selector ‘sY’ as a function due to escaped type variables
      Probable fix: use pattern-matching syntax instead
    • In the expression: sY

---

In short, I am now of the belief that traditional record selectors for singled data types are borked, and we should avoid them in favor of manual record selectors. I'm not even sure if we can realistically offer manual record selectors as an optional feature. Consider this program:

$(withLocalOptions defaultOptions{ accursedUnutterableTraditionalRecordSelectors = True }
  singletons $ lift
  [d| data T = (:+:) { x :: Bool }
             | (:*:) { x :: Bool }
    |])

For the reasons noted above, we can't generate this code:

data ST :: T -> Type where
  (%:+:) :: { sX :: Sing b } -> ST ((:+:) b)
  (%:*:) :: { sX :: Sing b } -> ST ((:*:) b)

Since sX would have different types in each constructor. One alternative would be to give the record selector different names in each constructor, but what would the naming convention be? Some extremely half-baked ideas are:

1. Prefix/suffix the record selector name with the name of the constructor. But that won't work well in the above example, since the constructor name is infix and the selector name is prefix.
2. Distinguish the record selectors with numeric suffixes, e.g., sX1 and sX2. This is slightly more robust, but not much more so, since this would conflict with any code that singles functions named x1 and x2.

Yuck. Rather than deal with the headache of traditional record selectors, I'm inclined to just not generate them at all. Any objections?

[RyanGlScott]

I decided to be bold and submit #436, which replaces traditional record selectors with manual ones during singling.