Improve dot patterns

Allow matching rather than unification, as long as it doesn't solve any
metavariables on the way. I noticed a potential unification bug on the
way, forgetting to update whether holes are solved when unifying
argument lists.

src/Core/LinearCheck.idr

@@ -205,10 +205,9 @@ mutual
            Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
                 | _ => throw (UndefinedName fc n)
            let expand = case (definition gdef, rig) of
-                             (Hole _ _, _) => False
-                             (Guess _ _, _) => False
                              (_, Rig0) => False
-                             _ => True
+                             (PMDef _ _ _ _ _, _) => True
+                             _ => False
            if expand
               then expandMeta rig erase env n idx (definition gdef) args
               else do let ty : ClosedTerm

src/Core/Unify.idr

@@ -18,11 +18,13 @@ import Data.List.Views
 public export
 data UnifyMode = InLHS
                | InTerm
+               | InDot
                | InSearch
 
 Eq UnifyMode where
    InLHS == InLHS = True
    InTerm == InTerm = True
+   InDot == InDot = True
    InSearch == InSearch = True
    _ == _ = False
 
@@ -167,7 +169,8 @@ unifyArgs mode loc env [] [] = pure success
 unifyArgs mode loc env (cx :: cxs) (cy :: cys)
     = do res <- unify mode loc env cx cy
          case constraints res of
-              [] => unifyArgs mode loc env cxs cys
+              [] => do cs <- unifyArgs mode loc env cxs cys
+                       pure (union res cs)
               _ => do cs <- unifyArgs mode loc env cxs cys
                       -- TODO: Fix this bit! See p59 Ulf's thesis
 --                       c <- addConstraint 
@@ -753,6 +756,14 @@ mutual
       = if hdx == hdy
            then unifyArgs InSearch loc env xargs yargs
            else unifyApp False InSearch loc env xfc fx xargs (NApp yfc fy yargs)
+  doUnifyBothApps InDot loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
+      = if hdx == hdy
+           then do logC 5 (do defs <- get Ctxt
+                              xs <- traverse (quote defs env) xargs
+                              ys <- traverse (quote defs env) yargs
+                              pure ("Unifying dot pattern args " ++ show xs ++ " " ++ show ys))
+                   unifyArgs InDot loc env xargs yargs
+           else unifyApp False InDot loc env xfc fx xargs (NApp yfc fy yargs)
   doUnifyBothApps mode loc env xfc fx ax yfc fy ay
       = unifyApp False mode loc env xfc fx ax (NApp yfc fy ay)
 
@@ -1143,7 +1154,7 @@ checkDots
              -- A dot is okay if the constraint is solvable *without solving
              -- any additional holes*
              catch
-               (do cs <- unify InTerm fc env x y
+               (do cs <- unify InDot fc env x y
                    defs <- get Ctxt
                    Just ndef <- lookupDefExact n (gamma defs)
                         | Nothing => throw (UndefinedName fc n)

tests/ttimp/dot001/Dot3.yaff

@@ -10,10 +10,10 @@ data Baz : Nat -> Type where
      AddThings : (x : Nat) -> (y : Nat) -> Baz (plus x y)
 
 addBaz : (x : Nat) -> Baz x -> Nat
-addBaz (plus $x $y) (AddThings $x $y) = plus x y
+addBaz (plus x y) (AddThings x y) = plus x y
 
--- Can't unify arguments of plus with the AddThings arguments (we'd need to
--- match rather than unify)
+-- Can't unify because holes are solved as part of the dot pattern (plus x x)
+-- which would accidentally lead to a non-linear pattern
 addBaz3 : (x : Nat) -> Baz x -> Nat
-addBaz3 (plus $x $y) (AddThings _ _) = plus x y
+addBaz3 (plus x x) (AddThings _ _) = plus x x
 

tests/ttimp/dot001/Dot4.yaff

@@ -10,9 +10,9 @@ data Baz : Nat -> Type where
      AddThings : (x : Nat) -> (y : Nat) -> Baz (plus x y)
 
 addBaz : (x : Nat) -> Baz x -> Nat
-addBaz (plus $x $y) (AddThings $x $y) = plus x y
+addBaz (plus x y) (AddThings _ _) = plus x y
 
--- Can't unify because we can't infer the arguments to 'plus'
+-- Can't unify because of the repeated argument
 addBaz4 : (x : Nat) -> Baz x -> Nat
-addBaz4 (plus _ _) (AddThings $x $y) = plus x y
+addBaz4 (plus _ _) (AddThings x x) = plus x x
 

tests/ttimp/dot001/expected

@@ -7,9 +7,9 @@ Dot2.yaff:15:10--15:15:Can't match on ($resolved84 ?{P:n:92}_[] ?{P:m:92}_[]) (N
 Yaffle> Bye for now!
 Processing as TTImp
 Dot3.yaff:18:1--20:1:When elaborating left hand side of Main.addBaz3:
-Dot3.yaff:18:10--18:15:Can't match on ($resolved84 ?{P:x:97}_[] ?{P:y:97}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved84 ?Main.{_:13}_[] ?Main.{_:14}_[])
+Dot3.yaff:18:10--18:15:Can't match on ($resolved84 ?{P:x:97}_[] ?{P:x:97}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved84 ?{P:x:97}_[] ?{P:x:97}_[])
 Yaffle> Bye for now!
 Processing as TTImp
-Dot4.yaff:17:1--19:1:When elaborating left hand side of Main.addBaz4:
-Dot4.yaff:17:10--17:15:Can't match on ($resolved84 ?Main.{_:13}_[] ?Main.{_:14}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved84 ?{P:x:97}_[] ?{P:y:97}_[])
+Dot4.yaff:13:1--16:1:When elaborating left hand side of Main.addBaz:
+Dot4.yaff:13:9--13:14:Can't match on ($resolved84 ?{P:x:91}_[] ?{P:y:91}_[]) (Not a constructor application or primitive) - it elaborates to ($resolved84 ?{P:x:91}_[] ?{P:y:91}_[])
 Yaffle> Bye for now!