为何需为特定类型计算的输出指定细化类型（或等价Aux类型）？

Great question! Let's break down why you need that explicit return type (or the equivalent Aux pattern) when working with this type-level Sum implementation.

First, let's recap the setup we're dealing with: we have a Sum trait (or type class) with an associated type Out that represents the result of the type-level addition. The apply method returns an instance of Sum where Out is refined to the actual sum type.

The Core Issue: Scala's Local Type Inference Limits #

When you write:

val x = Sum[_0, _1]

without an explicit return type, Scala's compiler does something that might seem counterintuitive at first: it infers x's type as the base Sum[_0, _1] (or just Sum, depending on the exact setup) — not the refined type Sum[_0, _1] { type Out = _1 }.

Scala's local type inference prioritizes inferring the most specific non-refined type by default. It doesn't automatically retain the refined Out type member in the variable's static type. So even though the runtime instance of x has a concrete Out type, the compiler only sees the abstract Out member from the base Sum trait when checking subsequent code.

Why This Breaks Subsequent Code #

When you try to run:

val y = Sum[x.Out, _1]

the compiler looks at x.Out and sees an abstract type (since x's static type is the base Sum). It has no way of knowing that x.Out is actually _1, so it can't resolve the implicit Sum instance needed for Sum[x.Out, _1] — hence the error.

How Explicit Return Types (or Aux) Fix This #

By specifying an explicit return type like:

val x: Sum[_0, _1] { type Out = _1 } = Sum[_0, _1]

or using the Aux pattern (which is just a type alias for the refined type):

type Aux[A, B, O] = Sum[A, B] { type Out = O }
val x: Aux[_0, _1, _1] = Sum[_0, _1]

you're telling the compiler exactly what x's static type is — including the concrete Out type member. Now, when you reference x.Out, the compiler knows it's _1, and can successfully resolve the implicit Sum instance for Sum[_1, _1].

Key Takeaway #

Type-level programming in Scala relies heavily on static type information. When dealing with types with associated members (like Sum's Out), you need to explicitly capture those refined types in your variable's static type — either via an explicit return type or the Aux pattern — because Scala's inference won't do it for you automatically. This gives the compiler the concrete type details it needs to carry out subsequent type-level computations.

内容的提问来源于stack exchange，提问作者allidoiswin