Skip to content

Conversation

@OlivierBlanvillain
Copy link
Contributor

It appears that TypeParamRef-s that appear in types inside provablyDisjoint always come from local type binders. As a result, it's OK to consider types containing TypeParamRef-s to be fullyInstantiated and trust the result of isSameType at that point.

// `arg1` and `arg2` are fully instantiated.
def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] {
override def apply(x: Boolean, t: Type) =
x && {
Copy link
Member

@smarter smarter Apr 10, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand the comment above: "We can only trust a "no" from isSameType when both arg1 and arg2 are fully instantiated.". What does "trust" mean here? isSameType(tp1, tp2) returning false means "I wasn't able to prove that tp1 and tp2 are the same type", having or not having type variables in these types does not change that.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It means we interpret !isSameType(A, B) as "A and B are definetly different type" when the conditions in && { ... } are met. The alternative would be to write another recursive method provablyNotSameType in the same style as provablyDisjoint that would be used here to draw disjointness conclusions from invarant type parameters.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It means we interpret !isSameType(A, B) as "A and B are definetly different type"

Unfortunately that's not true, even if you exclude type variables, type parameters and abstract types. For example Nothing and Int & String are the same type, but the compiler doesn't know that and isSameType will return false.

The alternative would be to write another recursive method provablyNotSameType in the same style as provablyDisjoint that would be used here to draw disjointness conclusions from invarant type parameters.

That seems like a good way forward yeah.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The alternative would be to write another recursive method provablyNotSameType

It looks like scalac has something like this for deciding if it needs to emit an unchecked type test warning, this could be a good inspiration: https://github.com/scala/scala/blob/dfb8f7364a56fc01ad1eaea57980fba586ef6914/src/compiler/scala/tools/nsc/typechecker/Checkable.scala#L275
(we may in fact want to use this in our own unchecked type tests which are currently pretty broken: #8808)

@OlivierBlanvillain OlivierBlanvillain self-assigned this Apr 20, 2020
Copy link
Member

@smarter smarter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is worth getting in since it's a net improvement even if it needs more work.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants