Original bug ID: 7319
Reporter: @alainfrisch
Status: acknowledged (set by @damiendoligez on 2016-09-27T14:23:18Z)
Resolution: open
Priority: normal
Severity: feature
Target version: later
Category: typing
Has duplicate: #7091
Related to: #5736
Monitored by: @yallop @Chris00

Bug description

Consider:

type _ ty =
  | Int: int ty
  | String: string ty
  | Bool: bool ty

let to_int: type t. t ty -> t -> int = fun ty x ->
  match ty with
  | Int -> x
  | String -> failwith "..."
  | Bool -> failwith "..."

One cannot share the last two cases with a simple or-pattern, because the type of ty is refined to two incompatible types (even if this type is not used).

Of course, one can share by introducing a function and call it in each case, but this is still quite a bit heavier than just String | Bool -> failwith "...". The risk is that users simply write | _ -> ... in such cases, which is more fragile.

I'm wondering if something could be done to address that, either requiring some explicit syntax (to tell the type-checker not to refine the type) or not (delaying refinement until the case needs it?). If we add some syntax to name existentials, could we reuse it with "_" as the name to ignore one specific existential?