Giter Club home page Giter Club logo

Comments (1)

jiribenes avatar jiribenes commented on August 21, 2024

I have a very simple fix for this that reports something like the following by constructing a string

Non exhaustive pattern matching, missing case Fork(Fork(_, false, _), _, _)
Non exhaustive pattern matching, missing case Fork(Fork(_, _, Fork(_, _, _)), _, _))
Non exhaustive pattern matching, missing case Fork(Leaf(), _, _)

for the following code:

type BooleyTree {
  Leaf()
  Fork(l: BooleyTree, v: Bool, r: BooleyTree)
}

def testTree(t: BooleyTree): Int = t match {
  case Leaf() => 42
  case Fork(Fork(l, true, Leaf()), _, r) => <>
}

However, I'm not 100% convinced that creating a string is the best solution here. If we instead construct the actual term, then we could later on use LSP to automatically suggest a fix (just insert a pp"case $MyPrettyTerm => <>").

In case I forget, here's the (very rough!) patch:

Warning: This patch is quite limited, has a lot of code duplication and doesn't actually consider two out of the four cases at all.

diff --git i/effekt/shared/src/main/scala/effekt/typer/ExhaustivityChecker.scala w/effekt/shared/src/main/scala/effekt/typer/ExhaustivityChecker.scala
index a9e18e68..33185921 100644
--- i/effekt/shared/src/main/scala/effekt/typer/ExhaustivityChecker.scala
+++ w/effekt/shared/src/main/scala/effekt/typer/ExhaustivityChecker.scala
@@ -150,13 +150,35 @@ object ExhaustivityChecker {
     // ---------------
     def reportNonExhaustive()(using C: ErrorReporter): Unit = missingCases.foreach {
       case Missing.Tag(ctor, at) =>
-        C.error(pp"Non exhaustive pattern matching, missing case for ${ ctor }")
+        // TODO: wouldn't it be better to construct terms and then pretty print those?
+        def pretty(ctor: Constructor, at: Trace, soFar: String): String = at match {
+          case Trace.Root(_) => soFar
+          case Trace.Child(childCtor, field, outer) => childCtor.fields match
+            case Nil => C.panic("reportNonExhaustive: impossible, child trace has no fields")
+            case _ =>
+              val acc = s"${childCtor.name}(${childCtor.fields.map { f => if f == field then soFar else "_" }.mkString(", ")})"
+              pretty(childCtor, outer, acc)
+        }
+        val root = ctor.fields match
+          case Nil => s"${ctor.name}()"
+          case _ => s"${ctor.name}(${ctor.fields.map { _f => "_" }.mkString(", ")})"
+        C.error(pp"Non exhaustive pattern matching, missing case ${pretty(ctor, at, root)}")
       case Missing.Guard(term) =>
         C.at(term) {
           C.error(pp"Non exhaustive pattern matching, guard could be false which is not covered")
         }
       case Missing.Literal(value, tpe, at) =>
-        C.error(pp"Non exhaustive pattern matching, missing case for ${value}")
+        // TODO: wouldn't it be better to construct terms and then pretty print those?
+        def pretty(value: Any, at: Trace, soFar: String): String = at match {
+          case Trace.Root(_) => soFar
+          case Trace.Child(childCtor, field, outer) => childCtor.fields match
+            case Nil => C.panic("reportNonExhaustive: impossible, child trace has no fields")
+            case _ =>
+              val acc = s"${childCtor.name}(${childCtor.fields.map { f => if f == field then soFar else "_" }.mkString(", ")})"
+              pretty(value, outer, acc)
+        }
+        val root = pp"${value}"
+        C.error(pp"Non exhaustive pattern matching, missing case ${pretty(value, at, root)}")
       case Missing.Default(tpe, at) =>
         C.error(pp"Non exhaustive pattern matching, scrutinees of type ${tpe} require a default case")
     }

EDIT: for completeness, here's what the code above outputs for the original problem:

Non exhaustive pattern matching, missing case Cons(_, Cons(_, _))

from effekt.

Related Issues (20)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.