One of the most surprising things in Alloy for me was that predicates are not constrained by their parameter type

```
pred foo[ n :one Int ] {}
run withset { foo[ Int ] }
run withnone { foo[ none ] }
```

Clearly the first run makes `n`

a `set`

and the second uses `none`

. Both times the constraint defined for the `n`

parameter does not satisfy the given constraint `one Int`

.

It would make my life a lot easier (and I expect newcomers as well) if the predicate began with checking its parameters. That s `pred foo[ n : Int ] { one n .... }`

I vaguely recall that Daniel ones explained me why this was a case of a rock and a hard place. However, I think it is a good time to have this discussion. And if Daniel can explain it, at least we’ve got it on record

It is indeed a really annoying feature of Alloy that declaration constraints are only enforced when you run a function or predicate directly. My recollection is that the reason we didn’t enforce them everywhere is that we couldn’t come up with a simple semantics. The obvious strategy would be to add explicit constraints in calls, so that if you call a predicate

```
pred foo[ n :one Int ] {}
```

like this

```
foo[e]
```

the call would be taken as short for

```
foo[e] and one e
```

The problem, as far as I recall, is that it’s not clear what to do with functions. Suppose I declare

```
fun bar [x: one X]: Y {...}
```

and now I have something like

```
all a, b: X | bar[a+b] in bar[a] + bar[b]
```

what constraints do I add and where?

It just seemed more trouble than it was worth. Now that I think about it again, though, I wonder if the inconsistency we already have is any better than just doing this for predicates but not functions, which should be pretty easy.

1 Like

Could we also constrain it to be in the proper set? I.e. `one (e & Int)`

. I guess the parser will not allow any mismatched types but it will make my life a bit easier I also think we already have a precedent for this since a `run foo`

already infers the proper type.

I wouldn’t translate the decl constraint that way. Suppose the predicate is

```
sig S {}
sig S2 extends S {}
pred foo [x: one S2] {...}
```

Then

```
one (x & S2)
```

allows `x`

to violate the constraint `x in S2`

. What’s wrong with this?

`one x and x in S2`

Not following … assuming s was meant to be x?

```
sig S {}
sig S2 extends S {}
check {
all x : univ | (x in S2 and one x) iff (one (x & S2))
}
```

Has no counter example?

Yes, sorry – meant x. I edited the original post.

Try this:

```
sig S {}
sig S2 extends S {}
check {
all x : set univ | (x in S2 and one x) iff (one (x & S2))
}
```