Tuples not treated as valid patterns in parameter declarations

[alicelogos]

When type-checking the following code:

#lang rzk-1

#define test1
  ( A : U)
  ( B : (a : A) → U)
  ( C : (a : A) → (b : B a) → U)
  : U
  := (((a , b) , c) : Σ (a : A , b : B a) , C a b) → U
  
#define test2
  ( A : U)
  ( B : (a : A) → U)
  ( C : (a : A) → (b : B a) → U)
  : U
  := ((a , b , c) : Σ (a : A , b : B a) , C a b) → U

Observed behavior:

Type-checking test1 works as expected, but type-checking test2 results in the following error:

rzk: ERROR: expected a pattern but got
  (a, b, c)
CallStack (from HasCallStack):
  error, called at src/Language/Rzk/Free/Syntax.hs:344:15 in rzk-0.7.5-EJ2uiUYTFnEGW7fnYMZZSu:Language.Rzk.Free.Syntax

Expected behavior:

Is this behavior intentional? It seems weird to me that tuples are not treated as valid patterns in parameter declarations, and I would expect tuples to be valid patterns in this context.

Suggested fix:

I looked at the source code at src/Language/Rzk/Free/Syntax.hs:344 and found the following implementation:

unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern
unsafeTermToPattern = ttp
  where
    ttp = \case
      Rzk.Unit loc                        -> Rzk.PatternUnit loc
      Rzk.Var loc x                       -> Rzk.PatternVar loc x
      Rzk.Pair loc l r                    -> Rzk.PatternPair loc (ttp l) (ttp r)
      term -> error ("ERROR: expected a pattern but got\n  " ++ Rzk.printTree term)

It seems that extending this function with an additional case to handle tuples might resolve the issue:

      Rzk.Tuple loc t1 t2 ts              -> Rzk.PatternTuple loc (ttp t1) (ttp t2) (map ttp ts)

However, I am not familiar with the full codebase, and I haven’t set up a development environment to verify if this modification is correct.

[fizruk]

@alicelogos Thanks for spotting this! I believe you are absolutely right and the fix is that simple. Would you be willing to submit a PR?