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 counter example for total active patterns that are not exhaustively matched #823

Open
smoothdeveloper opened this issue Jan 3, 2020 · 4 comments

Comments

@smoothdeveloper
Copy link
Contributor

@smoothdeveloper smoothdeveloper commented Jan 3, 2020

Given

let (|PA|PB|) x = match x with Some _ -> PA | _ -> PB
let f = function | PA -> ()

it currently produces

  let f = function | PA -> ();;
  --------^^^^^^^^
warning FS0025: Incomplete pattern matches on this expression.

I'd like the compiler to provide counter example of PB the same way it does with normal pattern matching on discriminated unions or concrete values.

Pros and Cons

Pros:

Cons:

  • PatternMatchCompilation.fs gets a bit bigger
  • some more work to produce the current warning, unsure if it is just missing to show the counter examples or if constituting the list is significant extra work, I assume not since it currently compiles to a ChoiceXofY and it is able to produce the warning

Extra information

Estimated cost: M

Affidavit

Please tick this by placing a cross in the box:

  • This is not a question (e.g. like one you might ask on stackoverflow) and I have searched stackoverflow for discussions of this issue
  • I have searched both open and closed suggestions on this site and believe this is not a duplicate
  • This is not something which has obviously "already been decided" in previous versions of F#. If you're questioning a fundamental design decision that has obviously already been taken (e.g. "Make F# untyped") then please don't submit it.

Please tick all that apply:

  • This is not a breaking change to the F# language design
  • I or my company would be willing to help implement and/or test this
@abelbraaksma

This comment has been minimized.

Copy link

@abelbraaksma abelbraaksma commented Jan 3, 2020

Would be a great addition to the heuristics, but it may be tricky if the active pattern matches are mixed with other active patterns, normal patterns in the same match statement.

Perhaps if we'd only implement the trivial case (one active pattern used in the match clauses, provided it's 'total') it'd be not too hard to do.

@charlesroddie

This comment has been minimized.

Copy link

@charlesroddie charlesroddie commented Jan 3, 2020

I'd like the compiler to provide counter example of PB

Following on from @abelbraaksma, I would have thought that None, not PB, is the right counterexample and your suggestion of PB could be due to a strangeness in the current inference.

let (|PA|PB|) = function Some() -> PA | None -> PB
let f(x:unit option) =
    match x with
    | PA -> ()
    // | None -> () : if this is added, then "Incomplete pattern matches on this expression."
    // PB -> () : if this is added, the compiler is happy.

The compiler does seem to have special logic checking completeness for complete active pattern cases. This seems brittle for settings where active and other patterns are included in a match.

An implementation of this suggestion might need to expand the match, substituting the patterns (expanding PA to Some() and PB to None in this case), and do a completeness check on that.

It should work as long as there is no non-terminating recursion:

/// should stall on runtime not compile time
let rec (|PA|PB|) = function QA -> PA | QB -> PB
and (|QA|QB|) = function PA -> QA | PB -> QB
@smoothdeveloper

This comment has been minimized.

Copy link
Contributor Author

@smoothdeveloper smoothdeveloper commented Jan 3, 2020

Thanks for the comments, active patterns can be mixed and total active patterns aren't an exception; I totally overlooked that while making the suggestion,

Would it make sense to update the suggestion so that it applies for match expression when existing clauses are solely members of the active pattern definition, aka unmixed?

let (|PA|PB|) x = match x with Some _ -> PA | _ -> PB
let f =
    function
    | PA -> ()
    | None -> ()

would remain unchanged (warning without counter example, despite being a false positive)

If the exhaustiveness check could be handled as @charlesroddie explains it would be even better, but the restricted case intended for this suggestion maybe has better chance to be implemented.

@abelbraaksma

This comment has been minimized.

Copy link

@abelbraaksma abelbraaksma commented Jan 4, 2020

but the restricted case intended for this suggestion maybe has better chance to be implemented.

@smoothdeveloper I agree. I think catching the general case is a good thing to have. Typically, one would use complete (or closed) active patterns to use them as a whole, so that the compiler only needs to call the active pattern function once. It seems to me that the available cases (internally, these are ChoiceXofY I believe) are transparent to the compiler and can be reasoned about during exhaustiveness checks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.