
<html><head>

<meta http-equiv="Content-Type" content="text/html; charset=utf-8">

  </head>

  <body>

    <br>

    > Under the David rules, this switch is not exhaustive,<br>

    <blockquote type="cite" cite="mid:CAA9v-_OakXNMHfYnUUVKWH4TBYKXAW9b_RpCMgSgGkHoRpGo=w@mail.gmail.com">

      <div dir="ltr">

        <div class="gmail_default" style="font-family:monospace">>

          because it matches neither Pair(null, _) or<br>

          > Pair(_, null). So what cases would you have to add to the<br>

          > switch to satisfy the compiler's complaints of<br>

          > non-exhaustiveness?  Write the code, and then tell me if<br>

          > you want to program in that language...<br>

          <br>

          Excellent example lol. That clarifies it perfectly. So, the

          reason why we do not want to have this level of specificity

          required by the programmer is because it would cascade into a

          giant pile of writing down edge cases. Makes perfect sense.<br>

        </div>

      </div>

    </blockquote>

    <br>

    Yes.  And it is not that I am against asking users to write down the

    edge cases when it makes sense, but here it makes no sense.  Being

    explicit about the potential combinatorial explosion of edge cases

    will not make anyone's code better, and will more likely encourage

    developers to achieve totality by sticking a default clause on --

    which means worse exhaustiveness checking which in turn means less

    reliable programs.  <br>

    <br>

    <br>

  </body>

</html>