fix(frontends/lean/parser): make sure imax and max level arguments are parsed using the same precendence we use to parse application arguments

This commit addresses an issue raised by @digama0 on the Lean slack channel.

library/init/category/alternative.lean

@@ -7,12 +7,12 @@ prelude
 import init.logic init.category.applicative
 universes u v
 
-class has_orelse (f : Type u → Type v) : Type (max u+1 v) :=
+class has_orelse (f : Type u → Type v) : Type (max (u+1) v) :=
 (orelse  : Π {α : Type u}, f α → f α → f α)
 
 infixr ` <|> `:2 := has_orelse.orelse
 
-class alternative (f : Type u → Type v) extends applicative f, has_orelse f : Type (max u+1 v) :=
+class alternative (f : Type u → Type v) extends applicative f, has_orelse f : Type (max (u+1) v) :=
 (failure : Π {α : Type u}, f α)
 
 section

library/init/category/applicative.lean

@@ -15,17 +15,17 @@ class has_pure (f : Type u → Type v) :=
 @[reducible, inline] def pure {f : Type u → Type v} [has_pure f] {α : Type u} : α → f α :=
 has_pure.pure f
 
-class has_seq (f : Type u → Type v) : Type (max u+1 v) :=
+class has_seq (f : Type u → Type v) : Type (max (u+1) v) :=
 (seq  : Π {α β : Type u}, f (α → β) → f α → f β)
 
 infixl ` <*> `:60 := has_seq.seq
 
-class has_seq_left (f : Type u → Type v) : Type (max u+1 v) :=
+class has_seq_left (f : Type u → Type v) : Type (max (u+1) v) :=
 (seq_left : Π {α β : Type u}, f α → f β → f α)
 
 infixl ` <* `:60  := has_seq_left.seq_left
 
-class has_seq_right (f : Type u → Type v) : Type (max u+1 v) :=
+class has_seq_right (f : Type u → Type v) : Type (max (u+1) v) :=
 (seq_right : Π {α β : Type u}, f α → f β → f β)
 
 infixl ` *> `:60  := has_seq_right.seq_right

library/init/category/functor.lean

@@ -11,7 +11,7 @@ universes u v
 section
 set_option auto_param.check_exists false
 
-class has_map (f : Type u → Type v) : Type (max u+1 v) :=
+class has_map (f : Type u → Type v) : Type (max (u+1) v) :=
 (map : Π {α β : Type u}, (α → β) → f α → f β)
 (map_const : Π {α β : Type u}, α → f β → f α := λ α β, map ∘ const β)
 
@@ -19,7 +19,7 @@ infixr ` <$> `:100 := has_map.map
 infixr ` <$ `:100  := has_map.map_const
 infixr ` $> `:100  := λ α a b, b <$ a
 
-class functor (f : Type u → Type v) extends has_map f : Type (max u+1 v) :=
+class functor (f : Type u → Type v) extends has_map f : Type (max (u+1) v) :=
 (map_const_eq : ∀ {α β : Type u}, @map_const α β = map ∘ const β . control_laws_tac)
 -- `functor` is indeed a categorical functor
 (id_map       : Π {α : Type u} (x : f α), id <$> x = x)

library/init/category/monad.lean

@@ -23,7 +23,7 @@ infixl ` >> `:55  := has_bind.and_then
 section
 set_option auto_param.check_exists false
 
-class monad (m : Type u → Type v) extends applicative m, has_bind m : Type (max u+1 v) :=
+class monad (m : Type u → Type v) extends applicative m, has_bind m : Type (max (u+1) v) :=
 (map := λ α β f x, x >>= pure ∘ f)
 (seq := λ α β f x, f >>= (<$> x))
 (bind_pure_comp_eq_map : ∀ {α β : Type u} (f : α → β) (x : m α), x >>= pure ∘ f = f <$> x  . control_laws_tac)

src/frontends/lean/parser.cpp

@@ -690,7 +690,7 @@ level parser::parse_max_imax(bool is_max) {
     next();
     buffer<level> lvls;
     while (curr_is_identifier() || curr_is_numeral() || curr_is_token(get_lparen_tk())) {
-        lvls.push_back(parse_level());
+        lvls.push_back(parse_level(get_max_prec()));
     }
     if (lvls.size() < 2) {
         return parser_error_or_level(

tests/lean/run/t2.lean

@@ -5,5 +5,5 @@ universe variable u
 #print raw Type.{2}
 #print raw Type.{l+1}
 #print raw Type.{max l u 1}
-#print raw Type.{imax l+1 u 1}
-#print raw Type.{imax l+1 l u}
+#print raw Type.{imax (l+1) u 1}
+#print raw Type.{imax (l+1) l u}