Fix for metavariables in type declarations

Allow multiple, with later allowed to depend on earlier
Record partial type inference info

Proof search now has access to this and can fill in some basic type
information. Lots still to do though (especially dealing with type
classes, properly spotting errors, and polymorphic type variables).
Some improvements in finding inference constraints
More consistency checking on inference constraints

Also added a test for simple interactive type inference