Enable warnings for vehicle-syntax package + resulting fixes (#836)

* Enable warnings for vehicle-syntax package + resulting fixes

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

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

* Fixed formatting warnings

* Avoid no-signature warnings

---------

Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com>

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

@@ -90,7 +90,7 @@ traverseExplicitArgExpr f arg
   | otherwise = return arg
 
 argFromBinder :: GenericBinder expr -> expr -> GenericArg expr
-argFromBinder (Binder p i v r _) = Arg p v r
+argFromBinder (Binder p _ v r _) = Arg p v r
 
 -- | Constructs an explicit relevant argument
 explicit :: expr -> GenericArg expr

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

@@ -1,9 +1,7 @@
 module Vehicle.Syntax.AST.Decl where
 
 import Control.DeepSeq (NFData)
-import Data.Map (Map)
 import Data.Serialize (Serialize)
-import Data.Text (Text)
 import GHC.Generics (Generic)
 import Prettyprinter (Pretty (..))
 import Vehicle.Syntax.AST.Expr
@@ -63,7 +61,7 @@ bodyOf = \case
 
 annotationsOf :: GenericDecl expr -> [Annotation]
 annotationsOf = \case
-  DefFunction _ _ anns _ e -> anns
+  DefFunction _ _ anns _ _ -> anns
   DefAbstract {} -> []
 
 -- | Traverses the type and body of a declaration using the first and
@@ -130,7 +128,7 @@ instance Pretty DefAbstractSort where
     "@" <> case t of
       NetworkDef -> "network"
       DatasetDef -> "dataset"
-      ParameterDef paramTyp -> "parameter"
+      ParameterDef {} -> "parameter"
       PostulateDef {} -> "postulate"
 
 isExternalResourceSort :: DefAbstractSort -> Bool

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

@@ -42,8 +42,7 @@ import Vehicle.Syntax.AST.Binder
 import Vehicle.Syntax.AST.Meta (MetaID)
 import Vehicle.Syntax.AST.Name (Identifier, Name)
 import Vehicle.Syntax.AST.Provenance (HasProvenance (..), Provenance, fillInProvenance)
-import Vehicle.Syntax.Builtin (Builtin)
-import Vehicle.Syntax.Prelude
+import Vehicle.Syntax.Prelude ()
 
 --------------------------------------------------------------------------------
 -- Universes

vehicle-syntax/src/Vehicle/Syntax/AST/Instances/NoThunks.hs

@@ -2,6 +2,7 @@
 
 module Vehicle.Syntax.AST.Instances.NoThunks where
 
+#ifdef nothunks
 import Vehicle.Syntax.AST.Arg
 import Vehicle.Syntax.AST.Binder
 import Vehicle.Syntax.AST.Decl
@@ -14,7 +15,6 @@ import Vehicle.Syntax.AST.Relevance
 import Vehicle.Syntax.AST.Visibility
 import Vehicle.Syntax.Builtin
 
-#ifdef nothunks
 import NoThunks.Class (NoThunks)
 
 -- Vehicle.Syntax.Builtin.Core

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

@@ -1,11 +1,11 @@
 module Vehicle.Syntax.AST.Name where
 
 import Control.DeepSeq (NFData)
-import Data.Aeson (FromJSON, FromJSONKey, ToJSON, ToJSONKey)
+import Data.Aeson (FromJSON, ToJSON, ToJSONKey)
 import Data.Hashable (Hashable)
 import Data.Serialize (Serialize)
 import Data.Serialize.Text ()
-import Data.Text (Text, pack)
+import Data.Text (Text)
 import GHC.Generics (Generic)
 import Prettyprinter (Pretty (..))
 
@@ -74,7 +74,7 @@ class HasName a name | a -> name where
   nameOf :: a -> name
 
 instance HasName Identifier Name where
-  nameOf (Identifier mod name) = name
+  nameOf (Identifier _mod name) = name
 
 instance HasName Name Name where
   nameOf = id

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

@@ -1,7 +1,6 @@
 module Vehicle.Syntax.AST.Prog where
 
 import Control.DeepSeq (NFData)
-import Data.Aeson (FromJSON, ToJSON)
 import Data.Serialize (Serialize)
 import GHC.Generics (Generic)
 import Vehicle.Syntax.AST.Decl (GenericDecl)
@@ -33,4 +32,4 @@ filterDecls ::
   (GenericDecl expr -> Bool) ->
   GenericProg expr ->
   GenericProg expr
-filterDecls pred (Main ds) = Main (filter pred ds)
+filterDecls f (Main ds) = Main (filter f ds)

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

@@ -13,16 +13,12 @@ module Vehicle.Syntax.AST.Provenance
 where
 
 import Control.DeepSeq (NFData (..))
-import Data.Aeson (KeyValue (..), ToJSON (..), object)
 import Data.Hashable (Hashable (..))
-import Data.List (sort)
 import Data.List.NonEmpty (NonEmpty)
 import Data.List.NonEmpty qualified as NonEmpty
-import Data.Maybe (maybeToList)
 import Data.Serialize (Serialize)
-import Data.Text (Text)
 import GHC.Generics (Generic (..))
-import Prettyprinter (Pretty (..), concatWith, squotes, (<+>))
+import Prettyprinter (Pretty (..), (<+>))
 import Vehicle.Syntax.AST.Name (Module (..))
 import Vehicle.Syntax.Parse.Token
 
@@ -68,7 +64,7 @@ data Range = Range
   deriving (Show, Eq, Generic)
 
 instance Ord Range where
-  Range s1 e1 <= Range s2 e2 = s1 < s2 || (s1 == s2 && e1 <= e1)
+  Range s1 e1 <= Range s2 e2 = s1 < s2 || (s1 == s2 && e1 <= e2)
 
 instance Semigroup Range where
   Range b1 _ <> Range _ b2 = Range b1 b2
@@ -92,7 +88,7 @@ instance Pretty Range where
 instance Serialize Range
 
 expandRange :: (Int, Int) -> Range -> Range
-expandRange (l, r) (Range start end) =
+expandRange (l, r) (Range {..}) =
   Range (alterColumn (\x -> x - l) start) (alterColumn (+ r) end)
 
 --------------------------------------------------------------------------------
@@ -120,7 +116,7 @@ instance Serialize Provenance
 
 -- | Get the provenance for a single token.
 tkProvenance :: (IsToken a) => Module -> a -> Provenance
-tkProvenance mod tk = Provenance (Range start end) mod
+tkProvenance modl tk = Provenance (Range start end) modl
   where
     start = tkPosition tk
     end = Position (posLine start) (posColumn start + tkLength tk)
@@ -133,18 +129,18 @@ fillInProvenance provenances = do
   Provenance (Range start end) (modul $ NonEmpty.head provenances)
   where
     getPositions :: Provenance -> (Position, Position)
-    getPositions (Provenance (Range start end) modul) = (start, end)
+    getPositions (Provenance (Range start end) _) = (start, end)
 
 expandProvenance :: (Int, Int) -> Provenance -> Provenance
 expandProvenance w (Provenance range o) = Provenance (expandRange w range) o
 
 instance Pretty Provenance where
-  pretty (Provenance origin mod) = case mod of
+  pretty (Provenance origin modl) = case modl of
     User -> pretty origin
-    StdLib -> pretty mod <> "," <+> pretty origin
+    StdLib -> pretty modl <> "," <+> pretty origin
 
 instance Semigroup Provenance where
-  Provenance origin1 owner1 <> Provenance origin2 owner2 =
+  Provenance origin1 owner1 <> Provenance origin2 _owner2 =
     Provenance (origin1 <> origin2) owner1
 
 noProvenance :: Provenance

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

@@ -5,7 +5,6 @@ import Data.Aeson (ToJSON)
 import Data.Hashable (Hashable)
 import Data.Serialize (Serialize)
 import GHC.Generics (Generic)
-import Vehicle.Syntax.Builtin
 
 --------------------------------------------------------------------------------
 -- Data

vehicle-syntax/src/Vehicle/Syntax/BNFC/Delaborate/External.hs

@@ -6,20 +6,16 @@ module Vehicle.Syntax.BNFC.Delaborate.External
   )
 where
 
-import Control.Monad.Identity (Identity (runIdentity), IdentityT)
-import Data.List.NonEmpty (NonEmpty)
-import Data.List.NonEmpty qualified as NonEmpty (head, toList)
-import Data.Map qualified as Map
-import Data.Maybe (fromMaybe, maybeToList)
+import Control.Monad.Identity (Identity (runIdentity))
+import Data.List.NonEmpty qualified as NonEmpty (toList)
+import Data.Maybe (fromMaybe)
 import Data.Text (Text, pack)
-import Prettyprinter (Doc, Pretty (..), squote, squotes, (<+>))
+import Prettyprinter (Pretty (..))
 import Vehicle.Syntax.AST qualified as V
 import Vehicle.Syntax.AST.Arg
 import Vehicle.Syntax.BNFC.Utils
 import Vehicle.Syntax.Builtin qualified as V
 import Vehicle.Syntax.External.Abs qualified as B
-import Vehicle.Syntax.External.Print as External (Print, printTree)
-import Vehicle.Syntax.Parse.Error
 import Vehicle.Syntax.Parse.Token
 import Vehicle.Syntax.Prelude
 import Vehicle.Syntax.Sugar
@@ -52,7 +48,6 @@ instance Delaborate (V.Decl V.Name V.Builtin) [B.Decl] where
       defAnn <- case a of
         V.PostulateDef linearityType polarityType -> do
           let nameOption = mkNameAnnOption "name" (V.nameOf n)
-          let types = t : fromMaybe [] (sequence [linearityType, polarityType])
           typeOption <- mkTypeAnnOption ("standard", t)
           linearOpt <- traverse (mkTypeAnnOption . ("linearity",)) linearityType
           polarityOpt <- traverse (mkTypeAnnOption . ("polarity",)) polarityType
@@ -117,7 +112,7 @@ delabNameBinder b = case V.binderNamingForm b of
   V.OnlyType {} ->
     developerError
       "Should not be delaborating the `OnlyType` binder to a `Binder Name`"
-  V.NameAndType name -> B.BasicNameBinder <$> delabM b
+  V.NameAndType {} -> B.BasicNameBinder <$> delabM b
   V.OnlyName name -> return $ case V.visibilityOf b of
     V.Explicit -> B.ExplicitNameBinder (delabModalities b) (delabSymbol name)
     V.Implicit {} -> B.ImplicitNameBinder (delabModalities b) (delabSymbol name)
@@ -270,32 +265,13 @@ delabOp1 op tk [arg]
   | V.isExplicit arg = op tk <$> delabM (argExpr arg)
 delabOp1 _ tk args = delabApp (cheatDelab $ tkSymbol tk) args
 
-delabOp2 :: (MonadDelab m, IsToken token) => (token -> B.Expr -> B.Expr -> B.Expr) -> token -> [V.Arg V.Name V.Builtin] -> m B.Expr
-delabOp2 op tk args@[arg1, arg2]
-  | all V.isExplicit args = op tk <$> delabM (argExpr arg1) <*> delabM (argExpr arg2)
-delabOp2 op tk args = delabApp (cheatDelab $ tkSymbol tk) args
-
-delabOp3 :: (MonadDelab m, IsToken token) => (token -> B.Expr -> B.Expr -> B.Expr -> B.Expr) -> token -> [V.Arg V.Name V.Builtin] -> m B.Expr
-delabOp3 op tk args@[arg1, arg2, arg3]
-  | all V.isExplicit args = op tk <$> delabM (argExpr arg1) <*> delabM (argExpr arg2) <*> delabM (argExpr arg3)
-delabOp3 op tk args = delabApp (cheatDelab $ tkSymbol tk) args
-
 delabInfixOp2 :: (MonadDelab m, IsToken token) => (B.Expr -> token -> B.Expr -> B.Expr) -> token -> [V.Arg V.Name V.Builtin] -> m B.Expr
 delabInfixOp2 op tk args@[arg1, arg2]
   | all V.isExplicit args = op <$> delabM (argExpr arg1) <*> pure tk <*> delabM (argExpr arg2)
-delabInfixOp2 op tk args
+delabInfixOp2 _op tk args
   | null args = delabApp (cheatDelab $ "(" <> tkSymbol tk <> ")") []
   | otherwise = delabApp (cheatDelab $ tkSymbol tk) args
 
-delabPartialSection :: Int -> [B.Expr] -> ([B.Expr] -> B.Expr) -> B.Expr
-delabPartialSection expectedArgs actualArgs mkOp = do
-  -- This is a hack until we get section syntax.
-  let missingArgNumbers = [0 .. (expectedArgs - length actualArgs)]
-  let missingVarNames = fmap (\v -> delabSymbol (pack "x" <> pack (show v))) missingArgNumbers
-  let missingVars = fmap B.Var missingVarNames
-  let missingBinders = fmap (B.ExplicitNameBinder mempty) missingVarNames
-  B.Lam tokLambda missingBinders tokArrow (mkOp (actualArgs <> missingVars))
-
 delabIf :: (MonadDelab m) => [V.Arg V.Name V.Builtin] -> m B.Expr
 delabIf args@[arg1, arg2, arg3]
   | all V.isExplicit args = do
@@ -305,18 +281,6 @@ delabIf args@[arg1, arg2, arg3]
       return $ B.If tokIf e1 tokThen e2 tokElse e3
 delabIf args = delabApp (cheatDelab "if") args
 
-argsError :: Text -> Int -> [B.Arg] -> a
-argsError s n args =
-  developerError $
-    "Expecting"
-      <+> pretty n
-      <+> "arguments for"
-      <+> squotes (pretty s)
-      <+> "but found"
-      <+> pretty (length args)
-      <+> "arguments:"
-      <+> squotes (pretty (External.printTree args))
-
 -- | Collapses pi expressions into either a function or a sequence of forall bindings
 delabPi :: (MonadDelab m) => V.Binder V.Name V.Builtin -> V.Expr V.Name V.Builtin -> m B.Expr
 delabPi binder body = case V.binderNamingForm binder of
@@ -372,28 +336,6 @@ delabQuantifier q args = case reverse args of
     return $ mkTk binders' tokDot body'
   _ -> return $ cheatDelab (layoutAsText $ pretty q)
 
-delabQuantifierIn :: (MonadDelab m) => V.Quantifier -> [V.Arg V.Name V.Builtin] -> m B.Expr
-delabQuantifierIn q args = case reverse args of
-  V.RelevantExplicitArg _ cont : V.RelevantExplicitArg _ (V.Lam _ binder body) : _ -> do
-    binder' <- delabNameBinder binder
-    cont' <- delabM cont
-    body' <- delabM body
-    let mkTk = case q of
-          V.Forall -> B.ForallIn tokForall
-          V.Exists -> B.ExistsIn tokExists
-    return $ mkTk binder' cont' tokDot body'
-  _ -> do
-    let sym = case q of V.Forall -> tkSymbol tokForall; V.Exists -> tkSymbol tokExists
-    argsError sym 2 <$> traverse delabM args
-
-delabForeach :: (MonadDelab m) => [V.Arg V.Name V.Builtin] -> m B.Expr
-delabForeach args = case reverse args of
-  V.RelevantExplicitArg _ (V.Lam _ binder body) : _ -> do
-    binder' <- delabNameBinder binder
-    body' <- delabM body
-    return $ B.Foreach tokForeach binder' tokDot body'
-  _ -> argsError (tkSymbol tokForeach) 1 <$> traverse delabM args
-
 delabAnn :: B.TokAnnotation -> [B.DeclAnnOption] -> B.Decl
 delabAnn name [] = B.DefAnn name B.DeclAnnWithoutOpts
 delabAnn name ops = B.DefAnn name $ B.DeclAnnWithOpts ops
@@ -406,16 +348,3 @@ mkNameAnnOption name value = B.NameAnnOption (mkToken B.TokAnnNameOpt name) (mkT
 
 mkTypeAnnOption :: (MonadDelab m) => (Text, V.Expr V.Name V.Builtin) -> m B.DeclAnnOption
 mkTypeAnnOption (name, value) = B.TypeAnnOption (mkToken B.Name name) <$> delabM value
-
-auxiliaryTypeError :: Doc a -> a
-auxiliaryTypeError e =
-  developerError $
-    "Encountered" <+> squotes e <> ". Should not be delaborating auxiliary-type system code."
-
-primOpError :: V.Builtin -> a
-primOpError e =
-  developerError $
-    "Encountered" <+> squotes (pretty e) <> ". Delaborating primitive builtins not yet supported."
-
-onlyExplicit :: NonEmpty (GenericArg expr) -> [expr]
-onlyExplicit args = argExpr <$> filter V.isExplicit (NonEmpty.toList args)

vehicle-syntax/src/Vehicle/Syntax/BNFC/Delaborate/Internal.hs

@@ -15,7 +15,6 @@ import Prettyprinter (Pretty (..))
 import Vehicle.Syntax.AST qualified as V
 import Vehicle.Syntax.Builtin qualified as V
 import Vehicle.Syntax.Internal.Abs qualified as B
-import Vehicle.Syntax.Parse.Error
 import Vehicle.Syntax.Parse.Token
 import Vehicle.Syntax.Prelude (layoutAsText)
 
@@ -53,7 +52,7 @@ instance Delaborate V.DefAbstractSort (B.NameToken -> B.Expr -> B.Decl) where
     V.PostulateDef {} -> B.DeclPost
     V.NetworkDef -> B.DeclNetw
     V.DatasetDef -> B.DeclData
-    V.ParameterDef sort -> case sort of
+    V.ParameterDef paramSort -> case paramSort of
       V.NonInferable -> B.DeclParam
       V.Inferable -> B.DeclImplParam
 
@@ -95,18 +94,6 @@ instance Delaborate (V.Binder V.Name V.Builtin) B.Binder where
 delabUniverse :: V.UniverseLevel -> B.Expr
 delabUniverse = \case
   V.UniverseLevel l -> B.Type (mkToken B.TypeToken ("Type" <> pack (show l)))
-  where
-    mkBuiltinToken :: (Pretty a) => a -> B.BuiltinToken
-    mkBuiltinToken a = mkToken B.BuiltinToken $ layoutAsText (pretty a)
-
-delabBoolLit :: Bool -> B.Expr
-delabBoolLit b = B.Literal $ B.BoolLiteral (mkToken B.BoolToken (if b then "True" else "False"))
-
-delabNatLit :: Int -> B.Expr
-delabNatLit n = B.Literal $ B.NatLiteral (mkToken B.Natural (pack $ show n))
-
-delabRatLit :: Rational -> B.Expr
-delabRatLit r = B.Literal $ B.RatLiteral (mkToken B.Rational (pack $ show (fromRational r :: Double)))
 
 delabSymbol :: Text -> B.NameToken
 delabSymbol = mkToken B.NameToken