Implementation of "guarded methods" using type equality witnesses