Typed Racket exposes unsafe primitives that make it possible to unsafely cast a value to an arbitrary type. Is it also possible to use existing unsafe utilities to somehow make Typed Racket assume that one type is another's subtype?
I imagine a few uses for such unsafe operation:
- To implement GADT, where, within some scope, for example, we make Typed Racket assume that
(Expr Integer)are the same type
- To encode higher-kinded polymorphism through type-level de-functionalization, where we make Typed Racket assume that a direct type application (e.g.
(List a)) is the same as a spelled-out type application
(Type-App List:Tag a)