Update for GHC8 and (partial) fix of assertion patterns checking

[yanok]

This pull request contains

1. Update for recent GHC/transformers
2. Fix of the assertion patterns check problem (except for the Dpendent.Monadic variant)
3. Fix of unification to prevent proving of arbitrary function injectivity

[be5invis]

@yanok You separated Unification into "solve" and "check" right?

[yanok]

@be5invis not really. It is still just solve.