Now, the type checker won't attempt to generalise over the skolem
variables in the interactive bindings.  If we end up trying to show
one of these types, there will be an unresolved predicate 'Show t'
which causes a type error (albeit a strange one, I'll fix that
later).