feat: Complain when we have remaining Nat-kinded holes

brat/Brat/Checker.hs

@@ -957,7 +957,7 @@ run :: VEnv
     -> Namespace
     -> Checking a
     -> Either Error (a, ([TypedHole], Store, Graph, Namespace))
-run ve initStore ns m =
+run ve initStore ns m = do
   let ctx = Ctx { globalVEnv = ve
                 , store = initStore
                 -- TODO: fill with default constructors
@@ -966,5 +966,16 @@ run ve initStore ns m =
                 , typeConstructors = defaultTypeConstructors
                 , aliasTable = M.empty
                 , hopeSet = S.empty
-                } in
-    (\(a,ctx,(holes, graph),ns) -> (a, (holes, store ctx, graph, ns))) <$> handler m ctx mempty ns
+                }
+  (a,ctx,(holes, graph),ns) <- handler m ctx mempty ns
+  let tyMap = typeMap $ store ctx
+  -- If the hopeSet has any remaining holes with kind Nat, we need to abort.
+  -- Even though we didn't need them for typechecking problems, our runtime
+  -- behaviour depends on the values of the holes, which we can't account for.
+  case S.toList $ S.filter (isNatKinded tyMap) (hopeSet ctx) of
+    [] -> pure (a, (holes, store ctx, graph, ns))
+    hs -> Left $ Err Nothing (RemainingNatHopes (show <$> hs))
+ where
+  isNatKinded tyMap e = case tyMap M.! e of
+    EndType Braty (Left Nat) -> True
+    _ -> False

brat/Brat/Error.hs

@@ -80,6 +80,7 @@ data ErrorMsg
  | WrongModeForType String
  -- TODO: Add file context here
  | CompilingHoles [String]
+ | RemainingNatHopes [String]
 
 instance Show ErrorMsg where
   show (TypeErr x) = "Type error: " ++ x
@@ -161,9 +162,10 @@ instance Show ErrorMsg where
   -- TODO: Make all of these use existing errors
   show (UnificationError str) = "Unification error: " ++ str
   show UnreachableBranch = "Branch cannot be reached"
-  show (CompilingHoles hs) = unlines ("Can't compile file with remaining holes": indent hs)
-   where
-    indent = fmap ("  " ++)
+  show (CompilingHoles hs) = unlines ("Can't compile file with remaining holes":indent hs)
+  show (RemainingNatHopes hs) = unlines ("Expected to work out values for these holes:":indent (indent hs))
+
+indent = fmap ("  " ++)
 
 data Error = Err { fc  :: Maybe FC
                  , msg :: ErrorMsg

brat/test/golden/error/remaining-nat-hopes.brat

@@ -0,0 +1,8 @@
+show(n :: #) -> []
+show(_) = []
+
+read([]) -> n :: #
+read([]) = 42
+
+bad :: []
+bad = let _ = read([]) in show(!)

brat/test/golden/error/remaining-nat-hopes.brat.golden

@@ -0,0 +1,5 @@
+Error in test/golden/error/remaining-nat-hopes.brat:
+  Expected to work out values for these holes:
+    In checking_check_defs_1_bad_2__2 0
+
+