Should pred/fun parameters be type checked in runtime?

[nmacedo]

Alloy allows function/predicate calls like the following, as long as the type of the parameter and the type of the argument are not disjoint (which is the case here, since univ contains A):

sig A,B {}

pred p[a:A] {
  a in univ
}

run { no A and some x: univ | p[x] }

The problem is that the resulting instance is inconsistent: it will have a B$0 for which p holds, even marked $x from skolemization (see screenshot). Even more confusing, if you ask the evaluator whether p[B$0] holds, it will gives a type error, even though it was the $x witness that made the run command consistent. However, if you ask p[x$0] it replies true, even though x$0 = B$0, because its type is univ.

This would be solved if calls to predicates tested the type of the argument during solving (in this case, a in A, which would exclude B atoms from passing it).

[grayswandyr]

This message from @dnjackson might be timely.