Apply lints

brat/Brat/Checker.hs

@@ -660,7 +660,7 @@ check' (Of n e) ((), unders) = case ?my of
       (elems, unders, rightUnders) <- getVecs len unders
       pure ((tgt, el):elems, (tgt, ty):unders, rightUnders)
   getVecs _ unders = pure ([], [], unders)
-check' Hope ((), ((tgt, ty):unders)) = case (?my, ty) of
+check' Hope ((), (tgt, ty):unders) = case (?my, ty) of
   (Braty, Left _k) -> do
     fc <- req AskFC
     req (ANewHope (toEnd tgt, fc))
@@ -731,7 +731,7 @@ checkBody fnName body cty = do
     NoLhs tm -> pure (tm, (fcOf tm, fcOf tm))
     Clauses (c :| cs) -> do
       fc <- req AskFC
-      pure $ (WC fc (Lambda c cs), (bimap fcOf fcOf c))
+      pure (WC fc (Lambda c cs), bimap fcOf fcOf c)
     Undefined -> err (InternalError "Checking undefined clause")
   ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do
     (((), ()), leftovers) <- check tm conns

brat/Brat/Checker/Helpers.hs

@@ -380,10 +380,10 @@ valueToBinder Braty = Right
 valueToBinder Kerny = id
 
 defineSrc :: Src -> Val Z -> Checking ()
-defineSrc src v = defineEnd (ExEnd (end src)) v
+defineSrc src = defineEnd (ExEnd (end src))
 
 defineTgt :: Tgt -> Val Z -> Checking ()
-defineTgt tgt v = defineEnd (InEnd (end tgt)) v
+defineTgt tgt = defineEnd (InEnd (end tgt))
 
 declareSrc :: Src -> Modey m -> BinderType m -> Checking ()
 declareSrc src my ty = req (Declare (ExEnd (end src)) my ty)

brat/Brat/Checker/Monad.hs

@@ -282,7 +282,7 @@ handler (Req s k) ctx g
       RemoveHope e -> let hset = hopeSet ctx in
                         if M.member e hset
                         then handler (k ()) (ctx { hopeSet = M.delete e hset }) g
-                        else (Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e))))
+                        else Left (dumbErr (InternalError ("Trying to remove hole not in set: " ++ show e)))
 
 howStuck :: Val n -> Stuck
 howStuck (VApp (VPar e) _) = AwaitingAny (S.singleton e)

brat/Brat/Checker/SolveHoles.hs

@@ -15,6 +15,7 @@ import Bwd
 import Hasochism
 import Util (zipSameLength)
 
+import Data.Bifunctor (second)
 import Data.Foldable (traverse_)
 import Data.Functor
 import qualified Data.Map as M
@@ -106,11 +107,12 @@ typeEqRow :: Modey m
           -> Ro m lv top0
           -> Ro m lv top1
           -> Either ErrorMsg (Some ((Ny :* Stack Z TypeKind :* Stack Z Sem) -- The new stack of kinds and fresh level
-                                   :* (((:~:) top0) :* ((:~:) top1))) -- Proofs both input rows have same length (quantified over by Some)
+                                   :* ((:~:) top0 :* (:~:) top1)) -- Proofs both input rows have same length (quantified over by Some)
                              ,[Checking ()] -- subproblems to run in parallel
                              )
 typeEqRow _ _ stuff R0 R0 = pure (Some (stuff :* (Refl :* Refl)), [])
-typeEqRow m tm stuff (RPr (_,ty1) ro1) (RPr (_,ty2) ro2) = typeEqRow m tm stuff ro1 ro2 <&> \(res, probs) -> (res, (typeEq tm stuff (kindForMode m) ty1 ty2):probs)
+typeEqRow m tm stuff (RPr (_,ty1) ro1) (RPr (_,ty2) ro2) = typeEqRow m tm stuff ro1 ro2 <&> second
+  ((:) (typeEq tm stuff (kindForMode m) ty1 ty2))
 typeEqRow m tm (ny :* kz :* semz) (REx (_,k1) ro1) (REx (_,k2) ro2) | k1 == k2 = typeEqRow m tm (Sy ny :* (kz :<< k1) :* (semz :<< semLvl ny)) ro1 ro2
 typeEqRow _ _ _ _ _ = Left $ TypeErr "Mismatched rows"
 
@@ -144,13 +146,13 @@ typeEqRigid tm lvkz (TypeFor m []) (VCon c args) (VCon c' args') | c == c' =
 typeEqRigid tm lvkz (Star []) (VFun m0 (ins0 :->> outs0)) (VFun m1 (ins1 :->> outs1)) | Just Refl <- testEquality m0 m1 = do
   probs :: [Checking ()] <- throwLeft $ typeEqRow m0 tm lvkz ins0 ins1 >>= \case -- this is in Either ErrorMsg
         (Some (lvkz :* (Refl :* Refl)), ps1) -> typeEqRow m0 tm lvkz outs0 outs1 <&> (ps1++) . snd
-  traverse_ id probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized
+  sequenceA_ probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized
 typeEqRigid tm lvkz (TypeFor _ []) (VSum m0 rs0) (VSum m1 rs1)
   | Just Refl <- testEquality m0 m1 = case zipSameLength rs0 rs1 of
       Nothing -> typeErr "Mismatched sum lengths"
-      Just rs -> traverse eqVariant rs >>= (traverse_ id . concat)
+      Just rs -> traverse eqVariant rs >>= (sequenceA_ . concat)
  where
-  eqVariant (Some r0, Some r1) = throwLeft $ (snd <$> typeEqRow m0 tm lvkz r0 r1)
+  eqVariant (Some r0, Some r1) = throwLeft (snd <$> typeEqRow m0 tm lvkz r0 r1)
 typeEqRigid tm _ _ v0 v1 = err $ TypeMismatch tm (show v0) (show v1)
 
 wire :: (Src, Val Z, Tgt) -> Checking ()

brat/Brat/Eval.hs

@@ -302,9 +302,7 @@ eqTests tm lvkz = go
 -- We can have bogus failures here because we're not normalising under lambdas
 -- N.B. the value argument is normalised.
 doesntOccur :: End -> Val n -> Either ErrorMsg ()
-doesntOccur e (VNum nv) = case getNumVar nv of
-  Just e' -> collision e e'
-  _ -> pure ()
+doesntOccur e (VNum nv) = traverse_ (collision e) (getNumVar nv)
  where
   getNumVar :: NumVal (VVar n) -> Maybe End
   getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of

brat/Control/Monad/Freer.hs

@@ -21,7 +21,7 @@ updateEnd (News m) e = case M.lookup e m of
 -- The RHS of the operation is the newer news
 -- Invariant: The domains of these Newses are disjoint
 instance Semigroup News where
-  (News m1) <> n2@(News m2) = News (m2 `M.union` (M.map (/// n2) m1))
+  (News m1) <> n2@(News m2) = News (m2 `M.union` M.map (/// n2) m1)
 
 instance Monoid News where
   mempty = News M.empty