Kotlin / kotlin-spec

Kotlin Language Specification:
https://kotlinlang.org/spec
Apache License 2.0
387 stars 80 forks source link

Use of top type in smart cast analysis transfer function #119

Open leanderBehr opened 1 year ago

leanderBehr commented 1 year ago

In the definition of the transfer function, $\top$ is used for the second element of the type pair as the "default". As far as I understand, $\top$ this is Any? and in that position would mean that the expression is smart cast to non-nullable.

For example in the rule for x == null this would mean that approxNegationType(N) = approxNegationType(Any?) = Any. Am I misunderstanding this or should the $\top$ s be $\bot$ s?