<p>Yes, the <a href="http://eclipseclp.org" rel="noreferrer" title="ECLiPSe">ECLiPSe</a> system does this.</p>

<p>As you suggest, it takes into account a number of simple built-in predicates (such as <code>integer/1, =/2, !/0</code>) for indexing purposes.  Your example then executes deterministically, without choicepoints, for all calls of <code>foo/2</code> with the first argument instantiated.  Moreover, ECLiPSe would do this on any argument, not just the first.</p>

<p>You can find a little more detail in the paper <a href="http://arxiv.org/abs/1012.4240" rel="noreferrer" title="ECLiPSe TPLP">ECLiPSe - from LP to CLP</a>.</p>

<p>To answer your followup question: No extra VM features are necessary, the generated VM code looks like this:</p>

<pre><code>foo / 2:
    switch_on_type           a(1) 
            list:           ref(L5)
            structure:      ref(L1)
            bignum:         ref(L7)
            []:             ref(L4)
            integer:        ref(L7)
            meta:           ref(L0)
label(L0):
    try                      0     2     ref(L1) 
    retry                    0     ref(L3) 
    trust                    0     ref(L5) 
label(L1):
    get_structure            a(1)     h / 1     ref(L2) 
    write_value              a(2) 
    ret                  
label(L2):
    read_value               a(2) 
    ret                  
label(L3):
    get_nil                  a(1) 
label(L4):
    get_atom                 a(2)     nil 
    ret                  
label(L5):
    get_list                 a(1)     ref(L6) 
    write_void               2 
label(L6):
    get_atom                 a(2)     cons 
    ret                  
label(L7):
    get_structure            a(2)     n / 1     ref(L8) 
    write_value              a(1) 
    ret                  
label(L8):
    read_value               a(1) 
    ret  
</code></pre>
First argument indexing
<p>I want to know how smart first argument indexing is implemented on various Prolog implementations.</p>

<p>In particular, simple type-test goals like <code>integer/1</code> right after a clause "neck" <em>could</em> contribute to better indexing.
Consider:</p>

<pre><code>foo(h(X),X).
foo([],nil).
foo([_|_],cons).
foo(X,Y) :- integer(X), Y = n(X).
</code></pre>

<p>With this clause ordering I would like the goal <code>foo([],_)</code> to succeed <strong>without</strong> leaving any useless choicepoints.</p>

<p>Unfortunately, SWI Prolog does not figure it out:</p>

<pre><code>?- length(Xs,10),
   maplist(=([]),Xs),
   statistics(trailused,T1),
   maplist(foo,Xs,Ys),
   statistics(trailused,T2).

T1 = 5792,
T2 = 5968,
Xs = [[], [], [], [], [], [], [], [], [], []],
Ys = [nil, nil, nil, nil, nil, nil, nil, nil, nil, nil] ...
</code></pre>

<p>Do other Prolog implementations do better?</p>