Type inference generalizes ADTs too eagerly, giving up type precision too easily

[anatoliykmetyuk]

The following works though shouldn't:

sealed trait Nat
case object Z extends Nat
case class S[N <: Nat](val pred: N) extends Nat

@main def Test1 =
  class Partially[M](m: M)
    def result(m1: M) = println(s"$m and $m1")
  val x = Partially(S(S(Z))).result(S(Z))
  // Typer:
  // val x: Unit =
  //   new Partially[S[(Nat & Product & Serializable)]](
  //     S.apply[(Nat & Product & Serializable)](S.apply[Z$](Z))
  //   ).result(S.apply[(Nat & Product & Serializable)](Z))

I would expect result to be callable only on S(S(Z)). Note the typer output (as reported by-Xprint:frontend): the type parameter of new Partially is S[(Nat & Product & Serializable)] though should be S[S[Z]].

The following reports an error properly:

@main def Test2 =
  class Partially[M](m: M)
    def result(m1: M) = println(s"$m and $m1")
  val x = Partially(S(S(Z)))
  x.result(S(Z))
  // Typer:
  // val x: Partially[S[S[Z$]]] =
  //   new Partially[S[S[Z$]]](S.apply[S[Z$]](S.apply[Z$](Z)))
  // x.result(S.apply[S[Z$]](Z))

Error:

-- [E007] Type Mismatch Error: /Users/anatolii/Projects/dotty/pg/nats/Test.scala:19:13
19 |  x.result(S(Z))
   |             ^
   |             Found:    Z.type
   |             Required: S[object Z]
result of /Users/anatolii/Projects/dotty/pg/nats/Test.scala after frontend:

Evidently type inference tries its best to compile as wide range of expressions as possible here, readily giving up type precision (and hence type safety) as shown above.

Another example:

@main def Test3 =
  given Z.type = Z
  given [P <: Nat](given p: P): S[P] = S(p)

  def f[N <: Nat](n: N)(given m: N) = println(s"n=$n ; m=$m")
  f(S(S(Z)))
  // Typer:
  // f[S[(Nat & Product & Serializable)]](
  //   S.apply[(Nat & Product & Serializable)](S.apply[Z$](Z))
  // )(given_S_P[(Nat & Product & Serializable)](given_))

Outputs:

n=S(S(Z)) ; m=S(Z)

Probably what happens here is the easiest to resolve Nat is resolved and the type parameter to f is generalised to fit both the passed and the resolved argument.

Works without givens as well – the below passes the compilation:

@main def Test4 =
  def f[N <: Nat](n: N)(m: N) = println(s"n=$n ; m=$m")
  f(S(S(Z)))(S(Z))
  // Typer:
  // f[S[(Nat & Product & Serializable)]](
  //   S.apply[(Nat & Product & Serializable)](S.apply[Z$](Z))
  // )(S.apply[(Nat & Product & Serializable)](Z))

The type is inferred precisely if both arguments have the same type (see typer output below):

@main def Test5 =
  def f[N <: Nat](n: N)(m: N) = println(s"n=$n ; m=$m")
  f(S(S(Z)))(S(S(Z)))
  // f[S[S[Z$]]](S.apply[S[Z$]](S.apply[Z$](Z)))(
  //   S.apply[S[Z$]](S.apply[Z$](Z))
  // )

I can imagine this behaviour to be a problem for type-safe programming: it is way to easy to bargain with the type system here to get the types that will make the program compile.

/cc @AleksanderBG

[smarter]

Evidently type inference tries its best to compile as wide range of expressions as possible here, readily giving up type precision (and hence type safety) as shown above.

Type inference job is to find type arguments that make the expression typecheck. If such arguments exist, you cannot assume that type inference will not find them (and you can't assume that the user won't write them himself either), so this is not a type safety issue.

[bishabosha]

another case for precise modifier, or just use type parameters more carefully