Merge remote-tracking branch 'origin/main' into holes

CQCL · Dec 3, 2024 · ef85987 · ef85987
2 parents 0cef0d3 + 9bad538
commit ef85987
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs
@@ -729,9 +729,9 @@ checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m)
 checkBody fnName body cty = do
   (tm, (absFC, tmFC)) <- case body of
     NoLhs tm -> pure (tm, (fcOf tm, fcOf tm))
-    Clauses (c :| cs) -> do
+    Clauses (c@(abs, tm) :| cs) -> do
       fc <- req AskFC
-      pure (WC fc (Lambda c cs), bimap fcOf fcOf c)
+      pure (WC fc (Lambda c cs), (fcOf abs, fcOf tm))
     Undefined -> err (InternalError "Checking undefined clause")
   ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do
     (((), ()), leftovers) <- check tm conns
@@ -806,7 +806,7 @@ kindCheck ((hungry, k@(TypeFor m [])):unders) (Con c arg) = req (TLup (m, c)) >>
         -- the thing we *do* define kindOut as
 
         (_, argUnders, [(kindOut,_)], (_ :<< _va, _)) <-
-          next "aliasargs" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0)
+          next "kc_alias" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0)
         -- arg is a juxtaposition
         (args, emptyUnders) <- kindCheck (second (\(Left k) -> k) <$> argUnders) (unWC arg)
         ensureEmpty "alias args" emptyUnders

diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs
@@ -250,14 +250,14 @@ getThunks :: Modey m
 getThunks _ [] = pure ([], [], [])
 getThunks Braty ((src, Right ty):rest) = do
   ty <- eval S0 ty
-  (src, (ss :->> ts)) <- vectorise Braty (src, ty)
+  (src, ss :->> ts) <- vectorise Braty (src, ty)
   (node, unders, overs, _) <- let ?my = Braty in
                                 anext "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts
   (nodes, unders', overs') <- getThunks Braty rest
   pure (node:nodes, unders <> unders', overs <> overs')
 getThunks Kerny ((src, Right ty):rest) = do
   ty <- eval S0 ty
-  (src, (ss :->> ts)) <- vectorise Kerny (src,ty)
+  (src, ss :->> ts) <- vectorise Kerny (src,ty)
   (node, unders, overs, _) <- let ?my = Kerny in anext "Splice" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts
   (nodes, unders', overs') <- getThunks Kerny rest
   pure (node:nodes, unders <> unders', overs <> overs')

diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs
@@ -142,7 +142,7 @@ solveConstructor my src (c, abs) ty p = do
   (CArgs pats _ patRo argRo, (tycon, tyargs)) <- lookupConstructor my c ty
   -- Create a row of hypothetical kinds which contextualise the arguments to the
   -- constructor.
-  -- These need to be Tgts because we don't know how to compute them dynamically/
+  -- These need to be Tgts because we don't know how to compute them dynamically
   (_, _, _, stuff) <- next "type_args" Hypo (S0, Some (Zy :* S0)) patRo R0
   (node, _, patArgWires, _) <- let ?my = my in anext "val_args" Hypo stuff R0 argRo
   trackM ("Constructor " ++ show c ++ "; type " ++ show ty)

diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs
@@ -115,7 +115,7 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do
 
 loadAlias :: TypeAlias -> Checking (QualName, Alias)
 loadAlias (TypeAlias fc name args body) = localFC fc $ do
-  (_, [(hhungry, Left k)], _, _) <- next "aliasargs" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0
+  (_, [(hhungry, Left k)], _, _) <- next "load_alias" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0
   let abs = WC fc $ foldr ((:||:) . APat . Bind . fst) AEmpty args
   ([v], unders) <- kindCheck [(hhungry, k)] $ Th (WC fc (Lambda (abs, WC fc body) []))
   ensureEmpty "loadAlias unders" unders