Use GHC-9-12 and Stackage Nightly

frontend/src/Language/Granule/Checker/Checker.hs

@@ -15,6 +15,7 @@
 module Language.Granule.Checker.Checker where
 
 import Control.Arrow (second)
+import Control.Monad
 import Control.Monad.State.Strict
 import Control.Monad.Except (throwError)
 import Data.List.NonEmpty (NonEmpty(..))

frontend/src/Language/Granule/Checker/Kinding.hs

@@ -493,7 +493,7 @@ synthKindWithConfiguration s config (TyCase t branches) | not (null branches) =
           Nothing ->
             throw KindMismatch { errLoc = s, tyActualK = Just branchTy, kExpected = kJoined, kActual = k })
       (snd $ head branchesAndKinds, substIntermediate)
-      (tail branchesAndKinds)
+      (drop 1 branchesAndKinds)
   --
   return (kind, substFinal, TyCase t' branches')
 

frontend/src/Language/Granule/Checker/Monad.hs

@@ -361,7 +361,7 @@ newCaseFrame =
 -- | This happens when we finish a case expression
 popCaseFrame :: Checker ()
 popCaseFrame =
-  modify (\st -> st { guardPredicates = tail (guardPredicates st) })
+  modify (\st -> st { guardPredicates = drop 1 (guardPredicates st) })
 
 -- | Takes the top two conjunction frames and turns them into an
 -- implication

frontend/src/Language/Granule/Checker/Patterns.hs

@@ -8,6 +8,7 @@
 -- | Type checking patterns
 module Language.Granule.Checker.Patterns where
 
+import Control.Monad
 import Control.Monad.Except (throwError)
 import Control.Monad.State.Strict
 import Data.List.NonEmpty (NonEmpty(..))

frontend/src/Language/Granule/Checker/Predicates.hs

@@ -135,7 +135,9 @@ prettyNegPred :: (?globals :: Globals) => Id -> Pred -> String
 prettyNegPred defId (Con c) =
     "  When checking `" <> pretty defId <> "`, " <> message
   where
-    message = toLower (head msg) : tail msg
+    makeLower [] = []
+    makeLower (head:tail) = toLower head : tail
+    message = makeLower msg
     msg = pretty (Neg c)
 -- Long-winded message
 prettyNegPred defId p =

frontend/src/Language/Granule/Checker/Types.hs

@@ -8,6 +8,7 @@
 -- | Type equality (and inequalities when grades are involved)
 module Language.Granule.Checker.Types where
 
+import Control.Monad
 import Control.Monad.State.Strict
 import Data.List (sortBy, sort)
 import Data.Functor ((<&>))

frontend/src/Language/Granule/Syntax/Def.hs

@@ -171,7 +171,7 @@ data DataConstr
     { dataConstrSpan :: Span, dataConstrId :: Id, dataConstrTypeScheme :: TypeScheme } -- ^ GADTs
   | DataConstrNonIndexed
     { dataConstrSpan :: Span, dataConstrId :: Id, dataConstrParams :: [Type] } -- ^ ADTs
-  deriving (Eq, Show, Generic, Typeable, Data)
+  deriving (Eq, Show, Generic, Data)
 
 -- | Is the data type an indexed data type, or just a plain ADT?
 isIndexedDataType :: DataDecl -> Bool

frontend/src/Language/Granule/Syntax/Expr.hs

@@ -67,7 +67,7 @@ data ValueF ev a value expr =
      -- /\(x : k) . t
     -- Extensible part
     | ExtF a ev
-   deriving (Generic, Eq, Rp.Data)
+   deriving (Generic, Eq, Rp.Data, Functor)
 
 deriving instance (Show ev, Show a, Show value, Show expr)
     => Show (ValueF ev a value expr)
@@ -153,7 +153,7 @@ data ExprF ev a expr value =
   | UnpackF Span a Bool Id Id expr expr
      -- unpack <a, x> = e1 in e2
   | HoleF Span a Bool [Id] (Maybe Hints)
-  deriving (Generic, Eq, Rp.Data)
+  deriving (Generic, Eq, Rp.Data, Functor)
 
 data Operator
   = OpLesser

frontend/src/Language/Granule/Syntax/Pattern.hs

@@ -29,7 +29,7 @@ data Pattern a
   | PChar Span a Bool Char
   | PFloat Span a Bool Double          -- ^ Float pattern
   | PConstr Span a Bool Id [Id] [Pattern a] -- ^ Constructor pattern
-  deriving (Eq, Show, Generic, Functor, Typeable, Data)
+  deriving (Eq, Show, Generic, Functor, Data)
 
 instance Term (Pattern a) where
   freeVars _ = []

frontend/src/Language/Granule/Syntax/Type.hs

@@ -41,7 +41,7 @@ type Kind     = Type
 
 -- Represents polairty information for lattices
 data Polarity = Normal | Opposite
- deriving (Eq, Show, Ord, Data, Typeable)
+ deriving (Eq, Show, Ord, Data)
 
 -- | Type syntax (includes effect, coeffect, and predicate terms)
 data Type where
@@ -73,7 +73,6 @@ deriving instance Show Type
 deriving instance Eq Type
 deriving instance Ord Type
 deriving instance Data Type
-deriving instance Typeable Type
 
 -- Constructors and operators are just strings
 data TypeOperator

frontend/src/Language/Granule/Synthesis/Monad.hs

@@ -12,6 +12,7 @@ import qualified Prettyprinter as P
 import qualified Data.Generics.Zipper as Z
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.List (isInfixOf)
+import Control.Monad
 import Control.Monad.Except
 import Control.Monad.State.Strict
 import Control.Monad.Logic

frontend/src/Language/Granule/Synthesis/Synth.hs

@@ -43,6 +43,7 @@ import Language.Granule.Synthesis.Common
 
 
 import Data.Either (lefts, rights, fromRight)
+import Control.Monad
 import Control.Monad.State.Strict
 
 -- import qualified Control.Monad.State.Strict as State (get)

frontend/src/Language/Granule/Synthesis/SynthLinearBase.hs

@@ -23,6 +23,7 @@ import Language.Granule.Synthesis.Contexts
 import Language.Granule.Synthesis.Common
 import Language.Granule.Utils
 
+import Control.Monad
 import Control.Monad.State.Strict
 import qualified System.Clock as Clock
 import Data.List (sortBy)

frontend/tests/cases/negative/simple/signature-equation-name-mismatch.gr.output

@@ -1,2 +1,2 @@
 Parse error: 
-Name for equation `f00` does not match the signature head `foo`
+Name for equation `f00` does not match the signature head `foo`

frontend/tests/hspec/Data/Bifunctor/FoldableSpec.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE DeriveFunctor #-}
 
 {-# options_ghc -Wno-missing-pattern-synonym-signatures #-}
 
@@ -15,6 +16,7 @@ data ExprF expr val =
     | OrF expr expr
     | NotF expr
     | ValF val
+    deriving (Functor)
 $(deriveBifunctor ''ExprF)
 
 type Expr = Fix2 ExprF ValueF
@@ -35,6 +37,7 @@ data ValueF val expr =
     LitF Bool
     | IgnoreF expr Bool -- `expr` does nothing, it's just here to
                         -- demonstrate mutual recursion.
+    deriving (Functor)
 $(deriveBifunctor ''ValueF)
 
 type Value = Fix2 ValueF ExprF

granule.cabal

@@ -37,18 +37,18 @@ common granule-default-lang
 common granule-dependencies
   build-depends:
       Glob          ==0.10.2
-    , array         ==0.5.4.0
-    , base          ==4.17.2.1
-    , bifunctors    ==5.5.15
+    , array         ==0.5.8.0
+    , base          ==4.21.2.0
+    , bifunctors    ==5.6.3
     , clock         ==0.8.4
-    , containers    ==0.6.7
-    , directory     ==1.3.7.1
-    , filepath      ==1.4.2.2
-    , mtl           ==2.2.2
-    , prettyprinter ==1.7.1
-    , text          ==2.0.2
-    , time          ==1.12.2
-    , transformers  ==0.5.6.2
+    , containers    ==0.7
+    , directory     ==1.3.10.1
+    , filepath      ==1.5.5.0
+    , mtl           ==2.3.2
+    , prettyprinter ==1.7.2
+    , text          ==2.1.4
+    , time          ==1.14
+    , transformers  ==0.6.3.0
 
 common granule-ghc-warnings
   ghc-options:
@@ -58,6 +58,7 @@ common granule-ghc-warnings
     -Wincomplete-record-updates
     -Wincomplete-uni-patterns
     -Wredundant-constraints
+    -Wno-x-partial
     -Wno-unused-matches
     -Wno-name-shadowing
     -Wno-type-defaults
@@ -343,8 +344,8 @@ executable grepl
     , filemanip           ==0.3.6.3
     , granule:frontend
     , granule:interpreter 
-    , haskeline           ==0.8.2
-    , parsec              ==3.1.16.1
+    , haskeline           ==0.8.4.1
+    , parsec              ==3.1.18.0
 
 executable grc
   import: granule-default-lang

interpreter/src/Language/Granule/Interpreter.hs

@@ -252,8 +252,7 @@ run config input = let ?globals = maybe mempty grGlobals (getEmbeddedGrFlags inp
     synthesiseHoles :: (?globals :: Globals) => GrConfig -> AST () () -> [(CheckerError, Maybe Measurement, Int)] -> Bool -> IO [(CheckerError, Maybe Measurement, Int)]
     synthesiseHoles config _ [] _ = return []
     synthesiseHoles config astSrc ((hole@(HoleMessage sp goal ctxt tyVars hVars synthCtxt@(Just (cs, defs, (Just defId, spec), index, hints, constructors)) hcases), aggregate, attemptNo):holes) isGradedBase = do
-      -- TODO: this magic number shouldn't here I don't think...
-      let timeout = if interactiveDebugging then maxBound :: Int else 10000000
+      let timeout = if interactiveDebugging then maxBound :: Int else (1000 * fromInteger solverTimeoutMillis)
       rest <- synthesiseHoles config astSrc holes isGradedBase
 
       gradedExpr <- if cartSynth > 0 then getGradedExpr config defId else return Nothing

interpreter/tests/Golden.hs

@@ -213,7 +213,9 @@ goldenTestsSynthesis config = do
         globalsSourceFilePath = Just fp,
         globalsSynthesise = Just True,
         globalsRewriteHoles = Just True,
-        globalsIncludePath = Just "StdLib" }
+        globalsIncludePath = Just "StdLib",
+        -- Slightly longer for synthesis examples which can be heavy
+        globalsSolverTimeoutMillis = Just 30000  }
 
 
     subtractiveGlobals :: FilePath -> Globals

repl/app/Language/Granule/Main.hs

@@ -17,6 +17,7 @@ import qualified Data.Map as M
 import qualified Data.List.NonEmpty as NonEmpty (NonEmpty, filter, fromList)
 import qualified Language.Granule.Checker.Monad as Checker
 import Control.Exception (try)
+import Control.Monad
 import Control.Monad.State
 import Control.Monad.Trans.Reader
 import qualified Control.Monad.Except as Ex
@@ -146,7 +147,7 @@ helpMenu = unlines
       ]
 
 handleCMD :: (?globals::Globals) => String -> REPLStateIO ()
-handleCMD "" = Ex.return ()
+handleCMD "" = return ()
 handleCMD s =
    case parseLine s of
     Right l -> handleLine l

runtime/src/Language/Granule/Runtime.hs

@@ -44,7 +44,7 @@ import Control.Monad
 import GHC.Err (undefined)
 import Data.Function (const)
 import Data.Functor ((<&>))
-import Data.Text
+import Data.Text hiding (show)
 import Data.Text.IO
 import Data.Time.Clock
 import qualified Data.IORef as MR

stack.yaml

@@ -1,11 +1,12 @@
-resolver: lts-21.25
+resolver: nightly-2026-08-11
 packages:
 - .
 
 # Dependency packages to be pulled from upstream that are not in the resolver
 extra-deps:
 - text-replace-0.1.0.3
-- sbv-9.2
+- git: https://github.com/BinderDavid/sbv
+  commit: a7c645d47de07c7c9ecfa6f13fec43884ee7d16c
 - syz-0.2.0.0
 - lsp-types-2.3.0.1
 - lsp-2.7.0.1