I can't tell if you are serious or not. OP goes through them by example.
Original type:
type 'a t = | Array of 'a array
| Bytes of bytes
GADT'd (same functionality as before):
type 'a t = | Array : 'a array -> 'a t
| Bytes : bytes -> 'a t
Now using power of GADT to add constraint:
type 'a t = | Array : 'a array -> 'a t
| Bytes : bytes -> char t
Just jumping into it seems like a fine choice to make. Allows for a (narrow) introduction to GADTs without getting bogged down in their full complexity/limitations. Shows that it's useful before/without a theoretical discussion.
Still, I wouldn't have minded a little discussion introducing GADTs.
