diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,6 @@
-## 0.6.1 (2021-03-03)
+## 0.6.2 (16 Jun 2021)
+* Support GHC 9.0
+
+## 0.6.1 (03 Mar 2021)
 * Require at least Vinyl 0.9 (`RMap` etc. via type classes)
 * Support at least GHC 8.6, 8.8, 8.10
diff --git a/Language/Expression/Scope.hs b/Language/Expression/Scope.hs
--- a/Language/Expression/Scope.hs
+++ b/Language/Expression/Scope.hs
@@ -45,8 +45,12 @@
 -- instance (HFoldableAt k g) => HFoldableAt k (BV g) where
 --   hfoldMap = hbifoldMap . hfoldMap
 
+-- Note that since GHC 9.0, a handful of these instances must be eta-expanded
+-- manually due to simplified subsumption. So if you see an @f@ or @g@ that
+-- looks like it could be omitted with a pointfree-er definition, that's likely
+-- the reason.
 instance HTraversable (BV g) where
-  htraverse = hbitraverseBV pure
+  htraverse f = hbitraverseBV pure f
 
 foldBV :: (w a -> r) -> (v a -> r) -> BV w v a -> r
 foldBV f g = \case
@@ -54,10 +58,10 @@
   F y -> g y
 
 instance HBifunctor BV where
-  hbimap = hbimapBV
+  hbimap f g = hbimapBV f g
 
 instance HBitraversable BV where
-  hbitraverse = hbitraverseBV
+  hbitraverse f g = hbitraverseBV f g
 
 hbitraverseBV :: (Functor t) => (g a -> t (g' b)) -> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b)
 hbitraverseBV f g = foldBV (fmap B . f) (fmap F . g)
@@ -66,7 +70,7 @@
 hbimapBV f g = foldBV (B . f) (F . g)
 
 instance HBifoldableAt k BV where
-  hbifoldMap = foldBV
+  hbifoldMap f g = foldBV f g
 
 --------------------------------------------------------------------------------
 --  Scopes
diff --git a/verifiable-expressions.cabal b/verifiable-expressions.cabal
--- a/verifiable-expressions.cabal
+++ b/verifiable-expressions.cabal
@@ -1,13 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.33.0.
+-- This file has been generated from package.yaml by hpack version 0.34.4.
 --
 -- see: https://github.com/sol/hpack
---
--- hash: b61cc1fb115270326d22ec5fbcdd0a38b0aed4c1489d119b344cf4e41c987188
 
 name:           verifiable-expressions
-version:        0.6.1
+version:        0.6.2
 synopsis:       An intermediate language for Hoare logic style verification.
 description:    A typed intermediate language for Hoare logic style verification. It defines the intermediate language and combinators to interact it.
 category:       Language
@@ -49,10 +47,10 @@
   build-depends:
       base >=4.9 && <5
     , containers >=0.5.7 && <0.7
-    , lens >=4.16.1 && <5
+    , lens >=4.16.1 && <5.1
     , mtl >=2.0 && <3
     , sbv >=8.0 && <9
-    , transformers >=0.5 && <0.6
+    , transformers ==0.5.*
     , union >=0.1.1 && <0.2
     , vinyl >=0.9 && <0.14
   default-language: Haskell2010