Typecheck patch

[HalflingHelper]

In lecture Matei found a weird bug related to this proof

import UInt
import List

lemma rev_rev_lemma2: all U:type. all xs : List<U>, ys :List<U>.
    reverse(reverse(xs) ++ ys) = reverse(ys) ++ reverse(reverse(xs))
proof
    arbitrary U:type
    induction List<U>
    case [] {
        arbitrary ys:List<U>
        expand reverse
        expand operator ++
        replace append_empty
        .
    }
    case node(x, xs') assume IH {
        arbitrary ys:List<U>
        expand reverse
        expand 2* operator ++
        replace IH[node(x, ys)]
        expand reverse
        replace IH[[x]]
        evaluate
    }
end

The problem was twofold

1. When the last evaluate is commented out, the last reverse(reverse(xs')) was admitted from the goal printed out in the proof advice. This was fixed by updating type_check_call_funty to handle associative operators in the case where it has to infer a TermInst.
2. The evaluate wouldn't evaluate the RHS, due to missing TermInst nodes that should have wrapped the ++ operator. I was able to fix this by typechecking the formula after performing a rewrite. However, the fact that this wasn't a concern before makes me wonder if there's an alternate fix that can happen when related to somewhere we do something wrong with associativity. The fact that tests haven't failed before now makes me think that that may be the case, because then we should see issues pop up elsewhere, in almost any proof where we do a rewrite with anything related to append.

I don't know if you have thoughts of another place to fix the second issue, I haven't been able to fix it otherwise, I'm going to spend some time trying to replicate the error in a simpler proof.

[HalflingHelper]

Yeah hold off on this, I think I found a deeper root cause

[HalflingHelper]

Looks like the problem was that reduce_associative assumed that the rator was a Var node, but it can sometimes be a TermInst. Just reusing fun works, but that might also create problems, maybe better is to check if fun is a TermInst and if so make rator
TermInst(loc, Var(...), type_args, inferred

I'm not sure what the original motivation was, do_recursive_call is fine with reusing fun.