Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Provide a way to ignore existentials in GADT pattern matching #7319

Closed
vicuna opened this issue Aug 4, 2016 · 1 comment
Closed

Provide a way to ignore existentials in GADT pattern matching #7319

vicuna opened this issue Aug 4, 2016 · 1 comment

Comments

@vicuna
Copy link

vicuna commented Aug 4, 2016

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?

@vicuna vicuna added the typing label Mar 14, 2019
@trefis
Copy link
Contributor

trefis commented Mar 15, 2019

This particular situation is now handled since 4.08, as a result of #2110.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants