fix: Check that all overs and unders are used in toplevel defs (#48)

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

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)

brat/test/golden/error/toplevel-leftovers.brat

@@ -0,0 +1,2 @@
+f :: Nat, Bool
+f = 42

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)
+
+

brat/test/golden/error/toplevel-leftovers2.brat

@@ -0,0 +1,2 @@
+f(Nat) -> Nat, Bool
+f(x) = x

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)
+
+

brat/test/golden/error/toplevel-leftovers3.brat

@@ -0,0 +1,2 @@
+f(Nat, Bool) -> Nat
+f(x) = x

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
+