Removing matching on PS

This makes it less boring to modify what's in the proof state...
Use correct error function for PElabError

Fixes #1800
New way of dealing with unmatchable patterns

Any term which is not matchable, i.e. a function application or a
repeated variable on the left hand side, is automatically put in a
PHidden. The effect of elaborating PHidden t is to:

1. Delay the elaboration of 't' to the end of elaboration
2. When elaborating t, ensure that its value is already known due to
solving some other unification problem.

If something is PHidden, but not solvable by unification, elaboration
fails.
This finally fixes #323, and probably several other things.
Hide other unmatchable patterns

Lambdas, in particular. Fixes #1671
Fix checkPossible when unifying bound vars

It's not a rigid fail if it's two bound variables that differ.
Fixes #1108
Coverage checker should ignore hidden arguments

Since they're required to be inferred from other arguments, they make no
contribution to coverage checking.
Fixes #1710
Undo dubious optimisation in resolveTC

Since hnf_compute doesn't do what it says, and it's causing some obscure
or complicated type class constraints not to resolve properly.
Fixes #1688
Update CHANGELOG
Only allow @ patterns on LHS

It's meaningless on the RHS and clashes with explicit instances, so
should be disallowed in the parser.
Forgot to commit the update test...