[pre-commit.ci] auto fixes from pre-commit.com hooks

for more information, see https://pre-commit.ci

vehicle-syntax/src/Vehicle/Syntax/AST/Decl.hs

@@ -157,4 +157,4 @@ instance Pretty Annotation where
     AnnProperty -> "@property"
 
 isProperty :: [Annotation] -> Bool
-isProperty anns = AnnProperty `elem` anns
+isProperty anns = AnnProperty `elem` anns

vehicle-syntax/src/Vehicle/Syntax/Builtin/TypeClass.hs

@@ -103,4 +103,4 @@ instance Pretty TypeClassOp where
     OrderTC op -> pretty op
     MapTC -> "map"
     FoldTC -> "fold"
-    QuantifierTC q -> pretty q
+    QuantifierTC q -> pretty q

vehicle/src/Vehicle/Compile/Error.hs

@@ -38,7 +38,7 @@ type MonadCompile m =
 --------------------------------------------------------------------------------
 -- Typing errors
 
-data MissingExplicitArgError builtin = MissingExplicitArgError 
+data MissingExplicitArgError builtin = MissingExplicitArgError
   { _ctx :: NamedBoundCtx
   , explicitBinder :: Binder builtin
   , nonExplicitArg :: Arg builtin
@@ -61,7 +61,7 @@ newtype FailedUnificationConstraintsError builtin = FailedUnificationConstraints
   { failedConstraints :: NonEmpty (WithContext (UnificationConstraint builtin))
   } deriving (Show)
 
-data FailedInstanceConstraintError builtin = 
+data FailedInstanceConstraintError builtin =
   FailedInstanceConstraintError
   { _freeEnv :: FreeEnv builtin
   , failedConstraint :: WithContext (InstanceConstraint builtin)
@@ -254,4 +254,4 @@ instance Pretty VehicleError where
   pretty (DError text) = unAnnotate text
 
 fixText :: Doc ann -> Doc ann
-fixText t = "Fix:" <+> t
+fixText t = "Fix:" <+> t

vehicle/src/Vehicle/Compile/Print/Builtin.hs

@@ -158,4 +158,4 @@ isCoercionExpr :: PrintableBuiltin builtin => Expr builtin -> Bool
 isCoercionExpr = \case
   Builtin _ b -> isCoercion b
   App (Builtin _ b) _ -> isCoercion b
-  _ -> False
+  _ -> False

vehicle/src/Vehicle/Compile/Print/Error.hs

@@ -680,7 +680,7 @@ instance MeaningfulError CompileError where
                   <+> "be used as the dimension of a dataset"
                   <+> "(networks will be supported later)."
           }
-      
+
 
     --------------------
     -- Backend errors --

vehicle/src/Vehicle/Compile/Print/TypingError.hs

@@ -268,7 +268,7 @@ typeRestrictionError (TypeRestrictionOrigin freeEnv (ident, p) sort typ) _candid
           RestrictedParameter NonInferable -> map pretty [Bool, Index, Nat, Rat]
           RestrictedDataset -> ["List A    " <+> datasetElementTypes, "Vector A n" <+> datasetElementTypes]
           RestrictedNetwork -> ["Tensor Rat [a_1, ..., a_n] -> Tensor Rat [b_1, ..., b_n]  (where 'a_i' and 'b_i' are all constants at compile time)"]
-        
+
         datasetElementTypes = "(where A is either `Index n`, `Nat`, `Rat`, `List A`, `Vector A n`)"
 
         prettyAllowedTypes :: [Doc a] -> Doc a

vehicle/src/Vehicle/Compile/Resource.hs

@@ -63,4 +63,4 @@ instance FromJSON NetworkBaseType
 
 instance Pretty NetworkBaseType where
   pretty = \case
-    NetworkRatType -> pretty Rat
+    NetworkRatType -> pretty Rat

vehicle/src/Vehicle/Compile/Type.hs

@@ -104,7 +104,7 @@ typeCheckAbstractDef p ident defSort uncheckedType = do
   checkedType <- checkDeclType ident uncheckedType
   finalCheckedType <- restrictAbstractDefType defSort (ident, p) checkedType
   let checkedDecl = DefAbstract p ident defSort finalCheckedType
-  
+
   solveConstraints (Just checkedDecl)
   substCheckedType <- substMetas finalCheckedType
 

vehicle/src/Vehicle/Compile/Type/Builtin/Standard.hs

@@ -60,7 +60,7 @@ typeOfTypeClass tc = case tc of
   ValidNetworkTensorType -> type0 ~> type0
   ValidDatasetType -> type0 ~> type0
   ValidDatasetElementType -> type0 ~> type0
-  
+
 typeOfTypeClassOp :: (HasStandardBuiltins builtin, BuiltinHasStandardTypeClasses builtin) => TypeClassOp -> DSLExpr builtin
 typeOfTypeClassOp b = case b of
   NegTC -> typeOfTCOp1 hasNeg

vehicle/src/Vehicle/Compile/Type/Constraint/InstanceBuiltins.hs

@@ -86,7 +86,7 @@ allInstances =
           -- ValidDatasetType --
           ----------------------
           ( forAllTypes $ \t ->
-              validDatasetElementType t .~~~> 
+              validDatasetElementType t .~~~>
                 validDatasetType (tList t)
           , implLam "t" type0 $ \t ->
               instLam "r1" (validDatasetElementType t) $ \_ ->
@@ -95,7 +95,7 @@ allInstances =
           ),
           ( forAllTypes $ \t ->
               forAllIrrelevantNat "n" $ \n ->
-                validDatasetElementType t .~~~> 
+                validDatasetElementType t .~~~>
                   validDatasetType (tVector t n)
           , implLam "t" type0 $ \t ->
               irrelImplNatLam "n" $ \_n ->
@@ -104,7 +104,7 @@ allInstances =
           , False
           ),
           ( forAllTypes $ \t ->
-              validDatasetElementType t .~~~> 
+              validDatasetElementType t .~~~>
                 validDatasetElementType (tList t)
           , implLam "t" type0 $ \t ->
               instLam "r1" (validDatasetElementType t) $ \_ ->
@@ -113,7 +113,7 @@ allInstances =
           ),
           ( forAllTypes $ \t ->
               forAllIrrelevantNat "n" $ \n ->
-                validDatasetElementType t .~~~> 
+                validDatasetElementType t .~~~>
                   validDatasetElementType (tVector t n)
           , implLam "t" type0 $ \t ->
               irrelImplNatLam "n" $ \_n ->
@@ -143,8 +143,8 @@ allInstances =
           -- ValidNetworkType --
           ----------------------
           ( forAllTypePairs $ \t1 t2 ->
-              validNetworkTensorType t1 .~~~> 
-                validNetworkTensorType t2 .~~~> 
+              validNetworkTensorType t1 .~~~>
+                validNetworkTensorType t2 .~~~>
                   validNetworkType (t1 ~> t2)
           , implTypeDoubleLam $ \t1 t2 ->
               instLam "r1" (validNetworkTensorType t1) $ \_ ->
@@ -156,17 +156,17 @@ allInstances =
               forAllIrrelevantNat "n1" $ \n1 ->
                 forAllIrrelevantNat "n2" $ \n2 ->
                   validNetworkTensorType (tVector t n1) .~~~>
-                    validNetworkTensorType (tVector (tVector t n1) n2) 
-          , implLam "t" type0 $ \t -> 
-              irrelImplNatLam "n1" $ \n1 -> 
-                irrelImplNatLam "n2" $ \_n2 -> 
+                    validNetworkTensorType (tVector (tVector t n1) n2)
+          , implLam "t" type0 $ \t ->
+              irrelImplNatLam "n1" $ \n1 ->
+                irrelImplNatLam "n2" $ \_n2 ->
                   instLam "r1" (validNetworkTensorType (tVector t n1)) $ \_ ->
                     tUnit
           , False
           ),
           ( forAllIrrelevantNat "n" $ \n ->
-              validNetworkTensorType (tVector tRat n) 
-          , irrelImplNatLam "n" $ \_n -> 
+              validNetworkTensorType (tVector tRat n)
+          , irrelImplNatLam "n" $ \_n ->
               tUnit
           , False
           ),

vehicle/src/Vehicle/Compile/Type/Constraint/InstanceSolver.hs

@@ -77,7 +77,7 @@ solveInstanceGoal constraint rawBuiltinCandidates goal = do
       <> line
 
   -- Try all candidates
-  (unsuccessfulCandidates, successfulCandidates) <- 
+  (unsuccessfulCandidates, successfulCandidates) <-
     partitionEithers <$> traverse (checkCandidate constraint goal) allCandidates
 
   case successfulCandidates of
@@ -251,8 +251,8 @@ replaceProvenance p = go
       Pi _ binder res -> Pi p (fmap go binder) (go res)
       Let _ e1 binder e2 -> Let p (go e1) (fmap go binder) (go e2)
       Lam _ binder e -> Lam p (fmap go binder) (go e)
-  
+
 extractCandidateError :: CompileError -> UnAnnDoc
 extractCandidateError err = case details err of
   UError e -> problem e
-  _ -> developerError "Unexpected error type when extracting error for instances"
+  _ -> developerError "Unexpected error type when extracting error for instances"

vehicle/src/Vehicle/Compile/Type/Core.hs

@@ -142,7 +142,7 @@ data InstanceTypeRestrictionOrigin builtin = TypeRestrictionOrigin
   , restrictedDeclType :: Type builtin
   } deriving (Show)
 
-data InstanceConstraintOrigin builtin 
+data InstanceConstraintOrigin builtin
   = InstanceArgOrigin (InstanceArgOrigin builtin)
   | InstanceTypeRestrictionOrigin (InstanceTypeRestrictionOrigin builtin)
   deriving (Show)
@@ -299,4 +299,4 @@ instance Pretty RestrictedDecl where
     RestrictedParameter s -> pretty (ParameterDef s)
     RestrictedProperty {} -> "@property"
     RestrictedNetwork {} -> pretty NetworkDef
-    RestrictedDataset {} -> pretty DatasetDef
+    RestrictedDataset {} -> pretty DatasetDef

vehicle/src/Vehicle/Compile/Type/Monad.hs

@@ -150,7 +150,7 @@ createFreshApplicationConstraint ctx problem blockingMetas = do
   let blockedConstraint = WithContext constraint (blockCtxOn blockingMetas context)
   addApplicationConstraint blockedConstraint
   return (unnormalised finalExpr, unnormalised finalType)
-  
+
 -- | Adds an entirely new type-class constraint (as opposed to one
 -- derived from another constraint).
 createFreshInstanceConstraint ::

vehicle/src/Vehicle/Compile/Type/Subsystem/InputOutputInsertion.hs

@@ -60,7 +60,7 @@ decomposePiType mkConstraint declProv@(ident, _) inputNumber = \case
 addFunctionConstraint ::
   (MonadTypeChecker builtin m, MonadState (MetaMap (Expr builtin)) m, BuiltinHasStandardData builtin) =>
   builtin ->
-  DeclProvenance -> 
+  DeclProvenance ->
   FunctionPosition ->
   Expr builtin ->
   m (Expr builtin)
@@ -84,7 +84,7 @@ addFunctionConstraint constraint declProv@(_, declP) position existingExpr = do
 
   freeEnv <- getFreeEnv
   let declSort = developerError "function IO constraints should never fail"
-  let origin = InstanceTypeRestrictionOrigin $ TypeRestrictionOrigin freeEnv declProv declSort existingExpr 
+  let origin = InstanceTypeRestrictionOrigin $ TypeRestrictionOrigin freeEnv declProv declSort existingExpr
   _ <- createFreshInstanceConstraint mempty declP origin Irrelevant tcExpr
 
   return newExpr

vehicle/src/Vehicle/Compile/Type/System.hs

@@ -247,4 +247,4 @@ assertUnquantifiedPolarity ::
   m (Type PolarityBuiltin)
 assertUnquantifiedPolarity (_, p) t = do
   createFreshUnificationConstraint p mempty CheckingAuxiliary (PolarityExpr p Unquantified) t
-  return t
+  return t