chore: Fix hlint action and apply changes

.github/workflows/hlint.yaml

@@ -1,6 +1,9 @@
 name: Brat CI
 on:
-  pull_request: []
+  pull_request:
+    branches: [ main ]
+    paths:
+      - "**.hs"
 
 jobs:
   hlint:

brat/.hlint.yaml

@@ -66,7 +66,9 @@
 - ignore: {name: Use newtype instead of data}
 - ignore: {name: Fuse foldr/<$>}
 - ignore: {name: Redundant bracket, within: Brat.Syntax.Value}
+- ignore: {name: Redundant bracket, within: Data.HugrGraph}
 - ignore: {name: Avoid NonEmpty.unzip} # Buggy - false positives
+- ignore: {name: Redundant <&>} # Often making things worse
 
 # Define some custom infix operators
 # - fixity: infixr 3 ~^#^~

brat/Brat/Checker.hs

@@ -757,7 +757,7 @@ checkClause my fnName cty clause = modily my $ do
           trackM $ "[[[[[[TestMatchData\n" ++ show match ++ "\n]]]]]]"
           pure (sol, match, patRo :->> outRo, fmap (Some . (patEz :*) . abstractEndz patEz) <$> defs)
 
-  for defs $ \((name, kind), Some (_ :* val)) -> trackM ("Def: " ++ show ((name, kind), val))
+  for_ defs $ \((name, kind), Some (_ :* val)) -> trackM ("Def: " ++ show ((name, kind), val))
 
   -- Now actually make a box for the RHS and check it
   ((boxPort, _ty), _) <- let ?my = my in makeBox (clauseName ++ "_rhs") rhsCty $ \(rhsOvers, rhsUnders) -> do
@@ -780,7 +780,7 @@ checkClause my fnName cty clause = modily my $ do
      -- would arise if we've not yet defined the outer src
      let vars = fst <$> sol
      env <- mkEnv vars rhsOvers
-     (localEnv (env <> defs) $ "$rhs" -! check @m (rhs clause) ((), rhsUnders))
+     localEnv (env <> defs) $ "$rhs" -! check @m (rhs clause) ((), rhsUnders)
   let NamedPort {end=Ex rhsNode _} = boxPort
   pure (match, rhsNode)
  where
@@ -804,8 +804,8 @@ checkClause my fnName cty clause = modily my $ do
          outPorts <- depOutPorts def
          srcAndTys <- for outPorts (\outport -> (NamedPort outport "",) <$> typeOfEnd Braty (ExEnd outport))
          zx <- pure $ foldl (\sol srcAndTy -> insert ("$" ++ show (end (fst srcAndTy)), srcAndTy) sol) zx srcAndTys
-         (sol, defs) <- worker (zx {-:< entry-}) sol
-         pure ({-(patVar, (src, Left k)):-}sol, ((patVar, k), def):defs)
+         (sol, defs) <- worker zx sol
+         pure (sol, ((patVar, k), def):defs)
     -- Pat vars beginning with '_' aren't in scope, we can ignore them
     -- (but if they're kinded they might come up later as the dependency of something else)
     worker zx (('_':_, _):sol) = worker zx sol
@@ -1085,7 +1085,7 @@ kindCheckRow' :: forall m n
               -> Checking (Int, VEnv, Some (Endz :* Ro m n))
 kindCheckRow' _ ez env (_,i) [] = pure (i, env, Some (ez :* R0))
 
-kindCheckRow' my nys env (name, i) ((Anon ty):rest) = kindCheckRow' my nys env (name, i) ((Named (show i) ty):rest)
+kindCheckRow' my nys env (name, i) ((Anon ty):rest) = kindCheckRow' my nys env (name, i) (Named (show i) ty:rest)
 kindCheckRow' Braty (ny :* s) env (name,i) ((Named p (Left k)):rest) = do -- s is Stack Z n
   let dangling = Ex name (ny2int ny)
   req (Declare (ExEnd dangling) Braty (Left k) Definable) -- assume none are SkolemConst??
@@ -1287,6 +1287,6 @@ runChecking ve initStore ns m = do
     -- show multiple error locations
     hs@((_,fc):_) -> Left $ Err (Just fc) (RemainingNatHopes (show . fst <$> hs))
  where
-  isNatKinded tyMap e = case tyMap M.! (InEnd e) of
+  isNatKinded tyMap e = case tyMap M.! InEnd e of
     (EndType Braty (Left Nat), _) -> True
     _ -> False

brat/Brat/Checker/Helpers.hs

@@ -692,6 +692,7 @@ valPats2Val (k:ks) (v:vs) = do
 valPats2Val [] [] = pure (B0, [])
 valPats2Val _ _ = err $ InternalError "Type args didn't match expected - kindCheck should've sorted it"
 
+{-# ANN traceChecking ("HLint: ignore Redundant pure" :: String) #-}
 traceChecking :: String -> (a -> Checking b) -> (a -> Checking b)
 traceChecking _lbl m a = do
   -- trackM ("Enter " ++ lbl ++ ": " ++ show a)

brat/Brat/Checker/Monad.hs

@@ -136,7 +136,7 @@ wrapper f (Yield st k) = Yield st (wrapper f . k)
 wrapper f (Fork d par c) = Fork d (wrapper f par) (wrapper f c)
 
 wrapper2 :: (forall a. CheckingSig a -> Maybe a) -> Checking v -> Checking v
-wrapper2 f = wrapper (\s -> pure (f s))
+wrapper2 f = wrapper (pure . f)
 
 localAlias :: (QualName, Alias) -> Checking v -> Checking v
 localAlias (name, alias) = wrapper2 (\case
@@ -147,7 +147,7 @@ localFC :: FC -> Checking v -> Checking v
 localFC f = wrapper (\case
   AskFC -> pure $ Just f
   (Throw e@Err{fc=Nothing}) -> req (Throw (e{fc=Just f})) >> error "Throw returned"
-  _ -> pure $ Nothing)
+  _ -> pure Nothing)
 
 localEnv :: (?my :: Modey m) => Env (EnvData m) -> Checking v -> Checking v
 localEnv = case ?my of
@@ -172,7 +172,7 @@ captureOuterLocals n c = do
  where
   helper :: VEnv -> forall a. CheckingSig a -> Checking (Maybe a)
   helper avail (VLup x) | j@(Just new) <- M.lookup x avail =
-    (req $ AddCapture n (x,new)) >> (pure $ Just j)
+    req (AddCapture n (x,new)) >> pure (Just j)
   helper _ _ = pure Nothing
 
 wrapError :: (Error -> Error) -> Checking v -> Checking v
@@ -272,7 +272,7 @@ handler (Req s k) ctx
       AskNS -> error "AskNS in handler, should only happen under `-!`"
       Throw err -> Left err
       LogHole hole -> do (v,ctx,holes) <- handler (k ()) ctx
-                         return (v,ctx,(hole:holes))
+                         return (v,ctx,hole:holes)
       AskFC -> error "AskFC in handler - shouldn't happen, should always be in localFC"
       VLup s -> handler (k $ M.lookup s (globalVEnv ctx)) ctx
       ALup s -> handler (k $ M.lookup s (aliasTable ctx)) ctx
@@ -350,7 +350,7 @@ handler (Define lbl end v k) ctx = let st@Store{typeMap=tm, valueMap=vm} = store
                                       InEnd inport -> case M.lookup inport (dynamicSet ctx) of
                                         Just fc -> track ("Replace " ++ show end ++ " with " ++ show newDynamics) $
                                                  M.union
-                                                 (M.fromList (zip newDynamics (repeat fc)))
+                                                 (M.fromList (map (, fc) newDynamics))
                                                  (M.delete inport (dynamicSet ctx))
                                         Nothing -> dynamicSet ctx
                           })

brat/Brat/Checker/SolveNumbers.hs

@@ -64,13 +64,13 @@ solveNumMeta mine e nv = case (e, numVars nv) of
 
 unifyNum :: (End -> Maybe String) -> NumVal (VVar Z) -> NumVal (VVar Z) -> Checking ()
 unifyNum mine nv0 nv1 = do
-  trailM $ ("unifyNum In\n  " ++ show nv0 ++ "\n  " ++ show nv1)
+  trailM ("unifyNum In\n  " ++ show nv0 ++ "\n  " ++ show nv1)
   nv0 <- numEval S0 nv0
   nv1 <- numEval S0 nv1
   unifyNum' mine (quoteNum Zy nv0) (quoteNum Zy nv1)
   nv0 <- numEval S0 (quoteNum Zy nv0)
   nv1 <- numEval S0 (quoteNum Zy nv1)
-  trailM $ ("unifyNum Out\n  " ++ show (quoteNum Zy nv0) ++ "\n  " ++ show (quoteNum Zy nv1))
+  trailM ("unifyNum Out\n  " ++ show (quoteNum Zy nv0) ++ "\n  " ++ show (quoteNum Zy nv1))
 
 -- Need to keep track of which way we're solving - which side is known/unknown
 -- Things which are dynamically unknown must be Tgts - information flows from Srcs
@@ -101,14 +101,14 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
       (VPar e@(InEnd p), VPar e'@(ExEnd dangling))
        | Just _ <- mine e -> do
           req (Wire (dangling, TNat, p))
-          defineTgt' ("flex-flex In Ex") (NamedPort p "") (VNum (nVar v'))
+          defineTgt' "flex-flex In Ex" (NamedPort p "") (VNum (nVar v'))
        | Just _ <- mine e' -> do
           req (Wire (dangling, TNat, p))
-          defineSrc' ("flex-flex In Ex") (NamedPort dangling "") (VNum (nVar v))
+          defineSrc' "flex-flex In Ex" (NamedPort dangling "") (VNum (nVar v))
        | otherwise -> mkYield "flexFlex" (S.singleton e) >> unifyNum mine (nVar v) (nVar v')
       (VPar e@(InEnd p), VPar e'@(InEnd p'))
        | Just _ <- mine e -> defineTgt' "flex-flex In In1" (NamedPort p "") (VNum (nVar v'))
-       | Just _ <- mine e' -> defineTgt' "flex-flex In In0"(NamedPort p' "") (VNum (nVar v))
+       | Just _ <- mine e' -> defineTgt' "flex-flex In In0" (NamedPort p' "") (VNum (nVar v))
        | otherwise -> mkYield "flexFlex" (S.fromList [e, e']) >> unifyNum mine (nVar v) (nVar v')
 
   lhsStrictMono :: StrictMono (VVar Z) -> NumVal (VVar Z) -> Checking ()
@@ -159,7 +159,7 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
       -- = 2^k + 2^k * y
       -- Hence, the predecessor is (2^k - 1) + (2^k * y)
   demandSucc (NumValue k x) | k > 0 = pure (NumValue (k - 1) x)
-  demandSucc (NumValue 0 (StrictMonoFun (mono@(StrictMono k (Linear (VPar e))))))
+  demandSucc (NumValue 0 (StrictMonoFun mono@(StrictMono k (Linear (VPar e)))))
     | Just loc <- mine e = do
       pred <- loc -! traceChecking "makePred" makePred e
       pure (nPlus ((2^k) - 1) (nVar (VPar pred)))

brat/Brat/Compile/Hugr.hs

@@ -115,12 +115,12 @@ addHole parent sig outPort = do
   hole <- gets (length . holes) -- but anyway
   h <- addNode ("hole " ++ show hole) (parent, OpCustom (holeOp hole sig))
   st <- get
-  put (st { holes = (holes st) :< (h, outPort)})
+  put (st { holes = holes st :< (h, outPort)})
   pure h
 
 filePrefix :: [String] -> Name -> Maybe Name
 filePrefix prefixes (MkName (("checking",_):_filename:ns)) =
-  hasPrefix (["globals"]++prefixes) (MkName ns)
+  hasPrefix ("globals" : prefixes) (MkName ns)
 
 runCheckingInCompile :: Free CheckingSig t -> Compile t
 runCheckingInCompile (Ret t) = pure t
@@ -259,15 +259,14 @@ compileTarget parent tgtN tgt = do
   edges <- compileInEdges parent tgt
   -- registerCompiled tgt tgtN -- really shouldn't be necessary, not reachable
   for_ edges (\(src, tgtPort) -> addEdge (src, Port tgtN tgtPort))
-  pure ()
 
-in_edges :: Name -> Compile [((OutPort, Val Z), Int)]
-in_edges name = gets bratGraph <&> \(_, es) -> [((src, ty), portNum) | (src, ty, In edgTgt portNum) <- es, edgTgt == name]
+inEdges :: Name -> Compile [((OutPort, Val Z), Int)]
+inEdges name = gets bratGraph <&> \(_, es) -> [((src, ty), portNum) | (src, ty, In edgTgt portNum) <- es, edgTgt == name]
 
 compileInEdges :: NodeId -> Name -> Compile [(PortId NodeId, Int)]
 compileInEdges parent name = do
-  in_edges <- in_edges name
-  catMaybes <$> for in_edges (\((src, _), tgtPort) -> getOutPort parent src <&> fmap (, tgtPort))
+  inEdges <- inEdges name
+  catMaybes <$> for inEdges (\((src, _), tgtPort) -> getOutPort parent src <&> fmap (, tgtPort))
 
 compileWithInputs :: NodeId -> Name -> Compile (Maybe NodeId)
 compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
@@ -283,14 +282,14 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
   -- If we only care about the node for typechecking, then drop it and return `Nothing`.
   -- Otherwise, NodeId of compiled node, and list of Hugr in-edges (source and target-port)
   compileNode :: Compile (Maybe (NodeId, [(PortId NodeId, Int)]))
-  compileNode = case (filePrefix ["decl"] name) of
+  compileNode = case filePrefix ["decl"] name of
     Just _ -> error "Kernel contained call to global; should have been a splice"
     _ -> do
       (ns, _) <- gets bratGraph
       let node = ns M.! name
       trackM ("compileNode (" ++ show parent ++ ") " ++ show name ++ " " ++ show node)
       nod_edge_info <- case node of
-        (BratNode _ _ _) -> error "Can't compile classical Brat"
+        (BratNode {}) -> error "Can't compile classical Brat"
         (KernelNode thing ins outs) -> compileNode' thing ins outs
       case nod_edge_info of
         Nothing -> pure Nothing
@@ -323,7 +322,7 @@ compileWithInputs parent name = gets (M.lookup name . compiled) >>= \case
         Nothing -> addHole parent sig outPort
 
     Source -> error "Source found outside of compileBox"
-      
+
     Target -> error "Target found outside of compileBox"
 
     Id | Nothing <- filePrefix ["decl"] name -> default_edges <$> do
@@ -500,10 +499,10 @@ makeConditional :: String    -- Label
 makeConditional lbl parent discrim otherInputs cases = do
   condId <- freshNode "Conditional" parent
   let rows = getSumVariants (snd discrim)
-  (outTyss_cases) <- for (zip (zip [0..] cases) rows) (\((ix, (name, f)), row) -> makeCase condId name ix (row ++ (snd <$> otherInputs)) f)
+  outTyss_cases <- for (zip (zip [0..] cases) rows) (\((ix, (name, f)), row) -> makeCase condId name ix (row ++ (snd <$> otherInputs)) f)
   let outTys = if allRowsEqual (fst <$> outTyss_cases)
                then fst (head outTyss_cases)
-               else (error "Conditional output types didn't match")
+               else error "Conditional output types didn't match"
   let condOp = OpConditional (Conditional rows (snd <$> otherInputs) outTys [("label", lbl)])
   setOp condId condOp
   onHugr $ H.setFirstChildren condId (snd <$> outTyss_cases)

brat/Brat/Compiler.hs

@@ -20,21 +20,21 @@ import Brat.Syntax.Port (NamedPort(..), OutPort(..), InPort(..))
 import Brat.Syntax.Value (Val(VFun))
 
 import Control.Exception (evaluate)
-import Control.Monad (forM, when)
+import Control.Monad (forM_, when)
 import Control.Monad.Except
 import Data.List (intercalate)
 import qualified Data.Map as M
 import qualified Data.ByteString.Lazy as BS
 import Data.Foldable (for_)
-import Data.HugrGraph (HugrGraph, NodeId, to_json)
+import Data.HugrGraph (HugrGraph, NodeId, toJson)
 import System.Exit (die)
 
 printDeclsHoles :: [FilePath] -> String -> IO ()
 printDeclsHoles libDirs file = do
   env <- runExceptT $ loadFilename root libDirs file
   (declEnv, holes, _, _, _) <- eitherIO env
   putStrLn "Decls:"
-  forM (M.toList declEnv) $ \(name, (src_tys, _vdecl)) ->
+  forM_ (M.toList declEnv) $ \(name, (src_tys, _vdecl)) ->
     putStrLn $ show name ++ " :: " ++ intercalate ", " (map (show . snd) src_tys)
   putStrLn ""
   putStrLn "Holes:"
@@ -94,16 +94,16 @@ compileFile libDirs file = do
   (newRoot, (declEnv, holes, st, outerGraph, _)) <- compileToGraph libDirs file
   let venv = M.map fst declEnv
   case holes of
-    [] -> let box_decls = (M.keys declEnv) >>= (findBoxes venv outerGraph)
-          in Right <$> (evaluate -- turns 'error' into IO 'die'
-            $ M.fromList [(n, let (hugr, holes) = compileKernel (newRoot, st, outerGraph) "root" n
-                               in (hugr, map fst holes))
-                         | n <- box_decls])
+    [] -> let box_decls = M.keys declEnv >>= findBoxes venv outerGraph
+          in Right <$> evaluate -- turns 'error' into IO 'die'
+              (M.fromList [(n, let (hugr, holes) = compileKernel (newRoot, st, outerGraph) "root" n
+                                in (hugr, map fst holes))
+                          | n <- box_decls])
     hs -> pure $ Left (CompilingHoles hs)
  where
   findBoxes :: VEnv -> Graph -> QualName -> [Name]
   findBoxes venv (ns, es) name = case M.lookup name venv of
-        Nothing -> error $ (show name) ++ ".... not found in VEnv"
+        Nothing -> error $ show name ++ ".... not found in VEnv"
         Just vals -> vals >>= \(NamedPort (Ex n _) _, _) -> case M.lookup n ns of
             Just (BratNode Id _ _) ->
                [src | (Ex src 0, _, In tgt _) <- es, tgt == n, isKernelBox src ns]
@@ -117,6 +117,6 @@ compileAndPrintFile :: [FilePath] -> String -> IO ()
 compileAndPrintFile libDirs file = compileFile libDirs file >>= \case
   Right hs -> for_ (M.toList hs) $ \(n, (hugr, splices)) -> do
     putStrLn $ "Compiled box: " ++ show n
-    BS.putStr (to_json hugr)
+    BS.putStr (toJson hugr)
     putStrLn $ "With splices: " ++ show splices
   Left err -> die (show err)

brat/Brat/Dot.hs

@@ -15,10 +15,9 @@ import qualified Data.Map as M
 import qualified Data.Set as S
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Text.Lazy (pack, unpack)
-import Data.Maybe (fromMaybe)
+import Data.Maybe ( fromMaybe, fromJust )
 import Data.Bifunctor (first)
 import Data.Graph (reachable, transposeG)
-import Data.Maybe (fromJust)
 import Data.Tuple.HT (snd3)
 
 
@@ -57,7 +56,7 @@ toDotString (ns,ws) cs = unpack . GV.printDotGraph $ GV.graphElemsToDot params v
   getRefEdge x (KernelNode (Splice (Ex y _)) _ _) = [(Name' y, x, EvalEdge)]
   getRefEdge x (BratNode (Box src tgt) _ _) = [(x, Name' src, SrcEdge), (x, Name' tgt, SrcEdge)]
   getRefEdge x (BratNode (PatternMatch (p:|pats)) _ _) =
-    [ (x, Name' innerBox, CaseEdge) | (_, innerBox) <- (p:pats) ]
+    [ (x, Name' innerBox, CaseEdge) | (_, innerBox) <- p:pats ]
   getRefEdge _ _ = []
 
   -- Map from node to cluster. Clusters are identified by their containing Box node.

brat/Brat/Eval.hs

@@ -134,7 +134,7 @@ quoteCTy lvy my ga (ins :->> outs) = quoteRo my ga ins lvy >>= \case
     (_, Some (outs' :* _)) -> pure (ins' :->> outs')
 
 quoteNum ::  Ny lv -> NumVal SVar -> NumVal (VVar lv)
-quoteNum lvy num = fmap (quoteVar lvy) num
+quoteNum lvy = fmap (quoteVar lvy)
 
 -- first number is next Lvl to use in Value
 --         require every Lvl in Sem is < n (converted by n - 1 - lvl), else must fail at runtime

brat/Brat/Load.hs

@@ -155,7 +155,7 @@ loadStmtsWithEnv ns (oldDeclEnv, oldHoles, oldStore, oldGraph, oldCaps) (fname,
       (_, unders, overs, _) <- prefix -! next (show name) thing (S0, Some (Zy :* S0)) ins outs
       pure ((name, VDecl d{fnSig=sig}), (unders, overs))
   trackM "finished kind checking"
-  unless (length holes == 0) $ error "Should be no holes from kind-checking"
+  unless (null holes) $ error "Should be no holes from kind-checking"
   unless (M.null capSets) $ error "Should be no captures from kind-checking"
   -- A list of local functions (read: with bodies) to define with checkDecl
   let to_define = M.fromList [ (name, unders) | ((name, VDecl decl), (unders, _)) <- entries, fnLocality decl == Local ]