Raise warning on redundant pattern matching

[ckeller]

Raise a warning when a pattern matching is redundant.

[ngrimm]

Unreachable patterns are also not typechecked correctly, as the following example shows:

module Hd

val hd : l:list 'a{is_Cons l} -> Tot 'a
let hd l = match l with
    | [] -> ()
    | hd::tl -> hd 

[catalin-hritcu]

In this case this probably shouldn't even be a warning, but an error.

[catalin-hritcu]

We discussed this with @nikswamy, @fournet, @ngrimm, @aseemr, @jkzinzindohoue this week, and doing this using the SMT solver seems hard, since it would require satisfiability (as opposed to unsatisfiability) queries, and for our theory that means waiting for a timeout.

We were thinking of maybe doing an incomplete syntactic check. Just listened to an ICFP talk on how they do this in Haskell: http://people.cs.kuleuven.be/~tom.schrijvers/Research/papers/icfp2015.pdf

Edit: there was also a talk at the ML workshop on checking GADT pattern exhaustiveness and redundancy for OCaml: http://www.mlworkshop.org/gadts-and-exhaustiveness-looking-for-the-impossible.pdf

[catalin-hritcu]

@kyoDralliam @nikswamy Saving our conversation from Slack. At the end it includes Nik's new suggestion for doing redundancy checking.

kyod [11:39 AM] At some point I had this dream of doing that kind of completion with the smt-solver in order to have only logically relevant branches in the match. Never got much farther than the basic idea though...

catalin [11:52 AM] Discussed with Nik about this in the past

catalin [2 days ago] The context of the previous discussion was giving out warnings for useless match branches (edited)

catalin [2 days ago] The issue with this is that it requires SMT queries which we expect to come back unknown (or sat, but that never happens), which means waiting for a timeout

kyod [2 days ago] can't we ask for satisfaction instead ?

kyod [2 days ago] and retrieve a model ?

catalin [2 days ago] for our kind of queries the SMT solver will never give us SAT, but unknown

catalin [2 days ago] but that's not the main problem, the main problem is that we need to wait for the timeout before getting the unknown, which makes interactivity difficult ... are you willing to wait for 5 seconds per match branch? (edited)

kyod [2 days ago] yes that was why what I had in mind was rather to start with an empty pattern matching and ask the smt for examples of terms which could be present in that 'hole' by successive refinements

catalin [2 days ago] this is even harder then, since mapping (often broken) SMT models back to F* terms in a reliable way seems very challenging

catalin [2 days ago] people doing counterexample finding tools like Nitpick and Nunchaku for Isabelle have devised different kinds of FOL encodings that are "sound for counterexamples" (i.e. for us complete but unsound)

kyod [2 days ago] Is that the kind of thing which would lead for instance to the following interaction ?:

• me : match l : list nat{Cons? l} with
• smt : [0] goes through
• me : match l : list nat with [n] -> ...
• smt : [0 ; 0] goes through
• me : match l : list nat with [n] -> ... | l -> ...
• smt : okay that seems exhaustive (edited)

catalin [2 days ago] Right, this could be the interaction, it's just hard to do. It would be very useful though, for instance for getting counterexamples for wrong specs.

nik [2 hours ago] this would be a very nice feature to have ... but also quite difficult to implement reliably and efficiently

nik [2 hours ago] catalin, isn't your work on dminor etc. also related?

nik [2 hours ago] at least inasmuch as you were using smt partial models, iirc

catalin [2 hours ago] right

catalin [2 hours ago] there is quite a bit of related work

catalin [2 hours ago] I think the state of the art is Isabelle's new Nunchaku tool: https://nunchaku-inria.github.io/nunchaku/ (edited)

nik [2 hours ago] for a start in this direction, a checker for redundant cases would be useful already and may employ similar technology

nik [2 hours ago] a random idea: staying in unsat territory, we could generate a syntatically exhaustive pattern matching form, asserting false in each branch, and retaining for the user only those branches in which false was not provable

nik [2 hours ago] maybe firing this off on a core in the background

nik [1 hour ago] and for interactive speed we could instantly present in the editor the syntactic case analysis, and a few seconds later revise the suggestion by removing some redundant cases

[nikswamy]

While desirable, addressing this feature requires a significant redesign. Closing as a wontfix.