Yes, exactly. Here's the type signature for `cast`:
cast : Cast from to => from -> to
So if the types `from` and `to` are part of the `Cast` typeclass, then cast will always convert one into the other, without "failing". The standard library defines a handful of "sensible" casts like Int to Float, but you can't even attempt to cast a function to a String, or a List to an Int, since those aren't part of the `Cast` typeclass.
For an operation that can fail, like a parse method, a more appropriate return type is `Maybe Int`, or `Either String Int` (where the `String` is an error message).
Also Idris provides a dependently-typed way to connect the check (`all isDigit (unpack input)`) to the conversion itself (`cast input`), so that you can't write an invalid check or forget to include the check at all. See my reply to vosper above.
For an operation that can fail, like a parse method, a more appropriate return type is `Maybe Int`, or `Either String Int` (where the `String` is an error message).
Also Idris provides a dependently-typed way to connect the check (`all isDigit (unpack input)`) to the conversion itself (`cast input`), so that you can't write an invalid check or forget to include the check at all. See my reply to vosper above.