The Singleton "kind" is not an upper bound

[Blaisorblade]

A few of us discussed this, but it seems we lack an issue for it. Quoting from #4942:

If A <: Singleton and B <: Singleton, it follows that A | B <: Singleton, but for instance 1 | 2 is not actually a singleton type.

In fact, already in Scala 2 we can exploit this and write the questionable

  def f[Bound, A <: Bound, B <: Bound](cond: Boolean, a: A, b: B): Bound = if (cond) a else b
  def g(cond: Boolean): Singleton = f[Singleton, 1, 2](cond, 1, 2)

In Dotty we also get the clearly broken:

  def f[Bound, A <: Bound, B <: Bound](cond: Boolean, a: A, b: B): (A | B) & Bound = if (cond) a else b
  def g(cond: Boolean): Singleton = f[Singleton, 1, 2](cond, 1, 2)
  // def h(cond: Boolean): (1|2) & Singleton = f[Singleton, 1, 2](cond, 1, 2) // doesn't compile
  type || [A, B] = A | B
  type Boo = 0 || 1

  // def h1(cond: Boolean): (1||2) & Singleton = f[Singleton, 1, 2](cond, 1, 2) // still fails because 1 | 2 is collapsed eagerly

def f2[Bound, A <: Bound, B <: Bound](cond: Boolean, a: A, b: B): (A || B) & Bound = if (cond) a else b

def h2(cond: Boolean): (1||2) & Singleton = f2[Singleton, 1, 2](cond, 1, 2)
def h2(cond: Boolean): Int(1) Any Int(2) & Singleton

Only h fails, and just because we forbid 1|2 syntactically for now (#1551), so h2 works.
Since Singleton is special in core typing rules, @odersky suggested this endangers even soundness. Ad-hoc restrictions (say, forbidding Singleton as a type argument) seems a losing whack-a-mole game.

Discussing this with @odersky today, we figured that Singleton behaves like a kind that can't be expressed via upper bounds, so we should consider something like an annotation or a modifier (tho modifiers on type variables don't exist yet).

Migration isn't easy, but one can easily support simple use cases of form [X <: Singleton] or even [X <: Foo with Singleton]. According to @nicolasstucki, even type SingAlias = Singleton; def foo[X <: Foo with SingAlias] doesn't currently work.

Paging @milessabin and @soronpo, as this affects SIP-23.

[Blaisorblade]

Marked with prio:high because @odersky said this is used relatively often.

[milessabin]

The use of Singleton bounds in SIP 23 and elsewhere in Scala 2 is almost entirely to influence type inference rather than to express a meaningful subtype relationship.

I'd be open to there being an alternative mechanism for doing that.

[soronpo]

The use of Singleton bounds in SIP 23 and elsewhere in Scala 2 is almost entirely to influence type inference rather than to express a meaningful subtype relationship.
I'd be open to there being an alternative mechanism for doing that.

And while we're at it, perhaps find a way to solve scala/bug#10838

[odersky]

The use of Singleton bounds in SIP 23 and elsewhere in Scala 2 is almost entirely to influence type inference rather than to express a meaningful subtype relationship.

Yes, that seems to be the case. I believe the only necessary use case of Singleton is to signal "don't widen this type argument". Expressing this with a subtype relationship is wrong. We need a label/modifier on the type parameter instead. Something like

def f[singleton T]

It would mean complicating the syntax by allowing a modifier on type parameters. Does anybody see an alternative way to express this?

[milessabin]

Does anybody see an alternative way to express this?

We have at least two areas where we want to be able to influence inference: type inference, as here (I suspect that there will more cases than just "don't widen" to be found if we go looking); and also term inference, as in implicit search.

My hunch is that it would be worth exploring the idea of a something like a tactic language to deal with both of these.

[milessabin]

A few examples in addition to inferring a singleton type if possible,

• Infer a concrete subtype of an ADT or infer the super type?
• Infer Nothing or not?
• Infer Any or not?
• Infer Product with Serializable or not?

I'm sure there are plenty more ...

In all these cases we can pick a most likely option, but there will be a significant number of scenarios where the most likely option isn't the right one.

Parenthetically, we need to be careful not to throw the baby out with the bath water ... there are cases where we want to accept only singleton typed terms, ie. where we want to ensure we have a stable value.

[odersky]

Parenthetically, we need to be careful not to throw the baby out with the bath water ... there are cases where we want to accept only singleton typed terms, ie. where we want to ensure we have a stable value.

Indeed. Right now, a typical pattern would be like this:

def f[U <: Universe with Singleton](m: Mirror[U]): U#Tree = ...

The "only singleton type" guarantee is important to ensure that U#Tree is well-formed. What we are trying to do here is pass a path as an argument, but as a type, not as a term. Maybe we can express this more directly?

def f[u.type <: Universe](m: Mirror[u.type]): u.Tree

The scheme would be to have a limited form of type pattern in type parameter binding position. A type pattern is either a type name or a term name followed by .type. In the second case, i.e.

x.type <: A

the term name x introduces an erased value of type A. This means no actual argument needs to be passed and x can be used only as a type prefix, never as a term prefix.

[milessabin]

I think that's a good example of how type and term inference are related. Couldn't we have something like,

def f(m: Mirror[u.type])(implicit u: Universe): u.Tree = ...

[milessabin]

Or, for that matter,

def f(implicit u: Universe)(m: Mirror[u.type]): u.Tree = ...

[odersky]

We can't have this, since u is used before being defined, and I fear that would be hard to change.

def f(m: Mirror[u.type])(implicit u: Universe): u.Tree = ...

But we could have the second version:

def f(implicit erased u: Universe)(m: Mirror[u.type]) u.Tree = ...

It's not completely equivalent, since it does not allow us to infer u from m, but that looks like a minor inconvenience.

So maybe the answer is: just deprecate Singleton instead of trying to fix it?

[milessabin]

It's not completely equivalent, since it does not allow us to infer u from m

This is something that's been bugging me for some time now.

Why is it possible that in this case,

def foo[Eariler](later: Foo[Earlier]) ...

we can infer the Earlier from later, whereas in this case,

def foo(implicit earlier: Whatever)(later: Foo[earlier.type]) ...

we can't infer earlier from later?