[Agda] Transitive-on

[Ramana Kumar]

I am getting yellow highlighting in the following, which I think
indicates a problem.
But I don't know what the problem might be or have any idea how to
find out by asking Agda directly...
What does yellow actually mean, and how can it be resolved?
And what's wrong with the following attempt? Is there a simpler way to proceed?
My short term goal is to define a strict total order on Strings (which
seems to be missing from the standard library...)

------8<------
open import Data.Nat using (ℕ) renaming (_<_ to _N<_)
open import Data.Nat.Properties renaming (<-trans to N<-trans)
open import Relation.Binary using (Rel;Transitive)
import Level

Transitive-on : ∀ {a b l} {A : Set a} {B : Set b} {_<_ : Rel A l} {f :
B → A} → Transitive _<_ → Transitive (_<_ on f)
Transitive-on t = t

Char<-isTransitive : Transitive (_N<_ on Data.Char.toNat)
-- Char<-isTransitive = Transitive-on N<-trans
Char<-isTransitive = Transitive-on {a = Level.zero} {b = Level.zero}
{l = Level.zero} {A = ℕ} {B = Data.Char.Char} {f = Data.Char.toNat}
N<-trans
------8<------

The right hand side of the last line (or the commented out
alternative) turns yellow. Everything else loads OK.