Stefan pushed to branch main at Stefan / Typer

Commits: bf851a68 by Stefan Monnier at 2022-10-07T19:23:48-04:00 * src/lexp.ml (push_susp): Don't call `mkSLlub'` with suspensions

(mkSLlub'): Improve error message ever so slightly

- - - - -

1 changed file:

- src/lexp.ml

Changes:

===================================== src/lexp.ml ===================================== @@ -356,8 +356,8 @@ let mkSLlub' (e1, e2) = match (lexp_lexp' e1, lexp_lexp' e2) with (* FIXME: This first case should be handled by calling `mkSLlub` instead! *) | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l - | (SortLevel SLz, _) | (_, SortLevel SLz) - -> Log.log_fatal ~section:"internal" "lub of SLz" + | (SortLevel SLz, e) | (e, SortLevel SLz) + -> Log.log_fatal ~section:"internal" "lub of SLz with %S" (lexp_head (hc e)) | (SortLevel (SLsucc _), SortLevel (SLsucc _)) -> Log.log_fatal ~section:"internal" "lub of two SLsucc" | ((SortLevel _ | Var _ | Metavar _ | Susp _), @@ -554,7 +554,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) | SortLevel (SLz) -> e | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s)) | SortLevel (SLlub (e1, e2)) - -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) + -> mkSortLevel (mkSLlub' (push_susp e1 s, push_susp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (_, _) -> e | Builtin _ -> e

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/bf851a685972478e08e8011862cfa7135a...