I don't have much experience with Scala. Looking at it the type system seems very complicated, somehow Idris appears to do more with less?

I have got a vague memory of reading a paper by Simon Peyton Jones (or was it a video?) He was discussing why is Haskell not object oriented and he seemed to be saying that things get complicated when we mix two types of polymorphism: parametric polymorphism (type variables in functional languages) and polymorphism based on subtyping (object oriented languages). Somehow when we try to combine these types of polymorphism the complexity inevitably results.

Its an interesting conjecture anyway. Could we prove it in category theory?

Martin