Pattern Unification & Implicits

[jfdm]

Steps to Reproduce

Take the following Idris program that describes a view (Compare) over two vectors, the corresponding covering function (compare), and a function (eq) that uses the covering function.

module Bug

import Data.Vect

public export
data Compare : (xs : Vect n a)
            -> (ys : Vect m a) -> Type where
  Empty      :                  Compare     Nil    Nil
  LeftHeavy  : Lazy (Compare xs ys) -> Compare (x::xs)     ys
  RightHeavy : Lazy (Compare xs ys) -> Compare     xs  (y::ys)
  Balanced   : Lazy (Compare xs ys) -> Compare (x::xs) (y::ys)

public export
compare : (xs : Vect n a)
       -> (ys : Vect m a)
             -> Compare xs ys
compare [] [] = Empty
compare [] (y :: ys) with (compare Nil ys)
  compare [] (y :: ys) | rest = RightHeavy rest
compare (x :: xs) [] with (compare xs Nil)
  compare (x :: xs) [] | rest = LeftHeavy rest
compare (x :: xs) (y :: ys) with (compare xs ys)
  compare (x :: xs) (y :: ys) | rest = Balanced rest

public export
eq : (xs : Vect n a)
  -> (ys : Vect m a)
        -> Bool
eq xs ys with (compare xs ys)
  eq [] [] | Empty = True
  eq (x :: xs) ys | (LeftHeavy _) = False
  eq xs (y :: ys) | (RightHeavy _) = False
  eq (x :: xs) (y :: ys) | (Balanced _) = True && eq xs ys

Expected Behavior

Should I be correct in expecting this program to type-check successfully.

Observed Behavior

Idris2 complains with:

- + Errors (1)
 `-- Bug.idr line 30 col 13:
     While processing left hand side of with block in eq. When unifying Compare [] [] and Compare [] [].
     Pattern variable n unifies with: 0.

     Bug.idr:29:1--29:3
         |
      29 | eq xs ys with (compare xs ys)
         | ^^

     Suggestion: Use the same name for both pattern variables, since they unify.

I suspect what is happening that the internals are complaining about implicit parameters n and m. When they are brought into scope as implicit parameters on the LHS everything typechecks.

[Russoul]

Maybe Idris forgets to abstract over n when elaborating the 'with' expression ? Or as another possibility: it abstracts over it but in the generated function representing the 'with' n is not properly destructed by patterns on LHS (basically n being a 'match-any' pattern variable in each clause) ?

[gallais]

My understanding is that the generated with function has the shape f {n} [] [] but now that both xs and ys have been pattern-matched on n unifies with 0 and Idris would really like the user to write 0 instead. The problem of course is that the user in this case is the idris elaborator for with functions and you get told off for something that's not your mistake.

This is handled in Agda by letting users (both top level ones and elaborators) write whatever they want and internally turning these type of n in f {n} [] [] into n@0.