normalizer: avoid possible infinite loop on maybe_unfold_head

[mtzguido]

No description provided.

[mtzguido]

Needed this to avoid a stack overflow on a Pulse rewrite. @aseemr does it look sensible to you?

[aseemr]

Hi Guido, looks reasonable to me. But if it is an fv or uinst node, wouldn't it match the cases before? What is the example term that loops?

[mtzguido]

The example I ran into was just maybe_unfold_head being called with a Tm_name. So it tries to split into head+args, the args are empty, and recurses on the head infinitely.

So this detects the empty args case to not make a recursive call and just tries to unfold the thing.

There's also he choice of calling maybe_unfold_head_fv on the term instead of just saying None, which I should have explained sorry. I think if the term is something like M.f <: ty then it will not match the previous two cases, and leftmost_head_and_args (which unascribes/unmetas) will return (M.f, []), but we should still try to unfold M.f. We could add a check here to only call maybe_unfold_head_fv on Tm_fvar/Tm_uinst, but since is the only client I thought it's just easier to remove the failwith and return None inside that function.