From 8752f320b22a66ab8564bc24b8cfe7f693b49ace Mon Sep 17 00:00:00 2001
From: Craig Roy <croyzor@users.noreply.github.com>
Date: Tue, 29 Oct 2024 17:00:25 +0000
Subject: [PATCH] fix: Check that all overs and unders are used in toplevel
 defs (#48)

---
 brat/Brat/Checker.hs                             | 16 ++++++++++++++--
 brat/Brat/Load.hs                                | 10 ++++++++--
 brat/test/golden/error/toplevel-leftovers.brat   |  2 ++
 .../golden/error/toplevel-leftovers.brat.golden  |  9 +++++++++
 brat/test/golden/error/toplevel-leftovers2.brat  |  2 ++
 .../golden/error/toplevel-leftovers2.brat.golden | 10 ++++++++++
 brat/test/golden/error/toplevel-leftovers3.brat  |  2 ++
 .../golden/error/toplevel-leftovers3.brat.golden |  6 ++++++
 8 files changed, 53 insertions(+), 4 deletions(-)
 create mode 100644 brat/test/golden/error/toplevel-leftovers.brat
 create mode 100644 brat/test/golden/error/toplevel-leftovers.brat.golden
 create mode 100644 brat/test/golden/error/toplevel-leftovers2.brat
 create mode 100644 brat/test/golden/error/toplevel-leftovers2.brat.golden
 create mode 100644 brat/test/golden/error/toplevel-leftovers3.brat
 create mode 100644 brat/test/golden/error/toplevel-leftovers3.brat.golden

diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs
index dcab2a97..12b7ddca 100644
--- a/brat/Brat/Checker.hs
+++ b/brat/Brat/Checker.hs
@@ -614,13 +614,25 @@ checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m)
           -> Checking Src
 checkBody fnName body cty = case body of
   NoLhs tm -> do
-    ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \(overs, unders) -> check tm (overs, unders)
+    ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do
+      (((), ()), leftovers) <- check tm conns
+      checkConnectorsUsed (fcOf tm, fcOf tm) (show tm) conns leftovers
     pure src
   Clauses (c :| cs) -> do
     fc <- req AskFC
-    ((box, _), _) <- makeBox (fnName ++ ".box") cty (check (WC fc (Lambda c cs)))
+    ((box, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do
+      let tm = Lambda c cs
+      (((), ()), leftovers) <- check (WC fc tm) conns
+      checkConnectorsUsed (fcOf (fst c), fcOf (snd c)) (show tm) conns leftovers
     pure box
   Undefined -> err (InternalError "Checking undefined clause")
+ where
+  checkConnectorsUsed _ _ _ ([], []) = pure ()
+  checkConnectorsUsed (_, tmFC) tm (_, unders) ([], rightUnders) = localFC tmFC $
+    let numUsed = length unders - length rightUnders in
+     err (TypeMismatch tm (showRow unders) (showRow (take numUsed unders)))
+  checkConnectorsUsed (absFC, _) _ _ (rightOvers, _) = localFC absFC $
+    typeErr ("Inputs " ++ showRow rightOvers ++ " weren't used")
 
 -- Constructs row from a list of ends and types. Uses standardize to ensure that dependency is
 -- detected. Fills in the first bot ends from a stack. The stack grows every time we go under
diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs
index 628aee65..0e16e288 100644
--- a/brat/Brat/Load.hs
+++ b/brat/Brat/Load.hs
@@ -67,8 +67,14 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do
     -- We must have a row of nouns as the definition
     Nothing -> case fnBody of
       NoLhs body -> do
-        (((), ()), ((), [])) <- let ?my = Braty in check body ((), to_define)
-        pure ()
+        (((), ()), ((), rightUnders)) <- let ?my = Braty in check body ((), to_define)
+        case rightUnders of
+          [] -> pure ()
+          _ -> localFC (fcOf body) $
+               err $
+               TypeMismatch fnName
+               (showRow to_define)
+               (showRow $ filter ((`notElem` (fst <$> rightUnders)) . fst) to_define)
       Undefined -> error "No body in `checkDecl`"
       ThunkOf _ -> case fnSig of
         Some ro -> err $ ExpectedThunk (showMode Braty) (show ro)
diff --git a/brat/test/golden/error/toplevel-leftovers.brat b/brat/test/golden/error/toplevel-leftovers.brat
new file mode 100644
index 00000000..1cfe2a71
--- /dev/null
+++ b/brat/test/golden/error/toplevel-leftovers.brat
@@ -0,0 +1,2 @@
+f :: Nat, Bool
+f = 42
diff --git a/brat/test/golden/error/toplevel-leftovers.brat.golden b/brat/test/golden/error/toplevel-leftovers.brat.golden
new file mode 100644
index 00000000..0dd4cdbf
--- /dev/null
+++ b/brat/test/golden/error/toplevel-leftovers.brat.golden
@@ -0,0 +1,9 @@
+Error in test/golden/error/toplevel-leftovers.brat@FC {start = Pos {line = 2, col = 5}, end = Pos {line = 2, col = 7}}:
+f = 42
+    ^^
+
+  Type mismatch when checking f
+Expected: (a1 :: Nat), (b1 :: Bool)
+But got:  (a1 :: Nat)
+
+
diff --git a/brat/test/golden/error/toplevel-leftovers2.brat b/brat/test/golden/error/toplevel-leftovers2.brat
new file mode 100644
index 00000000..61874fcf
--- /dev/null
+++ b/brat/test/golden/error/toplevel-leftovers2.brat
@@ -0,0 +1,2 @@
+f(Nat) -> Nat, Bool
+f(x) = x
diff --git a/brat/test/golden/error/toplevel-leftovers2.brat.golden b/brat/test/golden/error/toplevel-leftovers2.brat.golden
new file mode 100644
index 00000000..cd19807c
--- /dev/null
+++ b/brat/test/golden/error/toplevel-leftovers2.brat.golden
@@ -0,0 +1,10 @@
+Error in test/golden/error/toplevel-leftovers2.brat@FC {start = Pos {line = 2, col = 8}, end = Pos {line = 2, col = 9}}:
+f(x) = x
+       ^
+
+  Type mismatch when checking x => 「x」
+
+Expected: (a1 :: Nat), (b1 :: Bool)
+But got:  (a1 :: Nat)
+
+
diff --git a/brat/test/golden/error/toplevel-leftovers3.brat b/brat/test/golden/error/toplevel-leftovers3.brat
new file mode 100644
index 00000000..b4c98d84
--- /dev/null
+++ b/brat/test/golden/error/toplevel-leftovers3.brat
@@ -0,0 +1,2 @@
+f(Nat, Bool) -> Nat
+f(x) = x
diff --git a/brat/test/golden/error/toplevel-leftovers3.brat.golden b/brat/test/golden/error/toplevel-leftovers3.brat.golden
new file mode 100644
index 00000000..1d094a04
--- /dev/null
+++ b/brat/test/golden/error/toplevel-leftovers3.brat.golden
@@ -0,0 +1,6 @@
+Error in test/golden/error/toplevel-leftovers3.brat@FC {start = Pos {line = 2, col = 2}, end = Pos {line = 2, col = 5}}:
+f(x) = x
+ ^^^
+
+  Type error: Inputs (b1 :: Bool) weren't used
+