Safer type tests in Prolog

This is a very naive attempt at implementing both your suggested solutions.

First, has_type(Type, Var) that succeeds, or fails with an instantiation error:

has_type(Type, X) :-
    var(X), !,
    throw(error(instantiation_error, _)).
has_type(Type, X) :-
    nonvar_has_type(Type, X).

nonvar_has_type(atom, X) :- atom(X).
nonvar_has_type(integer, X) :- integer(X).
nonvar_has_type(compound, X) :- compound(X).
% etc

Second, a could_be(Type, Var) (analogy to must_be/2) that uses coroutining to allow the query to succeed at some point in the future:

could_be(Type, X) :-
    var(X), !,
    freeze_type(Type, X).
could_be(Type, X) :-
    nonvar_has_type(Type, X).

freeze_type(integer, X) :- freeze(X, integer(X)).
freeze_type(atom, X) :- freeze(X, atom(X)).
freeze_type(compound, X) :- freeze(X, compound(X)).
% etc

There are several weak points to this approach but your comments might help me understand the use cases better.

EDIT: On "types" in Prolog

Types in Prolog, as I understand them, are not "types": they are just information that can be queried at run time, and which exists because it is a useful leaky abstraction of the underlying implementation.

The only way I have been able to make practical use of a "type" has been to "tag" my variables, as in the compound terms number(1), number(pi), operator(+), date(2015, 1, 8), and so on. I can then put variables in there, write deterministic or semi-deterministic predicates, understand what my code means when I see it a week later....

So a free variable and an integer are just terms; mostly because, as your question very smartly points out, a free variable can become an integer, or an atom, or a compound term. You could use coroutining to make sure that a free variable can only become a certain "type" of term later, but this is still inferior to using compound terms, from a practical point of view.

It highly likely that I am confounding very different issues here; and to be honest, my experience with Prolog is limited at best. I just read the documentation of the implementation I am using, and try to find out the best way to use it to my advantage.

The testing for types needs to distinguish itself from the traditional "type testing" built-ins that implicitly also test for a sufficient instantiation. So we effectively test only for sufficiently instantiated terms (si). And if they are not sufficiently instantiated, an appropriate error is issued.

For a type nn, there is thus a type testing predicate nn_si/1 with the only error condition

a) If there is a θ and σ such that nn_si(Xθ) is true and nn_si(Xσ) is false
— instantiation_error.

atom_si(A) :-
   functor(A, _, 0),    % for the instantiation error
   atom(A).

integer_si(I) :-
   functor(I, _, 0),
   integer(I).

atomic_si(AC) :-
   functor(AC,_,0).

list_si(L) :-
   \+ \+ length(L, _),  % for silent failure
   sort(L, _).          % for the instantiation error

This is available as library(si) in Scryer.

In SWI, due to its differing behavior in length/2, use rather:

list_si(L) :-
    '$skip_list'(_, L, T),
    functor(T,_,_),
    T == [].