The more complicated a type system is, the harder it is to make inference work. Global type inference typically works well in Haskell without any hand-holding,

The more complicated a type system is, the harder it is to make inference work. Global type inference typically works well in Haskell without any hand-holding, but when you pack more features into the type system (e.g. in Idris), the programmer needs to explicitly write out more type signatures. This type system looks "next-level complicated", so inference is probably way out of the question, e.g. if you saw the expression 2 + 3, maybe the types are: 2 :: Head<Filter<IsPositive,[-1,-3,2,4]>> 3 :: Head<Drop<4,Fibonnaci>> If you were type-checking, you could start on the RHS, end up with the LHS, and then confirm that these two sub-expressions can be added. But with inference you're trying to figure out the most appropriate RHS from the LHS.