agda/.hlint.yaml

# 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: "Avoid lambda using `infix`"}
- ignore: {name: "Avoid lambda"}
- ignore: {name: "Eta reduce"}
- ignore: {name: "Evaluate"}
- ignore: {name: "Fuse foldr/map"}
- ignore: {name: "Fuse mapM/map"}
- ignore: {name: "Hoist not"}
- ignore: {name: "Move brackets to avoid $"}
- ignore: {name: "Reduce duplication"}
- ignore: {name: "Redundant $"}
- ignore: {name: "Redundant <$>"}
- ignore: {name: "Redundant bracket"}
- ignore: {name: "Redundant case"}
- ignore: {name: "Redundant guard"}
- ignore: {name: "Redundant if"}
- ignore: {name: "Redundant lambda"}
- ignore: {name: "Redundant multi-way if"}
- ignore: {name: "Redundant return"}
- ignore: {name: "Redundant section"}
- ignore: {name: "Redundant variable capture"}
- ignore: {name: "Replace case with fromMaybe"}
- ignore: {name: "Replace case with maybe"}
- ignore: {name: "Use &&"}
- ignore: {name: "Use ++"}
- ignore: {name: "Use :"}
- ignore: {name: "Use <$"}
- ignore: {name: "Use <$>"}
- ignore: {name: "Use <=<"}
- ignore: {name: "Use >"}
- ignore: {name: "Use Just"}
- ignore: {name: "Use camelCase"}
- ignore: {name: "Use const"}
# Andreas, 2021-02-15
# Silence specific hlint warnings, e.g.
# https://github.com/agda/agda/pull/5214/checks?check_run_id=1909201141
- ignore: {name: "Use curry", within: Agda.TypeChecking.Reduce.reduceWithBlocker }
- ignore: {name: "Use empty"}
# Andreas, 2021-03-03
# "Use fewer imports" is quite silly if one has imports under #if.
- ignore: {name: "Use fewer imports"}
- ignore:
    name: "Use fmap"
    within:
      - Agda.TypeChecking.Rules.Application.checkPrimTrans
      - Agda.TypeChecking.Primitive.Cubical.primTrans'
      - Agda.TypeChecking.Primitive.Cubical.primComp
      - Agda.Syntax.Concrete.Operators.parsePat
- ignore: {name: "Use fromMaybe"}
- ignore: {name: "Use id"}
- ignore: {name: "Use infix"}
- ignore: {name: "Use intercalate"}
- ignore: {name: "Use lambda-case"}
- ignore: {name: "Use list comprehension"}
- ignore: {name: "Use list literal pattern"}
- ignore: {name: "Use list literal"}
- ignore: {name: "Use mapMaybe"}
- ignore: {name: "Use maximum"}
- ignore: {name: "Use maybe"}
- ignore: {name: "Use mconcat"}
- ignore: {name: "Use newtype instead of data"}
- ignore: {name: "Use notElem"}
- ignore: {name: "Use null"}
- ignore: {name: "Use record patterns"}
- ignore: {name: "Use second"}
- ignore: {name: "Use section"}
- ignore: {name: "Use sequenceA"}
- ignore: {name: "Use ||"}


# Specify additional command line arguments
#
# - arguments: [--color, --cpp-simple, -XQuasiQuotes]
- arguments: [
  -XBangPatterns,
  -XConstraintKinds,
  -XDefaultSignatures,
  -XDeriveDataTypeable,
  -XDeriveFoldable,
  -XDeriveFunctor,
  -XDeriveGeneric,
  -XDeriveTraversable,
  -XExistentialQuantification,
  -XFlexibleContexts,
  -XFlexibleInstances,
  -XFunctionalDependencies,
  -XGeneralizedNewtypeDeriving,
  -XInstanceSigs,
  -XLambdaCase,
  -XMultiParamTypeClasses,
  -XMultiWayIf,
  -XNamedFieldPuns,
  -XOverloadedStrings,
  -XPatternSynonyms,
  -XRankNTypes,
  -XRecordWildCards,
  -XScopedTypeVariables,
  -XStandaloneDeriving,
  -XTupleSections,
  -XTypeFamilies,
  -XTypeSynonymInstances,
  # hlint (3.1.6, anyway), seems to assume -XTypeApplications,
  # which causes a parsing error in some cases.
  # (At the time of this note, a parse error in Agda.TypeChecking.Generalize)
  -XNoTypeApplications,
]

# 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}


# 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}


# 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