F* seems to diverge on this example consuming a lot of memory

[nikswamy]

https://github.com/FStarLang/FStar/blob/master/ulib/experimental/Steel.FractionalAnchoredPreorder.fst#L485

[aseemr]

We zeroed it down to a normalization call from the unifier that is trying to normalize the types with delta constant 0 as well as zeta on. This results in repeated unfoldings of Steel.Preorder.extends' type, which is recursive, and the recursive call is not guarded under a match.

I will try switching off zeta in those norm calls, and see what happens.