add hlint

.github/workflows/lint.yml

@@ -0,0 +1,21 @@
+name: lint
+on:
+  pull_request:
+  push:
+    branches:
+      - master
+
+jobs:
+  hlint:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: 'Set up HLint'
+      uses: haskell-actions/hlint-setup@v2
+
+    - name: 'Run HLint'
+      uses: haskell-actions/hlint-run@v2
+      with:
+        path: src/
+        fail-on: warning

.hlint.yaml

@@ -0,0 +1,67 @@
+# HLint configuration file
+# https://github.com/ndmitchell/hlint
+##########################
+# Warnings currently triggered by your code
+
+
+# Specify additional command line arguments
+#
+# - arguments: [--color, --cpp-simple, -XQuasiQuotes]
+
+
+# Control which extensions/flags/modules/functions can be used
+#
+# - extensions:
+#   - default: false # all extension are banned by default
+#   - name: [PatternGuards, ViewPatterns] # only these listed extensions can be used
+#   - {name: CPP, within: CrossPlatform} # CPP can only be used in a given module
+#
+# - flags:
+#   - {name: -w, within: []} # -w is allowed nowhere
+#
+# - modules:
+#   - {name: [Data.Set, Data.HashSet], as: Set} # if you import Data.Set qualified, it must be as 'Set'
+#   - {name: Control.Arrow, within: []} # Certain modules are banned entirely
+#
+# - functions:
+#   - {name: unsafePerformIO, within: []} # unsafePerformIO can only appear in no modules
+
+
+# Add custom hints for this project
+#
+# Will suggest replacing "wibbleMany [myvar]" with "wibbleOne myvar"
+# - error: {lhs: "wibbleMany [x]", rhs: wibbleOne x}
+
+# The hints are named by the string they display in warning messages.
+# For example, if you see a warning starting like
+#
+# Main.hs:116:51: Warning: Redundant ==
+#
+# You can refer to that hint with `{name: Redundant ==}` (see below).
+
+# Turn on hints that are off by default
+#
+# Ban "module X(module X) where", to require a real export list
+# - warn: {name: Use explicit module export list}
+#
+# Replace a $ b $ c with a . b $ c
+# - group: {name: dollar, enabled: true}
+#
+# Generalise map to fmap, ++ to <>
+# - group: {name: generalise, enabled: true}
+#
+# Warn on use of partial functions
+# - group: {name: partial, enabled: true}
+
+
+# Ignore some builtin hints
+# - ignore: {name: Use let}
+# - ignore: {name: Use const, within: SpecialModule} # Only within certain modules
+
+
+# Define some custom infix operators
+# - fixity: infixr 3 ~^#^~
+
+
+# To generate a suitable file for HLint do:
+# $ hlint --default > .hlint.yaml

src/Cornelis/Agda.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE NumDecimals       #-}
+
 {-# LANGUAGE OverloadedLabels  #-}
 {-# LANGUAGE OverloadedStrings #-}
 

src/Cornelis/Diff.hs

@@ -49,7 +49,7 @@ modifyDiff buf f = do
 
 -- | Reset the diff to an empty diff.
 resetDiff :: BufferNum -> Neovim CornelisEnv ()
-resetDiff buf = modifyDiff buf $ \_ -> (D.emptyDiff, ())
+resetDiff buf = modifyDiff buf $ const (D.emptyDiff, ())
 
 -- | Add a buffer update (insertion or deletion) to the diff.
 -- The buffer update event coming from Vim is structured exactly how the diff-loc

src/Cornelis/Goals.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE OverloadedLabels  #-}
+
 {-# LANGUAGE OverloadedStrings #-}
 
 module Cornelis.Goals where
@@ -63,23 +63,19 @@ findGoal hunt = withAgda $ do
 prevGoal :: Neovim CornelisEnv ()
 prevGoal =
   findGoal $ \pos goal ->
-    case pos > goal of
-      False -> Nothing
-      True -> Just $ ( p_line goal .-. p_line pos
-                     , p_col goal .-. p_col pos  -- TODO: This formula looks fishy
-                     )
+    (if pos > goal then Just ( p_line goal .-. p_line pos
+               , p_col goal .-. p_col pos  -- TODO: This formula looks fishy
+               ) else Nothing)
 
 
 ------------------------------------------------------------------------------
 -- | Move the vim cursor to the next interaction point.
 nextGoal :: Neovim CornelisEnv ()
 nextGoal =
   findGoal $ \pos goal ->
-    case pos < goal of
-      False -> Nothing
-      True -> Just $ Down ( p_line goal .-. p_line pos
-                          , p_col goal .-. p_col pos
-                          )
+    (if pos < goal then Just $ Down ( p_line goal .-. p_line pos
+                    , p_col goal .-. p_col pos
+                    ) else Nothing)
 
 ------------------------------------------------------------------------------
 -- | Uses highlighting extmarks to determine what a hole is; since the user
@@ -89,7 +85,7 @@ getGoalAtCursor = do
   w <- nvim_get_current_win
   b <- window_get_buffer w
   p <- getWindowCursor w
-  fmap (b, ) $ getGoalAtPos b p
+  (b, ) <$> getGoalAtPos b p
 
 
 getGoalAtPos
@@ -100,9 +96,7 @@ getGoalAtPos b p = do
   fmap (getFirst . fold) $ withBufferStuff b $ \bs -> do
     for (bs_ips bs) $ \ip -> do
       int <- getIpInterval b ip
-      pure $ case containsPoint int p of
-        False -> mempty
-        True -> pure $ ip { ip_intervalM = Identity int }
+      pure (if containsPoint int p then pure $ ip { ip_intervalM = Identity int } else mempty)
 
 ------------------------------------------------------------------------------
 -- | Run a continuation on a goal at the current position in the current
@@ -114,7 +108,7 @@ withGoalAtCursor f = getGoalAtCursor >>= \case
    (_, Nothing) -> do
      reportInfo "No goal at cursor"
      pure Nothing
-   (b, Just ip) -> fmap Just $ f b ip
+   (b, Just ip) -> (Just <$> f b ip)
 
 ------------------------------------------------------------------------------
 -- | Run the first continuation on the goal at the current position,
@@ -150,20 +144,20 @@ withGoalContentsOrPrompt prompt_str on_goal on_no_goal = getGoalAtCursor >>= \ca
 
 ------------------------------------------------------------------------------
 -- | Get the contents of a goal.
-getGoalContents_maybe :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv (Maybe Text)
-getGoalContents_maybe b ip = do
+getGoalContentsMaybe :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv (Maybe Text)
+getGoalContentsMaybe b ip = do
   int <- getIpInterval b ip
-  iv <- fmap T.strip $ getBufferInterval b int
+  iv <- T.strip <$> getBufferInterval b int
   pure $ case iv of
     "?" -> Nothing
          -- Chop off {!, !} and trim any spaces.
-    _ -> Just $ T.strip $ T.dropEnd 2 $ T.drop 2 $ iv
+    _ -> Just $ T.strip $ T.dropEnd 2 $ T.drop 2 iv
 
 
 ------------------------------------------------------------------------------
 -- | Like 'getGoalContents_maybe'.
 getGoalContents :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text
-getGoalContents b ip = fromMaybe "" <$> getGoalContents_maybe b ip
+getGoalContents b ip = fromMaybe "" <$> getGoalContentsMaybe b ip
 
 
 ------------------------------------------------------------------------------

src/Cornelis/Highlighting.hs

@@ -21,7 +21,7 @@ import           Data.Functor ((<&>))
 import           Data.IntervalMap.FingerTree (IntervalMap)
 import qualified Data.IntervalMap.FingerTree as IM
 import qualified Data.Map as M
-import           Data.Maybe (listToMaybe, catMaybes)
+import           Data.Maybe (listToMaybe, catMaybes, mapMaybe)
 import qualified Data.Text as T
 import           Data.Text.Encoding (encodeUtf8)
 import           Data.Traversable (for)
@@ -90,15 +90,13 @@ addHighlight b lis hl = do
   case Interval
            <$> lookupPoint lis (hl_start hl)
            <*> lookupPoint lis (hl_end hl) of
-    Just (int@(Interval start end)) -> do
+    Just int@(Interval start end) -> do
       ext <- setHighlight b int $ parseHighlightGroup hl
 
-      fmap (, ext) $ case isHole hl of
-        False -> pure mempty
-        True -> do
-          let vint = Interval start end
-          aint <- traverse (unvimify b) vint
-          pure $ maybe mempty (M.singleton aint) ext
+      (, ext) <$> (if isHole hl then (do
+        let vint = Interval start end
+        aint <- traverse (unvimify b) vint
+        pure $ maybe mempty (M.singleton aint) ext) else pure mempty)
     Nothing -> pure (mempty, Nothing)
   where
     -- Convert the first atom in a reply to a custom highlight
@@ -114,10 +112,10 @@ addHighlight b lis hl = do
     -- TODO: Investigate whether is is possible/feasible to
     -- attach multiple HL groups to buffer locations.
     parseHighlightGroup :: Highlight -> Maybe HighlightGroup
-    parseHighlightGroup = listToMaybe . catMaybes . map atomToHlGroup . hl_atoms
+    parseHighlightGroup = listToMaybe . mapMaybe atomToHlGroup . hl_atoms
 
     isHole :: Highlight -> Bool
-    isHole = any (== "hole") . hl_atoms
+    isHole = elem "hole" . hl_atoms
 
 setHighlight
     :: Buffer
@@ -143,8 +141,7 @@ setHighlight' b (Interval (Pos sl sc) (Pos el ec)) hl = do
     $ fmap (Just . coerce)
     $ nvim_buf_set_extmark b ns (from0 sl) (from0 sc)
     $ M.fromList
-    $ catMaybes
-    $ [ Just
+    $ catMaybes [ Just
           ( "end_line"
           , ObjectInt $ from0 el
           )
@@ -194,10 +191,10 @@ parseExtmark b
     }
 parseExtmark _ _ = pure Nothing
 
-#if __GLASGOW_HASKELL__ <= 904
+
 hoistMaybe :: Applicative m => Maybe a -> MaybeT m a
 hoistMaybe = MaybeT . pure
-#endif
+
 
 
 getExtmarks :: Buffer -> AgdaPos -> Neovim CornelisEnv [ExtmarkStuff]
@@ -212,7 +209,5 @@ getExtmarks b p = do
   marks <- fmap catMaybes $ traverse (parseExtmark b) $ V.toList res
 
   pure $ marks >>= \es ->
-    case containsPoint (es_interval es) p of
-      False -> mempty
-      True -> [es]
+    (if containsPoint (es_interval es) p then [es] else mempty)
 

src/Cornelis/InfoWin.hs

@@ -70,12 +70,10 @@ showInfoWindow b doc = withBufferStuff b $ \bs -> do
   -- Check if the info win still exists, and if so, just modify it
   found <- fmap or $
     for vis $ \(w, vb) -> do
-      case vb == iw_buffer ib of
-        False -> pure False
-        True -> do
-          writeInfoBuffer ns ib doc
-          resizeInfoWin w ib
-          pure True
+      (if vb == iw_buffer ib then (do
+        writeInfoBuffer ns ib doc
+        resizeInfoWin w ib
+        pure True) else pure False)
 
   -- Otherwise we need to rebuild it
   unless found $ do

src/Cornelis/Offsets.hs

@@ -1,5 +1,5 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DerivingStrategies #-}
+
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -214,11 +214,11 @@ fromBytes t (Index i) | i < 0 = error $ "from bytes underflow" <> show (t, i)
 fromBytes _ (Index 0) = Index 0
 fromBytes t (Index i) | Just (c, str) <- T.uncons t =
   let diff = BS.length $ encodeUtf8 $ T.singleton c
-   in case i - diff >= 0 of
-        True -> Index $ 1 + coerce (fromBytes str (Index (i - diff)))
-        -- We ran out of bytes in the middle of a multibyte character. Just
-        -- return the one we're on, and don't underflow!
-        False -> Index 0
+   in if i - diff >= 0
+      then Index $ 1 + coerce (fromBytes str (Index (i - diff)))
+      -- We ran out of bytes in the middle of a multibyte character. Just
+      -- return the one we're on, and don't underflow!
+      else Index 0
 fromBytes t i = error $ "missing bytes: " <> show (t, i)
 
 addCol :: Pos e i j -> Offset e -> Pos e i j

src/Cornelis/Pretty.hs

@@ -119,7 +119,7 @@ renderWithHlGroups = go [] 0 0
 
 
 prettyType :: C.Type -> Doc HighlightGroup
-prettyType (C.Type ty) = annotate CornelisType $ sep $ fmap pretty $ T.lines ty
+prettyType (C.Type ty) = annotate CornelisType $ sep (pretty <$> T.lines ty)
 
 
 groupScopeSet :: [InScope] -> [[InScope]]
@@ -149,7 +149,7 @@ prettyGoals (GoalSpecific _ scoped ty mhave mboundary mconstraints) =
     [ annotate CornelisTitle "Have:" <+> prettyType have
     | have <- maybeToList mhave
     ] <>
-    [ vcat $ fmap prettyInScopeSet $ groupScopeSet scoped
+    [ vcat (prettyInScopeSet <$> groupScopeSet scoped)
     ] <>
     [ section "Constraints" (fromMaybe [] mconstraints) pretty
     ]
@@ -233,5 +233,5 @@ prettyGoal (GoalInfo name ty) =
 
 prettyError :: Message -> Doc HighlightGroup
 prettyError (Message msg) =
-  let (hdr, body) = fmap (T.drop 1) $ T.break (== '\n') msg in
+  let (hdr, body) = (T.drop 1 <$> T.break (== '\n') msg) in
   vcat [ annotate CornelisError (pretty hdr) , pretty body ]

src/Cornelis/Types.hs

@@ -9,6 +9,8 @@
 {-# LANGUAGE UndecidableInstances  #-}
 
 {-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use camelCase" #-}
 
 module Cornelis.Types
   ( module Cornelis.Types
@@ -207,7 +209,7 @@ ip_interval' :: InteractionPoint Identity -> AgdaInterval
 ip_interval' (InteractionPoint _ (Identity i)) = i
 
 sequenceInteractionPoint :: Applicative f => InteractionPoint f -> f (InteractionPoint Identity)
-sequenceInteractionPoint (InteractionPoint n f) = InteractionPoint <$> pure n <*> fmap Identity f
+sequenceInteractionPoint (InteractionPoint n f) = InteractionPoint n <$> fmap Identity f
 
 
 data NamedPoint = NamedPoint
@@ -307,13 +309,13 @@ data DisplayInfo
   | UnknownDisplayInfo Value
   deriving (Eq, Ord, Show, Generic)
 
-data TypeAux = TypeAux
+newtype TypeAux = TypeAux
   { ta_expr :: Type
   }
 
 instance FromJSON TypeAux where
   parseJSON = withObject "TypeAux" $ \obj ->
-    (TypeAux . Type) <$> obj .: "expr"
+    TypeAux . Type <$> obj .: "expr"
 
 instance FromJSON DisplayInfo where
   parseJSON v = flip (withObject "DisplayInfo") v $ \obj ->

src/Cornelis/Types/Agda.hs

@@ -1,5 +1,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use camelCase" #-}
 
 module Cornelis.Types.Agda where