feat: change ite and dite argument order

Motivation: make sure `propagateExpectedType` heuristic is applied in
the new frontend when processing them.

src/Init/Core.lean

@@ -849,12 +849,12 @@ isFalse notFalse
 
 -- We use "dependent" if-then-else to be able to communicate the if-then-else condition
 -- to the branches
-@[macroInline] def dite (c : Prop) [h : Decidable c] {α : Sort u} : (c → α) → (¬ c → α) → α :=
+@[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] : (c → α) → (¬ c → α) → α :=
 fun t e => Decidable.casesOn h e t
 
 /- if-then-else -/
 
-@[macroInline] def ite (c : Prop) [h : Decidable c] {α : Sort u} (t e : α) : α :=
+@[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α :=
 Decidable.casesOn h (fun hnc => e) (fun hc => t)
 
 namespace Decidable
@@ -1717,7 +1717,7 @@ match (propDecidable (Nonempty α)) with
 
 noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
   (h : Nonempty α) : {x : α // Exists (fun (y : α) => p y) → p x} :=
-@dite (Exists (fun (x : α) => p x)) (propDecidable _) _
+@dite _ (Exists (fun (x : α) => p x)) (propDecidable _)
   (fun (hp : Exists (fun (x : α) => p x)) =>
     show {x : α // Exists (fun (y : α) => p y) → p x} from
     let xp := indefiniteDescription _ hp;

src/Init/Data/Repr.lean

@@ -24,7 +24,9 @@ instance : HasRepr Bool :=
 ⟨fun b => cond b "true" "false"⟩
 
 instance {p : Prop} : HasRepr (Decidable p) :=
-⟨fun b => @ite p b _ "true" "false"⟩
+⟨fun h => match h with
+  | Decidable.isTrue _  => "true"
+  | Decidable.isFalse _ => "false"⟩
 
 protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String
 | b,     []    => ""

src/Init/Data/ToString.lean

@@ -34,8 +34,9 @@ instance : HasToString Bool :=
 ⟨fun b => cond b "true" "false"⟩
 
 instance {p : Prop} : HasToString (Decidable p) :=
--- Remark: type class inference will not consider local instance `b` in the new Elaborator
-⟨fun b => @ite p b _ "true" "false"⟩
+⟨fun h => match h with
+  | Decidable.isTrue _  => "true"
+  | Decidable.isFalse _ => "false"⟩
 
 protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String
 | b,     []    => ""

src/library/app_builder.cpp

@@ -963,7 +963,7 @@ expr mk_ite(type_context_old & ctx, expr const & c, expr const & t, expr const &
     expr t_type   = ctx.infer(t);
     level u       = get_level(ctx, t_type);
     return mk_app(mk_constant(get_ite_name(), {u}),
-                  {c, *dec_c_val, t_type, t, e});
+                  {t_type, c, *dec_c_val, t, e});
 }
 
 expr mk_id(type_context_old & ctx, expr const & type, expr const & h) {

stage0/src/library/app_builder.cpp

@@ -963,7 +963,7 @@ expr mk_ite(type_context_old & ctx, expr const & c, expr const & t, expr const &
     expr t_type   = ctx.infer(t);
     level u       = get_level(ctx, t_type);
     return mk_app(mk_constant(get_ite_name(), {u}),
-                  {c, *dec_c_val, t_type, t, e});
+                  {t_type, c, *dec_c_val, t, e});
 }
 
 expr mk_id(type_context_old & ctx, expr const & type, expr const & h) {

tests/lean/run/doNotation1.lean

@@ -99,7 +99,7 @@ def pred2 (x : Nat) : IO Bool :=
 pure $ x > 0
 
 def tst5 (x : Nat) : IO (Option Nat) :=
-if x > 10 then pure x else pure (x-1)
+if x > 10 then pure x else pure none
 
 syntax [doHash] "#":max : term
 

tests/lean/run/elabIte.lean

@@ -0,0 +1,4 @@
+new_frontend
+
+def f (x y : Nat) : Option Nat :=
+if x > y then x else none