diff --git a/benchmark/src/Main.hs b/benchmark/src/Main.hs
index f75896cd..41f71d72 100644
--- 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
index e868cded..4d71d01c 100644
--- 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
index fdb6de04..d45b5c64 100644
--- 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
index cb9baa5c..79607db3 100644
--- 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
index d0fcea0f..f93f96e4 100644
--- 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
index 386fc713..5f40989f 100644
--- 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
index 476a6c3d..1f628729 100644
--- 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
index aad42220..8bbfa669 100644
--- 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
index f095c793..737aba8f 100644
--- 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
index eac6ad8b..ce71c2bb 100644
--- 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
index fcd15f4f..60c2a675 100644
--- 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
index aff8f96b..71bd3963 100644
--- 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
index f5c8cf8e..39e8adee 100644
--- 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
index 5476f2dd..58dfc40d 100644
--- 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
index 6f57d7b6..62dc8c2a 100644
--- 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
index aedad649..fda87998 100644
--- 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
index 391589a9..278fa8ab 100644
--- 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
index d7d1e838..f74fd192 100644
--- 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
index bc3ec489..d0a8121b 100644
--- 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
index 43934e06..2e440078 100644
--- 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
index 618ef600..44ae5c92 100644
--- 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
index 83400a96..93e612d3 100644
--- 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
index 1c830401..11957d57 100644
--- 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
index c01cde1b..cfa5bcc7 100755
--- 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
index 720cde26..2aeb72af 100644
--- 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
index 37ab5c71..62ee5bda 100644
--- 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
index 87f6fbb0..ecafaeda 100644
--- 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
index 01c36722..c6d72637 100644
--- 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
index 3180d1bf..ac3ba6b8 100644
--- 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
index 337263cb..930301f1 100644
--- 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
index b62fda1a..db3ee122 100644
--- 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
index e04369f6..e0b1d8b7 100644
--- 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
index 902da749..2a553ecf 100644
--- 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
index f05730da..acede270 100644
--- 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
index 901aeaa0..a4d13185 100644
--- 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
index 17dd28c6..4cfc4518 100644
--- 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
index 0fb52911..3609b937 100644
--- 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
index b735e5ba..25ab0dfd 100644
--- 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
index 910240f9..0a5879e0 100644
--- 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
index cf5b8c6b..39a90d44 100644
--- 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
index 2ff8ea6a..e50cab9f 100644
--- 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
index c86f6348..9569a8e6 100644
--- 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
index 5cf4d0d3..9d9a9900 100644
--- 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
index e3425397..939e2e71 100644
--- 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
index d35a7ca3..f2060291 100644
--- 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
index caba1f53..0926838e 100644
--- 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
index f33f7461..13e7a603 100644
--- 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
index 0fedb0c7..0a7519c3 100755
--- 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
index f259d667..d2cc1980 100644
--- 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
index ef9e05dd..b4889568 100755
--- 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
index d9dbceab..f2c91ab4 100644
--- 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
diff --git a/repl/app/Language/Granule/ReplError.hs b/repl/app/Language/Granule/ReplError.hs
index c3c9cce5..8c0f3d91 100644
--- a/repl/app/Language/Granule/ReplError.hs
+++ b/repl/app/Language/Granule/ReplError.hs
@@ -1,6 +1,3 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE ImplicitParams #-}
-
 module Language.Granule.ReplError where
 
 import Control.Monad.Except()
diff --git a/repl/app/Language/Granule/ReplParser.hs b/repl/app/Language/Granule/ReplParser.hs
index 52bd239b..aebc1cf1 100644
--- a/repl/app/Language/Granule/ReplParser.hs
+++ b/repl/app/Language/Granule/ReplParser.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE FlexibleContexts #-}
 module Language.Granule.ReplParser where
 
 import Prelude
diff --git a/runtime/src/Language/Granule/Runtime.hs b/runtime/src/Language/Granule/Runtime.hs
index 11fcab2c..4794fc4f 100644
--- a/runtime/src/Language/Granule/Runtime.hs
+++ b/runtime/src/Language/Granule/Runtime.hs
@@ -1,6 +1,6 @@
 -- | Implementations of builtin Granule functions in Haskell
 
-{-# LANGUAGE NamedFieldPuns, Strict, NoImplicitPrelude, TypeFamilies,
+{-# LANGUAGE Strict, NoImplicitPrelude, TypeFamilies,
              DataKinds, GADTs #-}
 {-# OPTIONS_GHC -fno-full-laziness -fno-warn-unused-binds #-}
 module Language.Granule.Runtime
diff --git a/server/app/Language/Granule/Server.hs b/server/app/Language/Granule/Server.hs
index 3a1e42c7..c3432449 100644
--- a/server/app/Language/Granule/Server.hs
+++ b/server/app/Language/Granule/Server.hs
@@ -1,9 +1,6 @@
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 
 module Language.Granule.Server where