scala3
scala3 copied to clipboard
Published
20 hours ago •
scala
scala
Found semi-reduced form, required reduced form
Compiler version
3.2.0
Minimized code
type Range[From <: Int, To <: Int] <: Int = (To - From) match {
case 0 => To
case 1 => From | To
// Binary tree-ish thing instead of easy recursion to save stack space
case _ => Range[From, From + ((To - From) / 2)] | Range[(From + 1) + ((To - From) / 2), To]
}
(0: Range[0, 22]) // => 0
(0: Range[0, 23]) // [E007] Type Mismatch Error
Output
-- [E007] Type Mismatch Error: -------------------------------------------------
1 |(0: Range[0, 23])
| ^^^^^^^^^^^^^^^
|Found: Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
|
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
|
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
|
| ]
|) | (Range[(12 : Int), (12 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int)] |
| Range[(12 : Int) + (1 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int),
|
| (17 : Int)
|
| ]
|
| | (Range[(18 : Int), (18 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int)] |
| Range[(18 : Int) + (1 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int),
|
| (23 : Int)
|
| ]
|
|))
|Required: (0 : Int) | (1 : Int) | (2 : Int) | ((3 : Int) | (4 : Int) | (5 : Int)) | (
|
| (6 : Int)
| (7 : Int) | (8 : Int) | ((9 : Int) | (10 : Int) | (11 : Int))) | ((12 : Int)
|
|
| (13 : Int) | (14 : Int) | ((15 : Int) | (16 : Int) | (17 : Int)) | ((18 : Int)
|
|
| (19 : Int) | (20 : Int) | ((21 : Int) | (22 : Int) | (23 : Int))))
|-----------------------------------------------------------------------------
| Explanation (enabled by `-explain`)
|- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
|
| Tree: 0:Range[0.type, 23.type]
| I tried to show that
| Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) | (Range[(12 : Int), (12 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int)] |
| Range[(12 : Int) + (1 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int),
| (17 : Int)
| ]
| | (Range[(18 : Int), (18 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int)] |
| Range[(18 : Int) + (1 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int),
| (23 : Int)
| ]
| ))
| conforms to
| (0 : Int) | (1 : Int) | (2 : Int) | ((3 : Int) | (4 : Int) | (5 : Int)) | (
| (6 : Int)
| | (7 : Int) | (8 : Int) | ((9 : Int) | (10 : Int) | (11 : Int))) | ((12 : Int)
| |
| (13 : Int) | (14 : Int) | ((15 : Int) | (16 : Int) | (17 : Int)) | ((18 : Int)
| |
| (19 : Int) | (20 : Int) | ((21 : Int) | (22 : Int) | (23 : Int))))
| but the comparison trace ended with `false`:
|
| ==> Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) | (Range[(12 : Int), (12 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int)] |
| Range[(12 : Int) + (1 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int),
| (17 : Int)
| ]
| | (Range[(18 : Int), (18 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int)] |
| Range[(18 : Int) + (1 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int),
| (23 : Int)
| ]
| )) <: (0 : Int) | (1 : Int) | (2 : Int) | ((3 : Int) | (4 : Int) | (5 : Int)) | (
| (6 : Int)
| | (7 : Int) | (8 : Int) | ((9 : Int) | (10 : Int) | (11 : Int))) | ((12 : Int)
| |
| (13 : Int) | (14 : Int) | ((15 : Int) | (16 : Int) | (17 : Int)) | ((18 : Int)
| |
| (19 : Int) | (20 : Int) | ((21 : Int) | (22 : Int) | (23 : Int))))
| ==> Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) | (Range[(12 : Int), (12 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int)] |
| Range[(12 : Int) + (1 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int),
| (17 : Int)
| ]
| | (Range[(18 : Int), (18 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int)] |
| Range[(18 : Int) + (1 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int),
| (23 : Int)
| ]
| )) <: Nothing
| ==> Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) <: Nothing
| ==> Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) <: Nothing
| ==> Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)] <: Nothing
| ==> Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)] <: Nothing
| ==> Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] <: Nothing
| ==> Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] <: Nothing
| ==> lub(<notype>, <notype>, canConstrain=false, isSoft=true)
| <== lub(<notype>, <notype>, canConstrain=false, isSoft=true) = <notype>
| ==> lub(<notype>, <notype>, canConstrain=false, isSoft=true)
| <== lub(<notype>, <notype>, canConstrain=false, isSoft=true) = <notype>
| ==> Range[(0 : Int), (0 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int) -
| (0 : Int)
| ) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)
|
| - (0 : Int)) / (2 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] <: Nothing
| ==> Range[(0 : Int), (0 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int) -
| (0 : Int)
| ) / (2 : Int)] <: Nothing
| ==> Range[(0 : Int), (0 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int) -
| (0 : Int)
| ) / (2 : Int)] <: Nothing
| ==> lub(<notype>, <notype>, canConstrain=false, isSoft=true)
| <== lub(<notype>, <notype>, canConstrain=false, isSoft=true) = <notype>
| ==> (0 : Int) | (0 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int) -
| (0 : Int)
| ) / (2 : Int) <: Nothing
| ==> Int <: Nothing in frozen constraint
| <== Int <: Nothing in frozen constraint = false
| ==> (0 : Int) <: Nothing
| ==> Int <: Nothing (left is approximated)
| <== Int <: Nothing (left is approximated) = false
| <== (0 : Int) <: Nothing = false
| <== (0 : Int) | (0 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int) -
| (0 : Int)
| ) / (2 : Int) <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int) -
| (0 : Int)
| ) / (2 : Int)] <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int) -
| (0 : Int)
| ) / (2 : Int)] <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int) -
| (0 : Int)
| ) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)
|
| - (0 : Int)) / (2 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)] <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)] <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) | (Range[(12 : Int), (12 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int)] |
| Range[(12 : Int) + (1 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int),
| (17 : Int)
| ]
| | (Range[(18 : Int), (18 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int)] |
| Range[(18 : Int) + (1 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int),
| (23 : Int)
| ]
| )) <: Nothing = false
| <== Range[(0 : Int), (0 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int)] |
| Range[(0 : Int) + (1 : Int) + ((5 : Int) - (0 : Int)) / (2 : Int), (5 : Int)]
| | (Range[(6 : Int), (6 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int)] |
| Range[(6 : Int) + (1 : Int) + ((11 : Int) - (6 : Int)) / (2 : Int), (11 : Int)
| ]
| ) | (Range[(12 : Int), (12 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int)] |
| Range[(12 : Int) + (1 : Int) + ((17 : Int) - (12 : Int)) / (2 : Int),
| (17 : Int)
| ]
| | (Range[(18 : Int), (18 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int)] |
| Range[(18 : Int) + (1 : Int) + ((23 : Int) - (18 : Int)) / (2 : Int),
| (23 : Int)
| ]
| )) <: (0 : Int) | (1 : Int) | (2 : Int) | ((3 : Int) | (4 : Int) | (5 : Int)) | (
| (6 : Int)
| | (7 : Int) | (8 : Int) | ((9 : Int) | (10 : Int) | (11 : Int))) | ((12 : Int)
| |
| (13 : Int) | (14 : Int) | ((15 : Int) | (16 : Int) | (17 : Int)) | ((18 : Int)
| |
| (19 : Int) | (20 : Int) | ((21 : Int) | (22 : Int) | (23 : Int)))) = false
|
| The tests were made under the empty constraint
-----------------------------------------------------------------------------
1 error found
Expectation
At least (0: Range[0, 23]) compiles. (The goal being RangeL[0L, 4294967296L] working for Longs; can possibly split Range into more branches for that.)
Your goal will probably break the compiler, even if this issue is resolved ☺️
Oh, certainly! But I'd love to know why this breaks, and I'd love even more to find out how far I can push this once it's fixed :)
I have played around with it, and what's interesting is that 0: Range[0, 23] (without parentheses) seems to work (both in repl and scalac, tested on b1b1dfdac832270fe2414569fad921c17ebd0fb6):
val res6: Range[0, 0 + (2 - 0) / 2] | Range[0 + 1 + (2 - 0) / 2, 2] | (
Range[3, 3 + (5 - 3) / 2]
| Range[3 + 1 + (5 - 3) / 2, 5]) | (Range[6, 6 + (8 - 6) / 2] |
Range[6 + 1 + (8 - 6) / 2, 8]
| (Range[9, 9 + (11 - 9) / 2] | Range[9 + 1 + (11 - 9) / 2, 11])) | (
Range[12, 12 + (14 - 12) / 2]
| Range[12 + 1 + (14 - 12) / 2, 14] | (Range[15, 15 + (17 - 15) / 2] |
Range[15 + 1 + (17 - 15) / 2, 17]
) | (Range[18, 18 + (20 - 18) / 2] | Range[18 + 1 + (20 - 18) / 2, 20] | (
Range[21, 21 + (23 - 21) / 2]
| Range[21 + 1 + (23 - 21) / 2, 23]))) = 0
However this only works up to a point as well, with 0: Range[0, 128] being the first one to break in the exact same manner as reported above. To me it all sounds like a stack overflow that is being incorrectly fallbacked into a type mismatch error.
