Let’s say I have a trivial GADT
type _ t = | Str : string t | Int : int t
If I have a function
f that’s defined as
let f : bool t -> bool = ...
f can be implemented using
function | _ -> failwith "unimplemented"
But if I add a new constructor
Bool : bool t to
t, ideally I should know that now I’m not being exhaustive, which that doesn’t guarantee.
Is it possible for me to ensure that
bool t doesn’t have any constructors, similar to how I can know that I’m not exhaustively enumerating all constructors in the non-empty case?