Why are underscores only allowed in type patterns?

As near as I can tell, this is allowed:

```
a: type.
t2: PI [!_,!_] : (!a * !a) . a = \[!x,!y]. x.
```

but this is not, and gives a parse error:

```
t3: PI [!_,!_] : (!a * !a) . a = \[!x,!_]. x.
```

This is a bit inconsistent and makes it more difficult than it needs to be to explain patterns.
