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) ++ "`"

In the pattern (first_elem, (second_elem, _rest)) you match a Pair a b against a pattern for a Pair a (Pair c d). But there is no guarantee that b is a Pair c d as it is a polymorphic argument. Just get rid of that line altogether.

@gallais: What I want showBoth' to do is to show the first two arguments if a tuple like (1,2,3,4) is passed in.
So both showBoth' (1,2) and showBoth' (1,2,3,4) should return "The first element is: 1 and the second element is: 2" : String`.

How can I add a separate clause for this function that is called when b is a Pair c d?

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.