This will get you a compiler crash in every version of Scala 2.x. I'm surprised I never noticed this before. Is there a ticket for this already? trait X { type Z } trait Y { type Z } type A = X { type Z = Int } type B = Y { type Z = Char } implicitly[A with B =:= B with A]
-
Show this thread
-
This Tweet is unavailable.
-
First, we don’t have a perfect story, but type equality is transitive *if you construct the proof* by explicitly using the (A with B)
#Z. It’s a bit like the difference between “definitional” and “propositional” equality, tho both are transitive there.1 reply 0 retweets 1 like -
Second, (A with B) is empty, so (A with B)
#Z should be rejected when actually using it. One bugfix from Martin here (https://github.com/lampepfl/dotty/pull/4036 …) has stalled (in part my fault), I’ll check what happens here.1 reply 0 retweets 2 likes
Replying to @Blaisorblade @contrarivariant
Appears to make some sense, but I'll have to spend some time thinking about it some more... ;)
4:54 AM - 20 Aug 2018
from Stockport, England
0 replies
0 retweets
0 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.