I watched a talk by Erik Meijer [1] recently where he mentioned that an implementation of a tuple such as (C# syntax mine, but illustrates the point)

  class Tuple<T1, T2>
  {
    public Tuple(T1 t1, T2 t2) { }
    public T1 Item1 => default(T1); // null for reference-types
    public T2 Item2 => default(T2); // null for reference-types
  }

is a perfectly type-safe implementation of a tuple that's completely nonsense. I'm curious as to how you might actually encode into the type system that the values that come out of Item1 and Item2 are actually the values you put in.

I would love to see tests at the interface level (or typeclass level for Haskellers) rather than the implementation level, to enforce that all implementations of an interface satisfy laws like this. In Haskell, this would mean that you could enforce things like monadic laws which we all assume to be true anyway.

[1] https://www.youtube.com/watch?v=JMP6gI5mLHc