# Predicate parameters are not constrained
**URL:** https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226
**Category:** Alloy 6
**Created:** [February 19, 2022, 11:41am UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226 "2022-02-19T11:41:10Z")
**Posts on this page:** 8
**Page:** 1
### Author:  [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)
#### Post date: [February 19, 2022, 11:41am UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226/1 "2022-02-19T11:41:11Z")
One of the most surprising things in Alloy for me was that predicates are not constrained by their parameter type
```nohighlight
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 🙂
---
### Author:  [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)
#### Post date: [February 21, 2022, 3:42pm UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226/2 "2022-02-21T15:42:01Z")
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.
---
### Author:  [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)
#### Post date: [February 21, 2022, 4:38pm UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226/3 "2022-02-21T16:38:52Z")
> [@DanielJackson](#):
>
> the call would be taken as short for
>
> ```alloy
> foo[e] and one e
>
> ```
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.
---
### Author:  [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)
#### Post date: [February 21, 2022, 4:39pm UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226/4 "2022-02-21T16:39:48Z")
BTW, there is already a discussion on github [No type checking on directly run predicates · Issue #14 · AlloyTools/org.alloytools.alloy · GitHub](https://github.com/AlloyTools/org.alloytools.alloy/issues/14)
---
### Author:  [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)
#### Post date: [February 21, 2022, 5:04pm UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226/5 "2022-02-21T17:04:55Z")
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
```
---
### Author:  [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)
#### Post date: [February 21, 2022, 5:42pm UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226/6 "2022-02-21T17:42:42Z")
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?
---
### Author:  [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)
#### Post date: [February 21, 2022, 7:15pm UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226/7 "2022-02-21T19:15:17Z")
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))
}
```
---
### Author:  [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)
#### Post date: [February 21, 2022, 7:58pm UTC](https://alloytools.discourse.group/t/predicate-parameters-are-not-constrained/226/8 "2022-02-21T19:58:35Z")
Ah! Thanks 🙂
Good lesson!