idris-lang/Idris-dev — pull request #1287 by david-christiansen (2014-06-05 12:04:55+00:00)
Title: Distinguish postulate providers and type providers at use site

This is not backwards compatible, but as far as I know, there are no
users of postulate providers who are not me.

The old system allowed both the definition of the provider and the use
site to be involved in the determination of what is a postulate and what
is not. This is not good - users should always be in full control of
this.

The new implementation has two syntaxes:

%provide (x : t) with p

and

%provide postulate x with p

The first is the type provider syntax we know and love. The second
requires that the provider in fact return a type, which is then made
into the type of the resulting postulate.