Postulate providers

Allow type providers to postulate their type, in addition to proving it.

Applications: easy interfacing to SMT solvers, compile-time quickcheck