Incorrect reduction of pattern matching

[edwinb]

Issue by ziman
Saturday May 02, 2020 at 10:49 GMT
Originally opened as edwinb/Idris2-boot#346

---

Steps to Reproduce

import Data.Vect

%default total

infix 3 .<=.
(.<=.) : Int -> Int -> Bool
(.<=.) p q = case (p, q) of
  (0, _) => True
  _ => False

countGreater : (thr : Int) -> (ctx : Vect n Int) -> Nat
countGreater thr [] = Z
countGreater thr (x :: xs) with (x .<=. thr)
  countGreater thr (x :: xs) | True = countGreater thr xs
  countGreater thr (x :: xs) | False = S $ countGreater thr xs

-- map a variable from the old context to the erased context
-- where we erase all bindings less than or equal to the threshold
eraseVar : (thr : Int) -> (ctx : Vect n Int) -> Fin n -> Maybe (Fin (countGreater thr ctx))
eraseVar thr (x :: xs) j with (x .<=. thr)
  eraseVar thr (x :: xs) FZ | True = Nothing
  eraseVar thr (x :: xs) FZ | False = Just FZ
  eraseVar thr (x :: xs) (FS i) | True = FS <$> eraseVar thr xs i  -- WRONG
  eraseVar thr (x :: xs) (FS i) | False = FS <$> eraseVar thr xs i

boom : Maybe (Fin 1)
boom = eraseVar 0 [0, 1] (FS FZ)

{-

Main> :t boom
Main.boom : Maybe (Fin 1)
Main> boom
Just (FS FZ)

-}

Expected Behavior

The function eraseVar should fail to check on the RHS of its second-to-last clause.

The correct RHS, eraseVar thr xs i, should check.

Observed Behavior

The program checks and Idris claims that Just (FS FZ) : Maybe (Fin 1).

The correct RHS, eraseVar thr xs i, does not check.

Other observations

Somehow the definition of .<=. is crucial to this problem. If I use just <= from Prelude in the with expressions, everything works as expected.

[edwinb]

Comment by ziman
Saturday May 02, 2020 at 11:02 GMT

---

The following definition makes the program work as expected again.

(.<=.) : Int -> Int -> Bool
0 .<=. _ = True
_ .<=. _ = False

[edwinb]

Comment by ziman
Saturday May 02, 2020 at 11:13 GMT

---

I can manually lift the case expression.

foo : (Int, Int) -> Bool
foo (0, _) = True
foo _ = False

infix 3 .<=.
(.<=.) : Int -> Int -> Bool
(.<=.) p q = foo (p, q)

Then :di foo shows something interesting:

Compile time tree:
case {arg:0}[0] : [__] of
  { Builtin.MkPair {e:0} {e:1} {e:2} {e:3}
    => case {e:2}[2] : [__] of
        { 0 => Prelude.True
        | _ => Prelude.False
        }
  | _ => Prelude.False
  }

The generated case tree has a default branch, even though it's not necessary.

Indeed, the default branch does seem to get in the way because if I change the second clause of foo to be foo (_, _) = False, the bug is fixed.

I wonder if the evaluator somehow mistakenly concludes Mismatch on the MkPair constructor instead of getting stuck, and proceeds to the default case.

[edwinb]

Comment by ziman
Saturday May 02, 2020 at 12:36 GMT

---

    -- Default case matches against any *concrete* value
    tryAlt env loc opts fc stk val (DefaultCase sc) def
         = if concrete val
              then evalTree env loc opts fc stk sc def
              else def
      where
        concrete : NF free -> Bool
        concrete (NDCon _ _ _ _ _) = True
        concrete (NTCon _ _ _ _ _) = True
        concrete (NPrimVal _ _) = True
        concrete (NBind _ _ _ _) = True
        concrete (NType _) = True
        concrete _ = False

I'll try marking only Lam and Pi as concrete.

[edwinb]

Comment by ziman
Saturday May 02, 2020 at 12:59 GMT

---

Changing the definition of concrete to the following does not seem to have any effect.

concrete : NF free -> Bool
concrete (NDCon _ _ _ _ _) = True
concrete (NTCon _ _ _ _ _) = True
concrete (NPrimVal _ _) = True
concrete (NBind _ _ (Lam _ _ _) _) = True
concrete (NBind _ _ (Pi _ _ _) _) = True
concrete (NType _) = True
concrete _ = False