granule-project · dorchard · Jul 21, 2026 · Jul 8, 2026
diff --git a/benchmark/src/Main.hs b/benchmark/src/Main.hs
@@ -1,6 +1,5 @@
 {-# OPTIONS_GHC -Wno-unused-imports -Wno-unused-local-binds #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 
 {-
 This tool is for quantitatively evaluating the --synthesis feature

diff --git a/compiler/app/Language/Granule/Compiler.hs b/compiler/app/Language/Granule/Compiler.hs
@@ -2,7 +2,6 @@
 {-# LANGUAGE ApplicativeDo #-}
 {-# LANGUAGE PackageImports #-}
 {-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE NamedFieldPuns #-}
 module Language.Granule.Compiler where
 
 import Control.Exception (SomeException, displayException, try)

diff --git a/compiler/src/Language/Granule/Compiler/HSCodegen.hs b/compiler/src/Language/Granule/Compiler/HSCodegen.hs
@@ -3,7 +3,6 @@
 {-# OPTIONS_GHC -Wno-unused-imports #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 {-# OPTIONS_GHC -Wno-typed-holes #-}
-{-# LANGUAGE NamedFieldPuns #-}
 module Language.Granule.Compiler.HSCodegen where
 
 import Control.Monad

diff --git a/frontend/src/Data/Bifunctor/Foldable.hs b/frontend/src/Data/Bifunctor/Foldable.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FunctionalDependencies #-}
 
 {- This module contains some recursion schemes designed for use with mutually

diff --git a/frontend/src/Language/Granule/Checker/Checker.hs b/frontend/src/Language/Granule/Checker/Checker.hs
@@ -1,9 +1,5 @@
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 

diff --git a/frontend/src/Language/Granule/Checker/Coeffects.hs b/frontend/src/Language/Granule/Checker/Coeffects.hs
@@ -1,5 +1,4 @@
 {- Deals with coeffect resource algebras -}
-{-# LANGUAGE ImplicitParams #-}
 
 module Language.Granule.Checker.Coeffects where
 

diff --git a/frontend/src/Language/Granule/Checker/Constraints.hs b/frontend/src/Language/Granule/Checker/Constraints.hs
@@ -1,9 +1,5 @@
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 

diff --git a/frontend/src/Language/Granule/Checker/Constraints/Compile.hs b/frontend/src/Language/Granule/Checker/Constraints/Compile.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE DataKinds #-}
 

diff --git a/frontend/src/Language/Granule/Checker/Constraints/SFrac.hs b/frontend/src/Language/Granule/Checker/Constraints/SFrac.hs
@@ -2,7 +2,6 @@
 
 {-# LANGUAGE DeriveAnyClass  #-}
 {-# LANGUAGE DeriveGeneric   #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 
 -- | Represents fractions with star in the solver
 module Language.Granule.Checker.Constraints.SFrac where

diff --git a/frontend/src/Language/Granule/Checker/Constraints/SNatX.hs b/frontend/src/Language/Granule/Checker/Constraints/SNatX.hs
@@ -2,7 +2,6 @@
 
 {-# LANGUAGE DeriveAnyClass  #-}
 {-# LANGUAGE DeriveGeneric   #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 
 -- | Represents the extended natural numbers in the solver
 module Language.Granule.Checker.Constraints.SNatX where

diff --git a/frontend/src/Language/Granule/Checker/DataTypes.hs b/frontend/src/Language/Granule/Checker/DataTypes.hs
@@ -1,8 +1,5 @@
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 

diff --git a/frontend/src/Language/Granule/Checker/Effects.hs b/frontend/src/Language/Granule/Checker/Effects.hs
@@ -1,6 +1,4 @@
 {- Deals with effect algebras -}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 

diff --git a/frontend/src/Language/Granule/Checker/Kinding.hs b/frontend/src/Language/Granule/Checker/Kinding.hs
@@ -1,10 +1,6 @@
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE FlexibleContexts #-}
 
 -- | Kind checking and inference algorithms
 -- | as well as the core type variable unifier

diff --git a/frontend/src/Language/Granule/Checker/Monad.hs b/frontend/src/Language/Granule/Checker/Monad.hs
@@ -1,13 +1,9 @@
-
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE OverloadedStrings #-}
 
 {-# options_ghc -fno-warn-incomplete-uni-patterns #-}
 {-# options_ghc -fno-warn-orphans #-}

diff --git a/frontend/src/Language/Granule/Checker/Patterns.hs b/frontend/src/Language/Granule/Checker/Patterns.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE ImplicitParams #-}
 
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}

diff --git a/frontend/src/Language/Granule/Checker/Predicates.hs b/frontend/src/Language/Granule/Checker/Predicates.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE DeriveGeneric #-}
 
 -- | This module provides the representation of theorems (predicates)

diff --git a/frontend/src/Language/Granule/Checker/Primitives.hs b/frontend/src/Language/Granule/Checker/Primitives.hs
@@ -1,9 +1,7 @@
 -- Provides all the type information for built-ins
 
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ImplicitParams #-}
 
 -- | Primitive data types and type constructors
 module Language.Granule.Checker.Primitives where

diff --git a/frontend/src/Language/Granule/Checker/Simplifier.hs b/frontend/src/Language/Granule/Checker/Simplifier.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE ImplicitParams #-}
-
 -- | Simplifier for predicates (useful for error messages)
 module Language.Granule.Checker.Simplifier where
 

diff --git a/frontend/src/Language/Granule/Checker/Substitution.hs b/frontend/src/Language/Granule/Checker/Substitution.hs
@@ -1,8 +1,6 @@
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
 
 -- Provides the core functionality for substitutions
 

diff --git a/frontend/src/Language/Granule/Checker/SubstitutionContexts.hs b/frontend/src/Language/Granule/Checker/SubstitutionContexts.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE DataKinds #-}
 module Language.Granule.Checker.SubstitutionContexts where
 

diff --git a/frontend/src/Language/Granule/Checker/Types.hs b/frontend/src/Language/Granule/Checker/Types.hs
@@ -1,7 +1,4 @@
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 

diff --git a/frontend/src/Language/Granule/Checker/Variables.hs b/frontend/src/Language/Granule/Checker/Variables.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE FlexibleContexts #-}
-
 -- | Helpers for working with type variables in the type checker
 module Language.Granule.Checker.Variables where
 

diff --git a/frontend/src/Language/Granule/Syntax/Def.hs b/frontend/src/Language/Granule/Syntax/Def.hs
@@ -1,12 +1,10 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE RecordWildCards #-}
 
 module Language.Granule.Syntax.Def where
 

diff --git a/frontend/src/Language/Granule/Syntax/Expr.hs b/frontend/src/Language/Granule/Syntax/Expr.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE InstanceSigs #-}

diff --git a/frontend/src/Language/Granule/Syntax/FirstParameter.hs b/frontend/src/Language/Granule/Syntax/FirstParameter.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 

diff --git a/frontend/src/Language/Granule/Syntax/Helpers.hs b/frontend/src/Language/Granule/Syntax/Helpers.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 
 {-# options_ghc -Wno-orphans #-}

diff --git a/frontend/src/Language/Granule/Syntax/Parser.y b/frontend/src/Language/Granule/Syntax/Parser.y
@@ -1,6 +1,4 @@
 {
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 

diff --git a/frontend/src/Language/Granule/Syntax/Pattern.hs b/frontend/src/Language/Granule/Syntax/Pattern.hs
@@ -1,11 +1,9 @@
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE LambdaCase #-}
 
 module Language.Granule.Syntax.Pattern where
 

diff --git a/frontend/src/Language/Granule/Syntax/Preprocessor.hs b/frontend/src/Language/Granule/Syntax/Preprocessor.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE ScopedTypeVariables #-}
-
 module Language.Granule.Syntax.Preprocessor where
 
 import Data.List (intercalate)

diff --git a/frontend/src/Language/Granule/Syntax/Preprocessor/Ascii.hs b/frontend/src/Language/Granule/Syntax/Preprocessor/Ascii.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE OverloadedStrings #-}
-
 module Language.Granule.Syntax.Preprocessor.Ascii
   ( asciiToUnicode
   , unicodeToAscii

diff --git a/frontend/src/Language/Granule/Syntax/Pretty.hs b/frontend/src/Language/Granule/Syntax/Pretty.hs
@@ -3,12 +3,7 @@
 -- Useful in debugging and error messages
 
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE InstanceSigs #-}
 

diff --git a/frontend/src/Language/Granule/Syntax/SecondParameter.hs b/frontend/src/Language/Granule/Syntax/SecondParameter.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 

diff --git a/frontend/src/Language/Granule/Syntax/Span.hs b/frontend/src/Language/Granule/Syntax/Span.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 
 module Language.Granule.Syntax.Span where

diff --git a/frontend/src/Language/Granule/Syntax/Type.hs b/frontend/src/Language/Granule/Syntax/Type.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -9,7 +8,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 
 -- Syntax of types
 

diff --git a/frontend/src/Language/Granule/Synthesis/Common.hs b/frontend/src/Language/Granule/Synthesis/Common.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE OverloadedStrings #-}
 module Language.Granule.Synthesis.Common where
 
 import Language.Granule.Context

diff --git a/frontend/src/Language/Granule/Synthesis/LinearHaskell.hs b/frontend/src/Language/Granule/Synthesis/LinearHaskell.hs
@@ -1,6 +1,5 @@
 {-# OPTIONS_GHC -Wno-unused-imports #-}
 
-{-# LANGUAGE ScopedTypeVariables #-}
 
 module Language.Granule.Synthesis.LinearHaskell where
 

diff --git a/frontend/src/Language/Granule/Synthesis/Monad.hs b/frontend/src/Language/Granule/Synthesis/Monad.hs
@@ -1,6 +1,4 @@
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE FlexibleContexts #-}
 
 module Language.Granule.Synthesis.Monad where
 

diff --git a/frontend/src/Language/Granule/Synthesis/RewriteHoles.hs b/frontend/src/Language/Granule/Synthesis/RewriteHoles.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DataKinds #-}
 
 module Language.Granule.Synthesis.RewriteHoles

diff --git a/frontend/src/Language/Granule/Synthesis/Synth.hs b/frontend/src/Language/Granule/Synthesis/Synth.hs
@@ -1,6 +1,4 @@
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 
 

diff --git a/frontend/src/Language/Granule/Synthesis/SynthLinearBase.hs b/frontend/src/Language/Granule/Synthesis/SynthLinearBase.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE ImplicitParams #-}
 {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 
 

diff --git a/frontend/src/Language/Granule/Utils.hs b/frontend/src/Language/Granule/Utils.hs
@@ -1,6 +1,3 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PackageImports #-}
 
 module Language.Granule.Utils where

diff --git a/frontend/tests/hspec/Language/Granule/Checker/CheckerSpec.hs b/frontend/tests/hspec/Language/Granule/Checker/CheckerSpec.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE DataKinds #-}
 
 module Language.Granule.Checker.CheckerSpec where

diff --git a/frontend/tests/hspec/Language/Granule/Checker/KindSpec.hs b/frontend/tests/hspec/Language/Granule/Checker/KindSpec.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE ImplicitParams #-}
-
 module Language.Granule.Checker.KindSpec where
 
 import Test.Hspec

diff --git a/frontend/tests/hspec/Language/Granule/Checker/MonadSpec.hs b/frontend/tests/hspec/Language/Granule/Checker/MonadSpec.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ImplicitParams #-}
 
 module Language.Granule.Checker.MonadSpec where
 

diff --git a/frontend/tests/hspec/Language/Granule/Checker/SubstitutionsSpec.hs b/frontend/tests/hspec/Language/Granule/Checker/SubstitutionsSpec.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE ImplicitParams #-}
-
 module Language.Granule.Checker.SubstitutionsSpec where
 
 import Language.Granule.Syntax.Type

diff --git a/frontend/tests/hspec/Language/Granule/Checker/TypesSpec.hs b/frontend/tests/hspec/Language/Granule/Checker/TypesSpec.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE ImplicitParams #-}
-
 module Language.Granule.Checker.TypesSpec where
 
 import Language.Granule.Syntax.Identifiers

diff --git a/interpreter/src/Language/Granule/Doc.hs b/interpreter/src/Language/Granule/Doc.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE ViewPatterns #-}
 module Language.Granule.Doc where
 
 -- grdoc - Documentation generator

diff --git a/interpreter/src/Language/Granule/Interpreter.hs b/interpreter/src/Language/Granule/Interpreter.hs
@@ -9,12 +9,8 @@
        \_/__/
 -}
 {-# LANGUAGE ApplicativeDo #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE PackageImports #-}
 {-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE TemplateHaskell #-}
 
 module Language.Granule.Interpreter where

diff --git a/interpreter/src/Language/Granule/Interpreter/Desugar.hs b/interpreter/src/Language/Granule/Interpreter/Desugar.hs
@@ -1,7 +1,4 @@
 -- Provides the desugaring step of the language
-
-{-# LANGUAGE ViewPatterns #-}
-
 module Language.Granule.Interpreter.Desugar where
 
 import Language.Granule.Syntax.Def

diff --git a/interpreter/src/Language/Granule/Interpreter/Eval.hs b/interpreter/src/Language/Granule/Interpreter/Eval.hs
@@ -1,11 +1,6 @@
 -- Granule interpreter
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ViewPatterns #-}
-{-# LANGUAGE LambdaCase #-}
-
 
 {-# options_ghc -Wno-incomplete-uni-patterns #-}
 

diff --git a/repl/app/Language/Granule/Main.hs b/repl/app/Language/Granule/Main.hs
@@ -1,8 +1,5 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ApplicativeDo #-}
-{-# LANGUAGE ImplicitParams #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE PackageImports #-}
 
 module Main where
Original file line number	Diff line number	Diff line change
		@@ -1,4 +1,3 @@
		{-# LANGUAGE ImplicitParams #-}
		{-# OPTIONS_GHC -Wno-incomplete-patterns #-}


Expand Down