You should be able to write your own named implementation of Cast and explicitly use it when calling cast to have different casts with different semantics http:

You should be able to write your own named implementation of Cast and explicitly use it when calling cast to have different casts with different semantics http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#named-implementations http://docs.idris-lang.org/en/latest/tutorial/interfaces.htm.... But yeah, you'd still have to see what the standard library implementation does