Warning against irrelevant dependent typing

Language Design
1

When using dependent typing (DT), especially for DT-beginners, it’s easy to make common mistakes like referencing a type that hold no real value. E.g.:

trait Bar{type Out}
class Foo(bar: Bar):
  type Out = bar.Out

IMO, the Out in Foo in this case never provides something relevant, and should generate a warning. Maybe even suggest a possible solution:

trait Bar{type Out}
class Foo[B <: Bar](bar: B):
  type Out = bar.Out

OK, you may think that this is very obvious and there is no point in making a warning. But, due to code desugaring, such references may also happen without us noticing. For example, as seen in issue #13580, a given .. with statement is desugared into a class with an argument:

trait IntWidth {type Out}
given IntWidth with {type Out = 155}

trait IntCandidate {type Out}
given (using w: IntWidth): IntCandidate with {type Out = w.Out} //desugared into class XYZ(w: IntWidth)...

val x = summon[IntCandidate]
val xx = summon[x.Out =:= 155] //error

This is very confusing because how we are used to write dependent implicit defs:

implicit def xyz(using w: IntWidth): IntCandidate {type Out = w.Out} = ??? //will work as expected
3 Likes