add hlint

.hlint.yaml

@@ -0,0 +1,73 @@
+# HLint configuration file
+# https://github.com/ndmitchell/hlint
+##########################
+
+# This file contains a template configuration file, which is typically
+# placed as .hlint.yaml in the root of your project
+
+
+# Warnings currently triggered by your code
+- ignore: {name: "Use <$>"} # 20 hints
+- ignore: {name: "Use if"} # 9 hints
+
+# 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,3 @@
-{-# 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,3 @@
-{-# LANGUAGE OverloadedLabels  #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 module Cornelis.Goals where
@@ -65,9 +64,9 @@ 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
-                     )
+      True -> Just ( p_line goal .-. p_line pos
+                   , p_col goal .-. p_col pos  -- TODO: This formula looks fishy
+                   )
 
 
 ------------------------------------------------------------------------------
@@ -150,20 +149,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
   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

@@ -20,7 +20,7 @@ import           Data.Coerce (coerce)
 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)
@@ -89,7 +89,7 @@ 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
@@ -113,10 +113,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

src/Cornelis/Offsets.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE TypeFamilies #-}

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) = pure (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
 

src/Cornelis/Utils.hs

@@ -1,7 +1,6 @@
 {-# LANGUAGE DerivingVia       #-}
 {-# LANGUAGE OverloadedLabels  #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ViewPatterns      #-}
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 
@@ -49,7 +48,7 @@ savingCurrentWindow m = do
 
 windowsForBuffer :: Buffer -> Neovim env [Window]
 windowsForBuffer b = do
-  wins <- fmap V.toList $ vim_get_windows
+  wins <- fmap V.toList vim_get_windows
   fmap catMaybes $ for wins $ \w -> do
     wb <- window_get_buffer w
     pure $ case wb == b of
@@ -58,7 +57,7 @@ windowsForBuffer b = do
 
 visibleBuffers :: Neovim env [(Window, Buffer)]
 visibleBuffers = do
-  wins <- fmap V.toList $ vim_get_windows
+  wins <- fmap V.toList vim_get_windows
   for wins $ \w -> fmap (w, ) $ window_get_buffer w
 
 criticalFailure :: Text -> Neovim env a

src/Cornelis/Vim.hs

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

src/Lib.hs

@@ -3,14 +3,14 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TemplateHaskell   #-}
 {-# LANGUAGE ViewPatterns      #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 
 module Lib where
 
 import           Control.Arrow ((&&&))
 import           Control.Concurrent.Chan.Unagi
 import           Control.Lens
-import           Control.Monad (forever)
-import           Control.Monad (when)
+import           Control.Monad (forever, when)
 import           Control.Monad.State.Class (gets)
 import           Cornelis.Config (getConfig)
 import           Cornelis.Debug (reportExceptions)
@@ -55,7 +55,7 @@ respond b (DisplayInfo dp) = do
 -- Update the buffer's interaction points map
 respond b (InteractionPoints ips) = do
   let ips' = mapMaybe sequenceInteractionPoint ips
-  modifyBufferStuff b $ #bs_ips .~ (M.fromList $ fmap (ip_id &&& id) ips')
+  modifyBufferStuff b $ #bs_ips .~ M.fromList (fmap (ip_id &&& id) ips')
 -- Replace a function clause
 respond b (MakeCase mkcase) = do
   doMakeCase b mkcase
@@ -89,9 +89,9 @@ respond b ClearHighlighting = do
 respond b (HighlightingInfo _remove hl) = do
   extmap <- highlightBuffer b hl
   modifyBufferStuff b $ \bs -> bs
-    & #bs_ip_exts <>~ M.compose extmap (fmap ip_interval' $ bs_ips $ bs)
+    & #bs_ip_exts <>~ M.compose extmap (fmap ip_interval' $ bs_ips bs)
 respond _ (RunningInfo _ x) = reportInfo x
-respond _ (ClearRunningInfo) = reportInfo ""
+respond _ ClearRunningInfo = reportInfo ""
 respond b (JumpToError _ pos) = do
   -- HACK(sandy): See #113. Agda reports error positions in sent messages
   -- relative to the *bytes* attached to the sent interval. But we can't easily
@@ -109,6 +109,7 @@ respond b (JumpToError _ pos) = do
 respond _ Status{} = pure ()
 respond _ (Unknown k _) = reportError k
 
+{-# HLINT ignore doMakeCase "Functor law" #-}
 doMakeCase :: Buffer -> MakeCase -> Neovim CornelisEnv ()
 doMakeCase b (RegularCase Function clauses ip) = do
   int' <- getIpInterval b ip

src/Plugin.hs

@@ -2,7 +2,6 @@
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE OverloadedLabels  #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ViewPatterns      #-}
 
 module Plugin where
 
@@ -75,7 +74,7 @@ doLoad :: CommandArguments -> Neovim CornelisEnv ()
 doLoad = const load
 
 atomicSwapIORef :: IORef a -> a -> IO a
-atomicSwapIORef r x = atomicModifyIORef r (\y -> (x , y))
+atomicSwapIORef r x = atomicModifyIORef r (x,)
 
 load :: Neovim CornelisEnv ()
 load = withAgda $ withCurrentBuffer $ \b -> do
@@ -95,11 +94,11 @@ questionToMeta b = withBufferStuff b $ \bs -> do
 
   res <- fmap fold $ for (sortOn (Down . iStart . ip_interval') ips) $ \ip -> do
     int <- getIpInterval b ip
-    getGoalContents_maybe b ip >>= \case
+    getGoalContentsMaybe b ip >>= \case
       -- We only don't have a goal contents if we are a ? goal
       Nothing -> do
         replaceInterval b int "{! !}"
-        let int' = int { iEnd = (iStart int) `addCol` Offset 5 }
+        let int' = int { iEnd = iStart int `addCol` Offset 5 }
         void $ highlightInterval b int' CornelisHole
         modifyBufferStuff b $
           #bs_ips %~ M.insert (ip_id ip) (ip & #ip_intervalM . #_Identity .~ int')
@@ -260,7 +259,7 @@ inferType :: Rewrite -> Neovim CornelisEnv ()
 inferType mode = withAgda $ do
     cmd <- withGoalContentsOrPrompt "Infer type of what?"
         (\goal -> pure . Cmd_infer mode (ip_id goal) NoRange)
-        (\input -> pure $ Cmd_infer_toplevel mode input)
+        (pure . Cmd_infer_toplevel mode)
     runInteraction cmd
 
 

test/PropertySpec.hs

@@ -46,7 +46,7 @@ spec = parallel $ do
       $ counterexample (show pn)
       $ counterexample (show $ strs !! rowidx)
       $ withVim (Seconds 1) $ \w b -> do
-          buffer_set_lines b 0 (-1) False $ V.fromList $ fmap T.pack $ strs
+          buffer_set_lines b 0 (-1) False $ V.fromList $ fmap T.pack strs
           setWindowCursor w pn
           ObjectInt row' <- vim_call_function "line" $ V.fromList [ObjectString "."]
           ObjectInt col' <- vim_call_function "virtcol" $ V.fromList [ObjectString "."]

test/TestSpec.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE NumDecimals       #-}
-{-# LANGUAGE OverloadedLabels  #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 module TestSpec where

test/Utils.hs

@@ -1,6 +1,5 @@
 {-# LANGUAGE NumDecimals       #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ViewPatterns      #-}
 
 module Utils
   ( module Utils
@@ -67,7 +66,7 @@ intervention b d m = do
 
 withVim :: Seconds -> (Window -> Buffer -> Neovim () ()) -> IO ()
 withVim secs m = do
-  let withNeovimEmbedded f a = testWithEmbeddedNeovim f secs () a
+  let withNeovimEmbedded f = testWithEmbeddedNeovim f secs ()
   withNeovimEmbedded Nothing $ do
     b <- nvim_create_buf False False
     w <- vim_get_current_window
@@ -93,11 +92,11 @@ vimSpec
     -> (Window -> Buffer -> Neovim CornelisEnv ())
     -> Spec
 vimSpec name secs fp m = do
-  let withNeovimEmbedded f a = testWithEmbeddedNeovim f secs () a
+  let withNeovimEmbedded f = testWithEmbeddedNeovim f secs ()
   it name $ do
     withSystemTempFile "test.agda" $ \fp' h -> do
       hPutStr h $ "module " <> takeBaseName fp' <> " where\n"
-      hPutStr h =<< fmap (unlines . tail . lines) (readFile fp)
+      hPutStr h . unlines . tail . lines =<< readFile fp
       hFlush h
       withNeovimEmbedded Nothing $ do
         env <- cornelisInit