Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Found semi-reduced form, required reduced form #16081

Open
s5bug opened this issue Sep 21, 2022 · 3 comments
Open

Found semi-reduced form, required reduced form #16081

s5bug opened this issue Sep 21, 2022 · 3 comments
Labels
area:match-types area:typer itype:bug

Comments

@s5bug
Copy link

s5bug commented Sep 21, 2022

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.)
@s5bug s5bug added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Sep 21, 2022
@soronpo
Copy link
Contributor

soronpo commented Sep 21, 2022

Your goal will probably break the compiler, even if this issue is resolved ☺️

@s5bug
Copy link
Author

s5bug commented Sep 21, 2022

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 :)

@jchyb jchyb added area:typer area:match-types and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Sep 21, 2022
@jchyb
Copy link
Contributor

jchyb commented Sep 21, 2022

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 b1b1dfd):

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
area:match-types area:typer itype:bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@s5bug @soronpo @jchyb