Support GHC 9.8.1 (#759)

* Bump GHC & Cabal versions * Fix freeze symlink * Remove freeze file * Add freeze file * Update tested-with * Support GHC 9.8.1 * Remove use of 'head' * Disable warning x-partial * Remove -Wno-x-partial * Removed all uses of partial functions * Fix unit test --------- Co-authored-by: MatthewDaggitt <[email protected]>
vehicle-lang · Jan 30, 2024 · cdfa922 · cdfa922
1 parent 3cc2806
commit cdfa922
Show file tree

Hide file tree

Showing 17 changed files with 232 additions and 46 deletions.
diff --git a/.github/workflows/build-vehicle.yml b/.github/workflows/build-vehicle.yml
@@ -26,6 +26,17 @@ jobs:
               project-file: "cabal.project.ghc-9.4.8"
               extra-args: ""
         include:
+          # Build with GHC 9.8.1
+          - os:
+              name: Linux
+              type: ubuntu-latest
+            haskell:
+              ghc:
+                version: "9.8.1"
+              cabal:
+                version: "3.10.2.1"
+                project-file: "cabal.project.ghc-9.8.1"
+                extra-args: ""
           # Build with GHC 9.6.4
           - os:
               name: Linux

diff --git a/cabal.project.ghc-9.2.8 b/cabal.project.ghc-9.2.8
@@ -1,4 +1,4 @@
--- Cabal project configuration file for GHC 9.2.7
+-- Cabal project configuration file for GHC 9.2.8
 --
 -- See `cabal.project` for details.
 

diff --git a/cabal.project.ghc-9.4.8 b/cabal.project.ghc-9.4.8
@@ -1,4 +1,5 @@
--- Cabal project configuration file for GHC 9.4.4
+
+-- Cabal project configuration file for GHC 9.4.8
 --
 -- See `cabal.project` for details.
 

diff --git a/cabal.project.ghc-9.6.4 b/cabal.project.ghc-9.6.4
@@ -1,4 +1,4 @@
--- Cabal project configuration file for GHC 9.6.1
+-- Cabal project configuration file for GHC 9.6.4
 --
 -- See `cabal.project` for details.
 

diff --git a/cabal.project.ghc-9.8.1 b/cabal.project.ghc-9.8.1
@@ -0,0 +1,5 @@
+-- Cabal project configuration file for GHC 9.8.1
+--
+-- See `cabal.project` for details.
+
+import: cabal.project
diff --git a/cabal.project.ghc-9.8.1.freeze b/cabal.project.ghc-9.8.1.freeze
@@ -0,0 +1,142 @@
+active-repositories: hackage.haskell.org:merge
+constraints: any.BNFC ==2.9.5,
+             any.Cabal ==3.10.2.1,
+             any.Cabal-syntax ==3.10.2.0,
+             any.Diff ==0.4.1,
+             any.Glob ==0.10.2,
+             any.OneTuple ==0.4.1.1,
+             any.QuickCheck ==2.14.3,
+             QuickCheck -old-random +templatehaskell,
+             any.StateVar ==1.2.2,
+             any.aeson ==2.2.1.0,
+             aeson +ordered-keymap,
+             any.aeson-pretty ==0.8.10,
+             aeson-pretty -lib-only,
+             any.alex ==3.5.0.0,
+             any.ansi-terminal ==0.11.5,
+             ansi-terminal -example +win32-2-13-1,
+             any.ansi-terminal-types ==0.11.5,
+             any.array ==0.5.6.0,
+             any.assoc ==1.1,
+             assoc +tagged,
+             any.attoparsec ==0.14.4,
+             attoparsec -developer,
+             any.attoparsec-aeson ==2.2.0.1,
+             any.base ==4.19.0.0,
+             any.base-compat ==0.13.1,
+             any.base-orphans ==0.9.1,
+             any.bifunctors ==5.6.1,
+             bifunctors +tagged,
+             any.binary ==0.8.9.1,
+             any.bytestring ==0.11.5.3,
+             any.call-stack ==0.4.0,
+             any.cereal ==0.5.8.3,
+             cereal -bytestring-builder,
+             any.cereal-text ==0.1.0.2,
+             any.cmdargs ==0.10.22,
+             cmdargs +quotation -testprog,
+             any.colour ==2.3.6,
+             any.comonad ==5.0.8,
+             comonad +containers +distributive +indexed-traversable,
+             any.containers ==0.6.8,
+             any.contravariant ==1.5.5,
+             contravariant +semigroups +statevar +tagged,
+             any.data-default ==0.7.1.1,
+             any.data-default-class ==0.1.2.0,
+             any.data-default-instances-containers ==0.0.1,
+             any.data-default-instances-dlist ==0.0.1,
+             any.data-default-instances-old-locale ==0.0.1,
+             any.data-fix ==0.3.2,
+             any.deepseq ==1.5.0.0,
+             any.directory ==1.3.8.1,
+             any.distributive ==0.6.2.1,
+             distributive +semigroups +tagged,
+             any.dlist ==1.0,
+             dlist -werror,
+             any.exceptions ==0.10.7,
+             any.file-embed ==0.0.15.0,
+             any.filepath ==1.4.200.1,
+             filepath -cpphs,
+             any.generically ==0.1.1,
+             any.ghc-bignum ==1.3,
+             any.ghc-boot-th ==9.8.1,
+             any.ghc-prim ==0.11.0,
+             any.gitrev ==1.3.1,
+             any.happy ==1.20.1.1,
+             any.hashable ==1.4.3.0,
+             hashable +integer-gmp -random-initial-seed,
+             any.hsc2hs ==0.68.10,
+             hsc2hs -in-ghc-tree,
+             any.indexed-traversable ==0.1.3,
+             any.indexed-traversable-instances ==0.1.1.2,
+             any.integer-conversion ==0.1.0.1,
+             any.integer-logarithms ==1.0.3.1,
+             integer-logarithms -check-bounds +integer-gmp,
+             any.linkedhashmap ==0.4.0.0,
+             any.mnist-idx ==0.1.3.2,
+             any.mtl ==2.3.1,
+             any.network-uri ==2.6.4.2,
+             any.old-locale ==1.0.0.7,
+             any.optparse-applicative ==0.18.1.0,
+             optparse-applicative +process,
+             any.parsec ==3.1.17.0,
+             any.pretty ==1.1.3.6,
+             any.prettyprinter ==1.7.1,
+             prettyprinter -buildreadme +text,
+             any.prettyprinter-ansi-terminal ==1.1.3,
+             any.primitive ==0.9.0.0,
+             any.process ==1.6.18.0,
+             any.random ==1.2.1.1,
+             any.regex-base ==0.94.0.2,
+             any.regex-tdfa ==1.3.2.2,
+             regex-tdfa +doctest -force-o2,
+             any.rts ==1.0.2,
+             any.scientific ==0.3.7.0,
+             scientific -bytestring-builder -integer-simple,
+             any.semialign ==1.3,
+             semialign +semigroupoids,
+             any.semigroupoids ==6.0.0.1,
+             semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers,
+             any.split ==0.2.5,
+             any.splitmix ==0.1.0.5,
+             splitmix -optimised-mixer,
+             any.sscript ==0.1.0.2,
+             any.stm ==2.5.2.1,
+             any.strict ==0.5,
+             any.string-qq ==0.0.5,
+             any.system-cxx-std-lib ==1.0,
+             any.tagged ==0.8.8,
+             tagged +deepseq +transformers,
+             any.tasty ==1.4.3,
+             tasty +unix,
+             any.tasty-hunit ==0.10.1,
+             any.template-haskell ==2.21.0.0,
+             any.temporary ==1.3,
+             any.terminal-progress-bar ==0.4.2,
+             any.terminal-size ==0.3.4,
+             any.text ==2.1,
+             text -developer +simdutf,
+             any.text-iso8601 ==0.1,
+             any.text-short ==0.1.5,
+             text-short -asserts,
+             any.th-abstraction ==0.6.0.0,
+             any.th-compat ==0.1.4,
+             any.these ==1.2,
+             any.time ==1.12.2,
+             any.time-compat ==1.9.6.1,
+             time-compat -old-locale,
+             any.transformers ==0.6.1.0,
+             any.transformers-compat ==0.7.2,
+             transformers-compat -five +five-three -four +generic-deriving +mtl -three -two,
+             any.unix ==2.8.5.0,
+             unix -os-string,
+             any.unordered-containers ==0.2.20,
+             unordered-containers -debug,
+             any.uuid-types ==1.0.5.1,
+             any.vector ==0.13.1.0,
+             vector +boundschecks -internalchecks -unsafechecks -wall,
+             any.vector-stream ==0.1.0.1,
+             vehicle -ghc-debug -nothunks -optimise-heavily -release-build,
+             vehicle-syntax -ghc-debug -nothunks -optimise-heavily,
+             any.witherable ==0.4.2
+index-state: hackage.haskell.org 2024-01-12T12:48:28Z
diff --git a/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs b/tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs
@@ -8,7 +8,7 @@
 
 module Test.Tasty.Golden.Executable.Runner where
 
-import Control.Exception (assert, throw)
+import Control.Exception (throw)
 import Control.Monad (unless, when)
 import Control.Monad.Catch (MonadCatch (..), MonadMask, MonadThrow, handle)
 import Control.Monad.IO.Class (MonadIO)
@@ -345,7 +345,7 @@ acceptTestProduced testProduces (IgnoreFiles testIgnores) = do
   let testSpecsList = toList testSpecs
   let thisTestIndices = List.findIndices ((== testName) . testSpecName) testSpecsList
   -- There should be EXACTLY ONE test named testSpecName:
-  thisTestIndex <- assert (length thisTestIndices == 1) (return $ head thisTestIndices)
+  thisTestIndex <- maybe (error $ "No unique test named '" <> testName <> "'") (return . fst) (List.uncons thisTestIndices)
   let (otherTestSpecsBefore, thisTestSpecAndOtherTestSpecsAfter) = List.splitAt thisTestIndex testSpecsList
   let (thisTestSpec, otherTestSpecsAfter) =
         fromMaybe (error $ printf "Could not find test named '%s'" testName) $

diff --git a/tasty-golden-executable/tasty-golden-executable.cabal b/tasty-golden-executable/tasty-golden-executable.cabal
@@ -50,7 +50,7 @@ library
     Test.Tasty.Golden.Executable.TestSpecs
 
   build-depends:
-    , aeson                 >=2.1.1   && <2.2
+    , aeson                 >=2.1.1   && <2.3
     , aeson-pretty          >=0.8.9   && <0.9
     , array                 >=0.5.4   && <0.6
     , base                  >=4.13    && <5

diff --git a/vehicle-syntax/vehicle-syntax.cabal b/vehicle-syntax/vehicle-syntax.cabal
@@ -152,18 +152,18 @@ library
     Vehicle.Syntax.Internal.Print
 
   build-depends:
-    , aeson          ^>=2.1.1
-    , array          >=0.5    && <1
-    , base           >=4      && <5
-    , cereal         >=0.5    && <1
-    , cereal-text    >=0.1    && <1
-    , containers     >=0.5    && <1
-    , deepseq        >=1.4    && <2
-    , hashable       >=1.3    && <2
-    , mtl            >=2.2    && <3
-    , prettyprinter  >=1.7    && <2
-    , text           >=1.2    && <3
-    , these          >=1.0    && <2
+    , aeson          >=2.1.1 && <2.3
+    , array          >=0.5   && <1
+    , base           >=4     && <5
+    , cereal         >=0.5   && <1
+    , cereal-text    >=0.1   && <1
+    , containers     >=0.5   && <1
+    , deepseq        >=1.4   && <2
+    , hashable       >=1.3   && <2
+    , mtl            >=2.2   && <3
+    , prettyprinter  >=1.7   && <2
+    , text           >=1.2   && <3
+    , these          >=1.0   && <2
 
   build-tool-depends:
     , alex:alex    >=3.2

diff --git a/vehicle/src/Vehicle/Backend/LossFunction/Compile.hs b/vehicle/src/Vehicle/Backend/LossFunction/Compile.hs
@@ -69,7 +69,9 @@ preprocessLogicalOperators logic = traverse (traverseBuiltinsM builtinUpdateFunc
     builtinUpdateFunction p1 p2 b args = do
       maybeUpdatedExpr <- case b of
         S.BuiltinFunction S.Not -> case compileNot logic of
-          TryToEliminate -> Just <$> lowerNot p2 (argExpr $ head args)
+          TryToEliminate -> case args of
+            [arg] -> Just <$> lowerNot p2 (argExpr arg)
+            _ -> compilerDeveloperError "Found partially applied Not"
           UnaryNot {} -> return Nothing
         _ -> return Nothing
 

diff --git a/vehicle/src/Vehicle/Backend/Queries/Error.hs b/vehicle/src/Vehicle/Backend/Queries/Error.hs
@@ -28,11 +28,10 @@ diagnoseNonLinearity queryFormat prog propertyProv@(propertyIdentifier, _) = do
       <+> quotePretty propertyIdentifier
       <> line
 
-  Main typedDecls <- typeCheckWithSubsystem mempty handleUnexpectedError prog
+  subTypedProg <- typeCheckWithSubsystem mempty handleUnexpectedError prog
 
   -- Extract and diagnose the type.
-  let property = head $ filter (\decl -> identifierOf decl == propertyIdentifier) typedDecls
-  let propertyType = typeOf property
+  propertyType <- findDeclType propertyIdentifier subTypedProg
   case propertyType of
     LinearityExpr _ (NonLinear source) -> do
       throwError $ UnsupportedNonLinearConstraint queryFormat propertyProv (Right source)
@@ -56,11 +55,10 @@ diagnoseAlternatingQuantifiers queryFormat prog propertyProv@(propertyIdentifier
       <+> quotePretty propertyIdentifier
       <> line
 
-  Main typedDecls <- typeCheckWithSubsystem mempty handleUnexpectedError prog
+  subTypedProg <- typeCheckWithSubsystem mempty handleUnexpectedError prog
 
   -- Extract and diagnose the type.
-  let property = head $ filter (\decl -> identifierOf decl == propertyIdentifier) typedDecls
-  let propertyType = typeOf property
+  propertyType <- findDeclType propertyIdentifier subTypedProg
   case propertyType of
     PolarityExpr _ (MixedSequential q p pp2) -> do
       throwError $ UnsupportedAlternatingQuantifiers queryFormat propertyProv (Right (q, p, pp2))
@@ -69,3 +67,10 @@ diagnoseAlternatingQuantifiers queryFormat prog propertyProv@(propertyIdentifier
     handleUnexpectedError :: (MonadCompile m) => CompileError -> m a
     handleUnexpectedError err =
       throwError $ UnsupportedAlternatingQuantifiers queryFormat propertyProv (Left err)
+
+findDeclType :: (MonadCompile m) => Identifier -> Prog Ix builtin -> m (Expr Ix builtin)
+findDeclType ident (Main decls) = do
+  let candidates = filter (\decl -> identifierOf decl == ident) decls
+  case candidates of
+    [property] -> return $ typeOf property
+    _ -> compilerDeveloperError $ "Could not find property" <+> quotePretty ident <+> "in program after subtyping."
diff --git a/vehicle/src/Vehicle/Compile/Error/Message.hs b/vehicle/src/Vehicle/Compile/Error/Message.hs
@@ -204,9 +204,9 @@ instance MeaningfulError CompileError where
                   <+> quotePretty annotationName
                   <+> "annotation.",
               fix =
-                if null suggestions
-                  then Nothing
-                  else Just $ "did you mean" <+> quotePretty (head suggestions) <> "?"
+                case suggestions of
+                  [] -> Nothing
+                  (s : _) -> Just $ "did you mean" <+> quotePretty s <> "?"
             }
       InvalidAnnotationOptionValue p parameterName parameterValue ->
         UError $
@@ -421,7 +421,9 @@ instance MeaningfulError CompileError where
                 <> line
                 <> indent 2 deducedType
                 <> line
-                <> "but" <+> originExpr <+> "has only the following valid types:"
+                <> "but"
+                  <+> originExpr
+                  <+> "has only the following valid types:"
                 <> line
                 <> indent 2 (vsep (fmap calculateCandidateType candidates)),
             fix = Nothing
@@ -1245,13 +1247,15 @@ supportedNetworkTypeDescription =
 errorInSubsystemMessage :: Doc a -> CompileError -> Doc a
 errorInSubsystemMessage task err =
   line
-    <> "Unfortunately while trying to" <+> task
+    <> "Unfortunately while trying to"
+      <+> task
     <> ","
       <+> "the following error was encountered:"
     <> line
     <> indent 2 (pretty (details err))
     <> line
-    <> "Please report this as an issue on Github" <+> parens githubIssues
+    <> "Please report this as an issue on Github"
+      <+> parens githubIssues
     <> line
 
 githubIssues :: Doc a

diff --git a/vehicle/src/Vehicle/Compile/Simplify.hs b/vehicle/src/Vehicle/Compile/Simplify.hs
@@ -48,18 +48,29 @@ instance Simplify (Expr Name Builtin) where
 
   shortenVec = mapBuiltins $ \p1 p2 b args ->
     case b of
-      BuiltinConstructor (LVec n)
-        | length args > 5 ->
-            normAppList
-              p1
-              (Builtin p2 (BuiltinConstructor (LVec n)))
-              [ head args,
-                Arg p2 Explicit Relevant (FreeVar p2 (Identifier StdLib ("<" <> n2 <> " more>"))),
-                last args
-              ]
-        where
-          n2 = Text.pack $ show $ length args - 2
+      BuiltinConstructor (LVec n) -> case getHeadMidTail args of
+        Just (firstArg, numberOfMiddleAgs, lastArg)
+          | numberOfMiddleAgs > 3 ->
+              normAppList
+                p1
+                (Builtin p2 (BuiltinConstructor (LVec n)))
+                [ firstArg,
+                  Arg p2 Explicit Relevant (FreeVar p2 (Identifier StdLib ("<" <> n2 <> " more>"))),
+                  lastArg
+                ]
+          where
+            n2 = Text.pack $ show $ length args - 2
+        _ -> normAppList p1 (Builtin p2 b) args
       _ -> normAppList p1 (Builtin p2 b) args
+    where
+      getHeadMidTail :: forall a. [a] -> Maybe (a, Int, a)
+      getHeadMidTail [] = Nothing
+      getHeadMidTail (x : xs) = go 0 xs
+        where
+          go :: Int -> [a] -> Maybe (a, Int, a)
+          go _ [] = Nothing
+          go l [e] = Just (x, l, e)
+          go l (_ : ys) = go (l + 1) ys
 
 instance Simplify (Binder Name Builtin) where
   uninsert = fmap uninsert

diff --git a/vehicle/src/Vehicle/Data/LinearExpr.hs b/vehicle/src/Vehicle/Data/LinearExpr.hs
@@ -83,7 +83,8 @@ foldTensor :: forall a. (Rational -> a) -> ([a] -> a) -> RationalTensor -> a
 foldTensor mkValue mkVec (RationalTensor dims value) = go dims (Vector.toList value)
   where
     go :: TensorDimensions -> [Rational] -> a
-    go [] xs = mkValue (head xs)
+    go [] [x] = mkValue x
+    go [] _xs = developerError "Mis-sized tensor. Expected a single element."
     go (_d : ds) xs = do
       let inputVarIndicesChunks = chunksOf (product ds) xs
       let elems = fmap (go ds) inputVarIndicesChunks

diff --git a/vehicle/src/Vehicle/Verify/Specification/Status.hs b/vehicle/src/Vehicle/Verify/Specification/Status.hs
@@ -92,7 +92,8 @@ prettyUserVariableAssignment (OriginalUserVariable {..}, variableValue) =
   pretty userTensorVarName <> ":" <+> pretty variableValue
 
 assignmentToExpr :: TensorDimensions -> [Rational] -> Expr Ix Builtin
-assignmentToExpr [] xs = RatLiteral mempty (toRational (head xs))
+assignmentToExpr [] [x] = RatLiteral mempty (toRational x)
+assignmentToExpr [] _ = developerError "Malformed tensor"
 assignmentToExpr (dim : dims) xs = do
   let vecConstructor = Builtin mempty (BuiltinConstructor $ LVec dim)
   let inputVarIndicesChunks = chunksOf (product dims) xs