Tools for reduced semantics and structural inference?

I see there is already an “A general comment…” post today, so please forgive another not-so-specific post.

So, I’m tempted to use Prolog again for a project – I’ve gone down this road before, and I’ve always had to back down, so I’m seeing if there is anything I’m missing that could help.

I think to summarize: Prolog gleefully makes all the hard stuff easy, but sadly, always seems to make all the stuff that should be easy a PITA.

There are two cases where I think tooling could help, but I haven’t seen it AFAIK.

(1) Basic algorithm description
Now there are cases where you want to do backtracking, but in many cases you don’t want to --so unwanted backtracking gets you. It is helpful of course, not to use failure-driven loops, etc., but to use higher-order predicates to control your program. With SWI Prolog “lambdas” this becomes a little easier, but still is a bit awkward. Also line-at-a-time stinging of predicates with temp logvars used for I/O params can also be a bit long-winded.

I think a few things could help here – (a) an embedded procedural, expression-orientated language that is transformed at read-time (like “is” on steroids), and/or (b) or a replacement for :- ( “:1-” ?) that has reduced, Mercury-like semantics so that preds that backtrack need to be marked explicitly, otherwise every unmarked goal is treated as if it had “once” wrapped around it. (Though there may be to be a “blacklist” of preds that still backtrack, special handling of meta-preds, etc.)
Prolog makes it pretty easy to provide these, but wondering if there is a standard in the community.

(2) Unification failure due to bugs (esp. during program evolution)
So it seems to me that it should be fairly easy to implement structural type inference and checking, either using call-site patterns, definition patterns, and/or user-provided pattern meta-data. For example, if have a “foo(X/Y) :- …” or “foo(Z) :- Z = X/Y, …”, etc., defined and I start typing “foo(” as a goal, I should get “intellisense” that gives me a possible structural pattern for the call. If I have a program with “foo(42)” as a goal (with no other foo defined that can possibly unify), I should know before I even run the program that this will fail. (Assuming foo/1 is not dynamic.)

This also brings up refactoring which seems especially painful. If I decide to use use X/Y for points in my program, and then want to switch to point(x,y), for example, then this can be hard. This is true especially because if you happen to match on Point (w/o matching sub-parts) rather than X/Y, so you can just pass the point to something else, on one hand it’s good because the intermediate preds don’t need to be modified for the change to point(x,y) – but by the same token, when things break at runtime you are now many layers down and don’t know where things went wrong. So it would be nice if pattern-based constraints percolated up the call-chain and were visible in tooling.

So, am I missing any tools/libs/plugins/etc., here to help me out??
Thanks