Incomplete exhaustiveness checking in Gren 0.6.3

[aramiscd]

I have found that Gren 0.6.3 compiles the following function without any objections:

fn r =
    when r is
        { a = False, b = True } -> 1
        { a = True, b = False } -> 2

That surprised me because the following branches are missing:

        { a = False, b = False } -> ...
        { a = True, b = True } -> ...

The exhaustiveness checking does evidently not function as it should. It seems to only affect record patterns, which is plausible because they were added/extended most recently.

[gilramir]

For a quick check, I asked Google Gemini to examine the isExhaustive function. It says:

The bug in your isExhaustive function lies in how you handle Record Patterns. Specifically, when the function encounters a record, it attempts to check for exhaustiveness by iterating through each field independently and concatenating the results.

The Problem: Logical "OR" vs. Logical "AND"

In pattern matching, a list of records is only exhaustive if all combinations of their fields are covered. Your current implementation uses concatMap isAltExhaustive fieldNames.

This effectively says: "The set is exhaustive if field A is exhaustive OR field B is exhaustive." In reality, if you have two fields (Color and Shape), you need to ensure that every Color is matched with every Shape. By checking them one by one and flattening the list, you are only checking if every value for one of those fields appears at least once in the matrix, ignoring the cross-product of the other fields.

---

Where the Bug Lives

Look at this specific block in your code:

let fieldNames = Map.keys baseRecord

    isAltExhaustive fieldName =
      map (asRecordPattern fieldName) $
        isExhaustive
          (Maybe.mapMaybe (specializeRowByRecordField fieldName) matrix)
          n
    -- ...
 in concatMap isAltExhaustive fieldNames -- <--- THE BUG

How to Fix It

To check if a record is exhaustive, you cannot treat the fields as alternative branches (like you do with Algebraic Data Type constructors). Instead, you must nest the checks. You need to verify field 1, and for the remaining rows that match field 1, verify field 2, and so on.

The Correct Approach:

Instead of concatMap, you should process the fields recursively or by folding over the list of field names.

1. Specialize the matrix for the first field.
2. Find the missing patterns for that field.
3. Recurse to the next field using the remaining matrix context.
4. Combine the results into a single record pattern.

Revised Logic Sketch

You want to transform the record problem into a "positional" problem. A record with fields is essentially a tuple of length .

1. When you encounter a Record, don't iterate through fieldNames and concat.
2. Instead, expand the "width" of your matrix. If a record has fields [A, B], treat the matrix as having columns temporarily.
3. Use the standard Maranget’s algorithm (which your code seems to be based on) to check columns one by one.

Summary of the Logic Error

• Constructors (Union types): Use concatMap (Sum types). You need to check if you've covered Ctor A OR Ctor B OR Ctor C.
• Records (Product types): Use recursion/nesting (Product types). You need to check if you've covered Field A AND Field B.

Would you like me to rewrite the Just baseRecord branch to show how to properly fold over the field names to ensure the cross-product is covered?

I told it "yes".

The complete conversation is at https://gemini.google.com/share/3e1a0300fb8a

[aramiscd]

I forked the compiler and started looking into the problem.

I believe that Gemini has correctly analyzed and described the bug. However, the proposed code adjustments do not fix it. I have adjusted isExhaustive and specializeRowByRecordField as described by Gemini and cannot see any change in how incomplete patterns are handled. Can anyone confirm this?

I will continue to work on this in my spare time. However, this could take a while. I don't feel comfortable pushing ahead with LLM-driven solutions. Or rather, I lack the expertise and confidence in LLMs to do so. Instead, I will study the algorithm and understand how the code implements it. Then I will restructure the code so that I can better understand and adapt it. If I can offer a solution, I will get back to you. If someone else has provided a solution more quickly in the meantime, that's fine with me too.

[gilramir]

In a branch in my fork of the repo, I added a unit test to exercise this logic.
Perhaps it will be useful to someone.
https://github.com/gilramir/gren-compiler/tree/exhaustive-check-test

[robinheghan]

I remember that when implementing this I tried to follow the logic for custom types very closely. There should be little difference in how exhaustiveness is calculated between the patterns { a = True, b = False } and Variant True False.

The one difference is that we're a bit lenient with records, treating { a = True } as the equivalent of { a = True, b = _ } (type is { a | a : Bool }).

[robinheghan]

Maybe there's a bug in the code that tries to be lenient with records, so that it thinks there is a { a = _, b = _ } pattern at the end?

[gilramir]

I have enhanced the unit tests in my branch at main...gilramir:gren-compiler:exhaustive-check-test

It now tests both cases which we discussed on Discord:

Case 1

fn r =
    when r is
        { a = False, b = True } -> 1
        { a = True, b = False } -> 2

Case 2

case 2 - variable assignment
    when r is
        Nothing -> "Nothing"
        Just { first = { key = lKey, value = lValue }, rest } -> lKey

With the current compiler code, test case 1 fails with:

  1) Nitpick.PatternMatches, PatternMatches tests, Test 1 bool matrix is not exhaustive
       expected: [["a : True, b : True","a : False, b : False"]]
        but got: []

and test case 2 passes.

With my attempted, but incorrect fix, test case 1 passes, but test case 2 fails with:

  1) Nitpick.PatternMatches, PatternMatches tests, Test 2 record destructuring is exhaustive
       expected: []
        but got: [["Just (first : anything, rest : anything )"]]

For the record, I'll post what my attempted fix was. This code replaces the code in this "let" block in isExhaustive:

                        Just baseRecord ->
                          let fieldNames = Map.keys baseRecord

My fix, (which was 99% Qwen AI's thinking, and 1% mine, although after it's creation I made sure to understand it), was:

                              -- Extract all record patterns and convert to field matrices
                              getRecordFields :: [Pattern] -> Maybe [Pattern]
                              getRecordFields [Record recordMap] =
                                Just [Maybe.fromMaybe Anything (Map.lookup fieldName recordMap) | fieldName <- fieldNames]
                              getRecordFields [Anything] =
                                Just (replicate (length fieldNames) Anything)
                              getRecordFields _ = Nothing

                              fieldMatrix = Maybe.mapMaybe getRecordFields matrix

                              -- Check if we have any record patterns to work with
                           in if null fieldMatrix
                                   then [replicate n Anything]  -- No records, so anything is missing
                                   else
                                     let missingFieldCombinations = isExhaustive fieldMatrix (length fieldNames)
                                         -- Convert each missing field combination back to a record pattern
                                         toRecordPattern :: [Pattern] -> [Pattern]
                                         toRecordPattern fields = [Record (Map.fromList (zip fieldNames fields))]
                                      in map toRecordPattern missingFieldCombinations