And make it Typeclasses Opaque to ensure that we indeed do not do
so using the proof mode.