Added foldr1 method to Vect.idr
Modified uniqueBinders function to prevent overlapping binders.
Preliminary version of type-directed search
Merge pull request #1258 from bmsherman/uniqueBinders

Fix possible bug in alpha conversion
Merge remote-tracking branch 'upstream/master' into typeSearch
Postpone implicit addition in case blocks

They get resolved later, when the lifted function is type checked. This
ensures that case blocks have the same pattern scoping rules as top
level functions (and saves a small amount of work!)

Fixes #1244
Rename 'effect' to 'call'

Sorry for breaking code again! But... "effect" is too overloaded, and
this really does just mean calling a single effectful operation.
"Effect" and "EFFECT" still refer to effect signatures and concrete
effects respectively.

This only affects effect definitions, not user code which uses an
effectful library.
Remove force/lazy

Since they are old style laziness and no longer work :). Also 'repeat'
on Lists since it used 'lazy'.
Merge pull request #1261 from jeffersoncarpenter/vect-foldr

Added foldr1 method to Vect.idr
Extend positivity check for mutual data types

Needs a make lib_clean
Find negative occurrences in positivity checker

We were only looking in higher order arguments, not in polymorphic
arguments, so missed a few.

Fixes #474
Merge branch 'master' of github.com:idris-lang/Idris-dev
Make load to line work with mutual blocks

Now reads entire block before stopping loading (otherwise we might not
get all the declarations we need for the block to type check)
Now we can handle typeclasses!

Note: The method by which we match typeclasses is ugly and brittle,
and ought to be changed eventually.
Unify more things!

If two solutions arrive at more or less the same time (e.g. part of the
same application) but are not identical, we need to unify them before
propagating solutions.
Merge pull request #1263 from bmsherman/typeSearch

Add type-directed search functionality (like Hoogle)
Add staticEff/toEff

Sometimes when working with effectful programs which change state, you
need to give the intermediate effect state explicitly, which can be
inconvenient with (>>=) especially, so these functions make it easier.

toEff is especially useful with 'case' blocks which branch the effects then
rejoin after.
New matching rule for solving simple functions

This applies only at the end of unification: if a constant function
returning a constructor form would solve a metavariable, fill it in.