A riddle regarding type safety

Of course, I have explained to the students in my language theory class what type safety means (remember: progress + preservation) and we have studied this notion time and again for some of the TAPL languages. However, I don't feel like the notion really sinked in universally. Some students consider all this semantics and calculus stuff as obscure and there is a certain critical mass of notation, when passed, concepts are not understood anymore (by some if not many of the Bachelor-level students in my class).

Last night, I came up with a nice "semantics riddle" for type safety:

What would be a super-trivial language with a type system and an SOS semantics such that type safety is violated?

I gave the students 2 minutes to think about the question.

I emphasized several times that the language should be super-trivial.

I also asked them for a general strategy for mis-designing a language to be type-unsafe.

One idea that popped up was to support some notion of cast.

We agreed that this would not be trivial, certainly not super-trivial.

Here is my reference solution:

Syntax of expressions

e ::= v | z

(Hence, there are expressions (forms) x, y and z.)

Values (normal forms)

v := x | y

Types

t ::= a | b

(a and b are the possible types.)

Small-step relation

z -> x

(Yes, we only have one axiom.)

Typing rules

x : a

y : b

z : b

(Yes, we have only axioms here.)

Demonstration of lack of type safety

The term z is the culprit.

z : b but z -> x and x : a

Regards,

Ralf