From 757972c46c0bc94f013d88f1e9632dc0bcef9e3b Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 11 Aug 2026 17:07:21 +0100 Subject: [PATCH 1/6] Use GHC-9-12 and Stackage Nightly --- .../src/Language/Granule/Checker/Checker.hs | 1 + .../src/Language/Granule/Checker/Kinding.hs | 2 +- .../src/Language/Granule/Checker/Monad.hs | 2 +- .../src/Language/Granule/Checker/Patterns.hs | 1 + .../Language/Granule/Checker/Predicates.hs | 4 ++- .../src/Language/Granule/Checker/Types.hs | 1 + frontend/src/Language/Granule/Syntax/Def.hs | 2 +- frontend/src/Language/Granule/Syntax/Expr.hs | 4 +-- .../src/Language/Granule/Syntax/Pattern.hs | 2 +- frontend/src/Language/Granule/Syntax/Type.hs | 3 +-- .../src/Language/Granule/Synthesis/Monad.hs | 1 + .../src/Language/Granule/Synthesis/Synth.hs | 1 + .../Granule/Synthesis/SynthLinearBase.hs | 1 + .../hspec/Data/Bifunctor/FoldableSpec.hs | 3 +++ granule.cabal | 27 ++++++++++--------- repl/app/Language/Granule/Main.hs | 3 ++- runtime/src/Language/Granule/Runtime.hs | 2 +- stack.yaml | 5 ++-- 18 files changed, 39 insertions(+), 26 deletions(-) diff --git a/frontend/src/Language/Granule/Checker/Checker.hs b/frontend/src/Language/Granule/Checker/Checker.hs index d0fcea0f3..15f0682df 100644 --- a/frontend/src/Language/Granule/Checker/Checker.hs +++ b/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(..)) diff --git a/frontend/src/Language/Granule/Checker/Kinding.hs b/frontend/src/Language/Granule/Checker/Kinding.hs index f5c8cf8ea..e40572ccf 100644 --- a/frontend/src/Language/Granule/Checker/Kinding.hs +++ b/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') diff --git a/frontend/src/Language/Granule/Checker/Monad.hs b/frontend/src/Language/Granule/Checker/Monad.hs index 5476f2ddd..9eecf882d 100644 --- a/frontend/src/Language/Granule/Checker/Monad.hs +++ b/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 diff --git a/frontend/src/Language/Granule/Checker/Patterns.hs b/frontend/src/Language/Granule/Checker/Patterns.hs index 6f57d7b62..0d78f7897 100644 --- a/frontend/src/Language/Granule/Checker/Patterns.hs +++ b/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(..)) diff --git a/frontend/src/Language/Granule/Checker/Predicates.hs b/frontend/src/Language/Granule/Checker/Predicates.hs index aedad6495..13f7e23bd 100644 --- a/frontend/src/Language/Granule/Checker/Predicates.hs +++ b/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 = diff --git a/frontend/src/Language/Granule/Checker/Types.hs b/frontend/src/Language/Granule/Checker/Types.hs index 618ef600f..c924e8af1 100644 --- a/frontend/src/Language/Granule/Checker/Types.hs +++ b/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 ((<&>)) diff --git a/frontend/src/Language/Granule/Syntax/Def.hs b/frontend/src/Language/Granule/Syntax/Def.hs index 1c830401a..b56f9b7d2 100644 --- a/frontend/src/Language/Granule/Syntax/Def.hs +++ b/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 diff --git a/frontend/src/Language/Granule/Syntax/Expr.hs b/frontend/src/Language/Granule/Syntax/Expr.hs index c01cde1b7..af9e12f3e 100755 --- a/frontend/src/Language/Granule/Syntax/Expr.hs +++ b/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 = e1 in e2 | HoleF Span a Bool [Id] (Maybe Hints) - deriving (Generic, Eq, Rp.Data) + deriving (Generic, Eq, Rp.Data, Functor) data Operator = OpLesser diff --git a/frontend/src/Language/Granule/Syntax/Pattern.hs b/frontend/src/Language/Granule/Syntax/Pattern.hs index 01c367227..2f3795ed5 100644 --- a/frontend/src/Language/Granule/Syntax/Pattern.hs +++ b/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 _ = [] diff --git a/frontend/src/Language/Granule/Syntax/Type.hs b/frontend/src/Language/Granule/Syntax/Type.hs index f05730da2..2d35440c6 100644 --- a/frontend/src/Language/Granule/Syntax/Type.hs +++ b/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 diff --git a/frontend/src/Language/Granule/Synthesis/Monad.hs b/frontend/src/Language/Granule/Synthesis/Monad.hs index 0fb52911b..7dc3359e8 100644 --- a/frontend/src/Language/Granule/Synthesis/Monad.hs +++ b/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 diff --git a/frontend/src/Language/Granule/Synthesis/Synth.hs b/frontend/src/Language/Granule/Synthesis/Synth.hs index 910240f93..bc5024211 100644 --- a/frontend/src/Language/Granule/Synthesis/Synth.hs +++ b/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) diff --git a/frontend/src/Language/Granule/Synthesis/SynthLinearBase.hs b/frontend/src/Language/Granule/Synthesis/SynthLinearBase.hs index cf5b8c6b0..014855c4f 100644 --- a/frontend/src/Language/Granule/Synthesis/SynthLinearBase.hs +++ b/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) diff --git a/frontend/tests/hspec/Data/Bifunctor/FoldableSpec.hs b/frontend/tests/hspec/Data/Bifunctor/FoldableSpec.hs index 513f59b34..bc81cb09a 100644 --- a/frontend/tests/hspec/Data/Bifunctor/FoldableSpec.hs +++ b/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 diff --git a/granule.cabal b/granule.cabal index 0cb15444d..20365382a 100644 --- a/granule.cabal +++ b/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 diff --git a/repl/app/Language/Granule/Main.hs b/repl/app/Language/Granule/Main.hs index d9dbceab6..e6e47076c 100644 --- a/repl/app/Language/Granule/Main.hs +++ b/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 diff --git a/runtime/src/Language/Granule/Runtime.hs b/runtime/src/Language/Granule/Runtime.hs index 11fcab2c5..43b4de844 100644 --- a/runtime/src/Language/Granule/Runtime.hs +++ b/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 diff --git a/stack.yaml b/stack.yaml index eacf13512..0d2e1311e 100644 --- a/stack.yaml +++ b/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 From 7555e1a391887f026257f0c922af63f5126e2a2f Mon Sep 17 00:00:00 2001 From: David Binder Date: Wed, 12 Aug 2026 13:20:40 +0100 Subject: [PATCH 2/6] Remove newline from goldenfile for testcase --- .../negative/simple/signature-equation-name-mismatch.gr.output | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontend/tests/cases/negative/simple/signature-equation-name-mismatch.gr.output b/frontend/tests/cases/negative/simple/signature-equation-name-mismatch.gr.output index 67bf5d175..4166db536 100644 --- a/frontend/tests/cases/negative/simple/signature-equation-name-mismatch.gr.output +++ b/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` \ No newline at end of file From aed91fff3bfa6b1d906ca4cfe0588667a77de232 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Wed, 12 Aug 2026 17:45:47 +0100 Subject: [PATCH 3/6] make hole synthesis use global timeout --- interpreter/src/Language/Granule/Interpreter.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/interpreter/src/Language/Granule/Interpreter.hs b/interpreter/src/Language/Granule/Interpreter.hs index 0fedb0c77..64fe153e1 100755 --- a/interpreter/src/Language/Granule/Interpreter.hs +++ b/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 From cb112cdec3c7739a5c8104ae320ef4164e58e263 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Wed, 12 Aug 2026 17:46:04 +0100 Subject: [PATCH 4/6] up timeout for synthesis example tests --- interpreter/tests/Golden.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/interpreter/tests/Golden.hs b/interpreter/tests/Golden.hs index 3fd398a8b..b44ef12aa 100644 --- a/interpreter/tests/Golden.hs +++ b/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 From 675423a7d1067116983289937fdd0a4a5834ba92 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Wed, 12 Aug 2026 21:36:17 +0100 Subject: [PATCH 5/6] up local timeout and mark either as no longer a known fault --- .known-issues | 1 - interpreter/tests/Golden.hs | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/.known-issues b/.known-issues index 71cb2c9cf..4d4eb0863 100644 --- a/.known-issues +++ b/.known-issues @@ -2,7 +2,6 @@ frontend/tests/cases/positive/indexed/infer-kinds.gr #299 frontend/tests/cases/positive/security/level_pos3.gr #314 frontend/tests/cases/rewrite/split-in-box.gr #313 frontend/tests/cases/synthesis/graded-base/list/drop.gr #281 -frontend/tests/cases/synthesis/graded-base/misc/either.gr #281 examples/effects_nondet.gr #312 examples/effects_state.gr #312 frontend/tests/cases/positive/effect-handlers/effects_state.gr #312 diff --git a/interpreter/tests/Golden.hs b/interpreter/tests/Golden.hs index b44ef12aa..c743ee99f 100644 --- a/interpreter/tests/Golden.hs +++ b/interpreter/tests/Golden.hs @@ -215,7 +215,7 @@ goldenTestsSynthesis config = do globalsRewriteHoles = Just True, globalsIncludePath = Just "StdLib", -- Slightly longer for synthesis examples which can be heavy - globalsSolverTimeoutMillis = Just 30000 } + globalsSolverTimeoutMillis = Just 40000 } subtractiveGlobals :: FilePath -> Globals From 42e1d823f71f7736b82e86319a0bd4729f6eb164 Mon Sep 17 00:00:00 2001 From: Dominic Orchard Date: Thu, 13 Aug 2026 14:15:14 +0100 Subject: [PATCH 6/6] mark either as expected fail --- .known-issues | 1 + 1 file changed, 1 insertion(+) diff --git a/.known-issues b/.known-issues index 4d4eb0863..71cb2c9cf 100644 --- a/.known-issues +++ b/.known-issues @@ -2,6 +2,7 @@ frontend/tests/cases/positive/indexed/infer-kinds.gr #299 frontend/tests/cases/positive/security/level_pos3.gr #314 frontend/tests/cases/rewrite/split-in-box.gr #313 frontend/tests/cases/synthesis/graded-base/list/drop.gr #281 +frontend/tests/cases/synthesis/graded-base/misc/either.gr #281 examples/effects_nondet.gr #312 examples/effects_state.gr #312 frontend/tests/cases/positive/effect-handlers/effects_state.gr #312