Edit: This question assumes you enabled the occurs check. It's not about setting Prolog flags.
There was a bunch of papers 30 years ago about optimizing away the occurs check automatically, when it's safe (about 90% of predicates, in typical codebases). Different algorithms were proposed. Do modern Prolog compilers (such as SWI Prolog) do anything like that (when the occurs check is turned on)? What algorithms do they favor?
As an example, would they remove the occurs check when compiling a predicate such as this:
less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).
(from the discussion below this answer)
There are a variety of optimizations that can optimize away the occurs check when the occurs check flag is set to "true". This is necessary to make sound unification feasible for common cases. A typical optimization is the detection of linearity of a head:
linear(Head) :-
term_variables(Head, Vars),
term_singletons(Head, Singletons),
Vars == Singletons.
In this case the occurs check can be omitted when invoking a clause. We can make the test for the less/2 example whether the heads are linear or not. It turns out that both heads are linear:
?- linear(less(0, s(_))).
true.
?- linear(less(s(X), s(Y))).
true.
So a Prolog system can totally omit the occurs check for the predicate less/2 and nevertheless produce sound unification. This optimization is for example seen in Jekejeke Prolog when inspecting the intermediate code. The instruction unify_linear is used:
?- vm_list(less/2).
less(0, s(A)).
0 unify_linear _0, 0
1 unify_linear _1, s(A)
less(s(X), s(Y)) :-
less(X, Y).
0 unify_linear _0, s(X)
1 unify_linear _1, s(Y)
2 goal_last less(X, Y)
In contrast to the instruction unify_term, the instruction unify_linear does not perform an occurs check, even when the occurs check flag is set to true.
Ritu Chadha; David A. Plaisted (1994). "Correctness of unification without occur check in prolog". The Journal of Logic Programming. 18 (2): 99–122. doi:10.1016/0743-1066(94)90048-5.