Uncommented the stuff in Decidable to see what happens.
Explicit instance to liftRel apparently makes Decidable work.
Merge branch 'master' of github.com:edwinb/Idris-dev
Fix bug in 'forget' for well-typed terms

Meant that sometimes if names were shadowed, the wrong ones were picked
up when rechecking, so a term which should have been well-typed was not.

Fixes #714
A simpler approach to handling name shadowing

It's hard to get right, so there's no need to be clever (indeed there's
a need not to be clever). So just before elaboration (while adding
implicits and resolving global names) we traverse a term and rename any
binder which has already been used, inventing a unique name which is not
used anywhere else in the term.
Merge branch 'master' of github.com:idris-lang/Idris-dev
Check lambda bound name is valid

Can't bind a name that is the same as a global type constructor name.
This can lead to mysterious errors if unchecked, particularly with
dependent pair types.

Fixes #704
Merge pull request #783 from tpsinnem/master

Make Decidable.Decidable and Decidable.Order available with a little fix
Remove comments in Decidable.Decidable
Make $ built in operation, rename ($) to apply

Slightly controversial, but I think it is better this way.

Main advantage:
Plays much better with disambiguation (which doesn't work especially
well with HOFs since it looks at the goal type and the types of each
argument to disambiguate, and if a function is the argument to $ we've
lost some of that information). This will make elaboration quicker in
some cases. $ is quite handy notation and we don't want to discourage it
just because it slows down the elaborator.

Main disadvantage:
Very occasional use in HOFs itself. Hence the new function 'apply' which
does the same thing.
Remove apply from reg001 since it's in the prelude!
Implicit "module Main" added

When there is no module header, it is assumed that the module is the
Main module. This is mostly to ensure all names are qualified.
%unqualified is for the (rare, and probably builtins only) case where no
name qualification is desired.
Allow mutually defined instances

Fixes #657
Fix error reporting with mutual instances
Merge branch 'master' of github.com:idris-lang/Idris-dev into prelude-ext