Tuples.idr

-- Note, this does not compile as-is, Idris tells me: 
-- "Attempting concrete match on polymorphic argument: MkPair second_elem _rest" 
-- and I don't know why. (Is it because I haven't specified that second_elem should implement Show in this case?)
showBoth' : Show a => Show b => Pair a b -> String
showBoth' (first_elem, (second_elem, _rest)) = "The first element is: `" ++ (show first_elem) ++ "` and the second element is: `" ++ (show second_elem) ++ "`"
showBoth' (first_elem, second_elem) = "The first element is: `" ++ (show first_elem) ++ "` and the second element is: `" ++ (show second_elem) ++ "`"

The problem here is that your concept of “first two elements of a tuple” is not a concept that makes sense with Idris tuples. If you want a tail to be distinct from an element, use a data structure which makes the distinction, like an HVect.