REPL does not fully normalize treeSort

[xianglic]

Load the TreeSort.aya in the test, then enter repl, run the following:

> .\aya.bat -i
Aya 0.34.0-SNAPSHOT (55cdeb6e48dba8988c2c092250604625547336d0)
λ> :l TreeSort.aya
In file C:\Users\92513\Downloads\AyaProver\bin\TreeSort.aya:59:7 ->

  57 │   private def aux (l : List A) (r : RBTree A) (dec_le : Decider A) : RBTree A elim l
  58 │   | [] => r
  59 │   | a :> l => aux l (repaint (insert a r dec_le)) dec_le
     │          ╰╯

Warning: The name `l' shadows a previous local definition from outer scope

λ> :normalize FULL
Normalization mode set to FULL
λ> tree_sortNat [ 3, 4, 1, 5, 2 ]
rbTreeToList {Nat} (repaint {Nat} (insert {Nat} 2 (repaint {Nat} (insert {Nat} 5 (repaint {Nat} (insert {Nat} 1 (repaint
{Nat} (insert_lemma {Nat} (\ p0 p1 ⇒ isZero (sub p0 p1)) 4 3 black rbLeaf rbLeaf (isZero (sub 3 4)))) (\ p0 p1 ⇒ isZero (sub
p0 p1)))) (\ p0 p1 ⇒ isZero (sub p0 p1)))) (\ p0 p1 ⇒ isZero (sub p0 p1)))) [  ]

Calling tree_sortNat [ 3, 4, 1, 5, 2 ] does not fully normalize the code, even if I set :normalize FULL. But if we copy the generated code and normalize it again, then it does normalize it:

λ> :{
| rbTreeToList {Nat} (repaint {Nat} (insert {Nat} 2 (repaint {Nat} (insert {Nat} 5 (repaint {Nat} (insert {Nat} 1 (repaint
| {Nat} (insert_lemma {Nat} (\\ p0 p1 ⇒ isZero (sub p0 p1)) 4 3 black rbLeaf rbLeaf (isZero (sub 3 4)))) (\\ p0 p1 ⇒ isZero (sub
| p0 p1)))) (\\ p0 p1 ⇒ isZero (sub p0 p1)))) (\\ p0 p1 ⇒ isZero (sub p0 p1)))) [  ]
| :}
[ 1, 2, 3, 4, 5 ]

🤔

[ice1000]

Reason: 1 becomes MetaLitTerm in the middle, and was not inferred to be the correct Nat. Therefore it is not reduced accordingly.