Improve termination checking for instances

[lukaszcz]

For example, this currently doesn't pass termination:

-- FIXME fails instance termination
instance
StateT-MonadReader {R S : Type} {M : Type → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) :=
   mkMonadReader@{
     monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}};
     reader {A : Type} : (R → A) → StateT S M A := liftStateT << MonadReader.reader;
     ask : StateT S M R := liftStateT MonadReader.ask;
     monad := StateT-Monad@{mon := MMonadReader.monad {{mreader}}};
     reader {A : Type} : (R → A) → StateT S M A := liftStateT << MMonadReader.reader;
     ask : StateT S M R := liftStateT MMonadReader.ask;
  };

The problem is that R does not decrease. We should do proper termination checking, trying to find a lexicographic order.