To quote the SICStus Prolog manual:
The usual mathematical theory behind Logic Programming forbids the creation of cyclic terms, dictating that an occurs-check should be done each time a variable is unified with a term. Unfortunately, an occurs-check would be so expensive as to render Prolog impractical as a programming language.
However, I ran these benchmarks (The Prolog ones) and saw fairly minor differences (less than 20%) in SWI Prolog between the occurs check (OC) being on and off:
OC is off: :- set_prolog_flag(occurs_check, false). in .swiplrc (restarted)
?- run_interleaved(10).
% 768,486,984 inferences, 91.483 CPU in 91.483 seconds (100% CPU, 8400298 Lips)
true.
?- run(1).
'Program' Time GC
================================
boyer 0.453 0.059
browse 0.395 0.000
chat_parser 0.693 0.000
crypt 0.481 0.000
fast_mu 0.628 0.000
flatten 0.584 0.000
meta_qsort 0.457 0.000
mu 0.523 0.000
nreverse 0.406 0.000
poly_10 0.512 0.000
prover 0.625 0.000
qsort 0.574 0.000
queens_8 0.473 0.000
query 0.494 0.000
reducer 0.595 0.000
sendmore 0.619 0.000
simple_analyzer 0.620 0.000
tak 0.486 0.000
zebra 0.529 0.000
average 0.534 0.003
true.
OC is on: :- set_prolog_flag(occurs_check, true). in .swiplrc (restarted)
?- run_interleaved(10).
% 853,189,814 inferences, 105.545 CPU in 105.580 seconds (100% CPU, 8083669 Lips)
true.
?- run(1).
'Program' Time GC
================================
boyer 0.572 0.060
browse 0.618 0.000
chat_parser 0.753 0.000
crypt 0.480 0.000
fast_mu 0.684 0.000
flatten 0.767 0.000
meta_qsort 0.659 0.000
mu 0.607 0.000
nreverse 0.547 0.000
poly_10 0.541 0.000
prover 0.705 0.000
qsort 0.660 0.000
queens_8 0.491 0.000
query 0.492 0.000
reducer 0.867 0.000
sendmore 0.629 0.000
simple_analyzer 0.757 0.000
tak 0.550 0.000
zebra 0.663 0.000
average 0.634 0.003
true.
Are these benchmarks not representative of real-world usage? (I remember reading somewhere that they were specifically chosen to be "fairly representative") Is SWI Prolog implementing some optimization tricks, that SICStus people aren't aware of, that make the cost of OC minor? If so, are they published? (I found a bunch of papers about this from the '90s, but I don't know if they are state-of-the-art)
The major optimization makes unification of local variables a constant operation.
Many abstract machines like the PLM, ZIP, WAM, VAM provide a special case for logic variables that cannot be subterm of some structure (called local variables). Unification with such variables does not require any occurs-check at all and thus can be constant. In this manner large terms can be "passed back" without an extra occurs-check required.
Without this optimization, the handling of grammars (for parsing a given list) gets an overhead quadratic in the number of tokens. Every time the "input list" is handed back (so, graphically speaking, every time you are crossing a comma after a non-terminal in the grammar body), the remaining input list needs to be scanned for the occurrence of that local variable. (It's better than quadratic in the number of characters, since regular expressions are mostly encoded tail-recursively).
This optimization was introduced 2007 in 5.6.39. It is surprising that your measurements show overheads even in cases like tak, where not a single structure is built at all. As far as I can remember, occurs-check unification in SWI 5.6.39 ran a tiny bit faster than rational tree unification (for simple cases) as (at that time) no extra setup was needed.
There is still ample room for many further occurs-check optimizations. But those will only happen, if people do use this feature. As for SWI, not much happened in the last 13 years.
But think-of-it: The very first Prolog, called Prolog 0 did support the occurs-check by default. But from Prolog I ("Marseille Prolog") on, only excuses (such as those you cite) were made. And at least, the standard did not rule out occurs-check unification as default by only defining NSTO executions and requiring unify_with_occurs_check/2 and acyclic_term/1. And now, Prologs like SWI, Tau, and Scryer provide it optionally via a flag.
A further optimization into the same direction is Joachim Beer's NEW_UNBOUND tag which avoids additionally occurs-checks of some heap-variables at the expense of a more complex scheme. See The Occur-Check Problem Revisited. JLP 5(3) 1988. And LNCS 404.