diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,3 +3,12 @@
 ## 0.1.0.0 -- 2024-07-21
 
 * initial release
+
+## 0.2.0.0 -- 2024-11-15
+
+* moved to required type arguments wherever possible
+* dropped support for GHC < 9.10
+* dropped support for base < 4.20
+* stopped reexporting Proxy
+* make `getElem` and `getElem'` take required type arguments, the search strategy and the type of the field, as well as the name of the field in the case of `getElem`
+* make all hc* functions take the constraint as a required type argument
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,8 +1,6 @@
-
-[![built with nix](https://img.shields.io/badge/built%20with-nix-%235277C3?logo=nixos)](https://nixos.org/)
 [![built on haskell](https://img.shields.io/badge/built%20on-haskell-%235D4F85?logo=haskell)](https://www.haskell.org/)
 ![ci](https://ci.mangoiv.com/api/badges/5/status.svg)
-[![haddock](https://img.shields.io/badge/haddock-mangoiv.com-e0b0ff)](https://mangoiv.com/htree)
+[![hackage](https://img.shields.io/hackage/v/htree.svg)](https://hackage.haskell.org/package/htree)
 
 # `htree`: heterogeneous rose tree 
 
@@ -60,9 +58,9 @@
   , TyNodeL "foo" Int '[]
   ]
 
--- >>> getElem @'DFS @"foo" @Int Proxy labeledTree
+-- >>> getElem DFS "foo" Int labeledTree
 -- Identity 69
--- >>> getElem @'BFS @"foo" @Int Proxy labeledTree
+-- >>> getElem BFS "foo" Int labeledTree
 -- Identity 67
 labeledTree :: HTree Identity LabeledTree
 labeledTree = 42 `HNodeL` HNodeL 4 (HNodeL 69 HNil ::: HNil) ::: HNodeL 67 HNil ::: HNil
diff --git a/htree.cabal b/htree.cabal
--- a/htree.cabal
+++ b/htree.cabal
@@ -1,19 +1,13 @@
 cabal-version:   3.4
 name:            htree
-tested-with:     GHC ==9.2.8 || ==9.4.8 || ==9.6.4 || ==9.8.1
-version:         0.1.1.0
+tested-with:     GHC ==9.10.1
+version:         0.2.0.0
 synopsis:
   a library to build and work with heterogeneous, type level indexed rose trees
 
 description:
   This library implements a heterogeneous rose-tree (HTree) that is indexed by a type-level rosetree (TyTree).
 
-  It also offers some useful functions, highlights include:
-
-      searching in the tree and creating evidence on the term-level via typeclasses
-      record-dot syntax for accessing elements in the tree.
-      mapping and traversing trees
-
 license:         AGPL-3.0-or-later
 license-file:    LICENSE
 author:          mangoiv
@@ -41,10 +35,12 @@
     OverloadedStrings
     PatternSynonyms
     QuantifiedConstraints
+    RequiredTypeArguments
+    TypeAbstractions
     TypeFamilies
     ViewPatterns
 
-  build-depends:      base >=4.16 && <5
+  build-depends:      base >=4.20 && <5
 
 library
   import:           warnings-and-imports
diff --git a/src/Data/HTree/Constraint.hs b/src/Data/HTree/Constraint.hs
--- a/src/Data/HTree/Constraint.hs
+++ b/src/Data/HTree/Constraint.hs
@@ -61,8 +61,8 @@
 proves (Proves x) k = k x
 
 -- | 'Has' but specialised to 'Typeable'
-type HasTypeable :: (k -> Type) -> k -> Type
-type HasTypeable = Has Typeable
+type HasTypeable :: forall k. (k -> Type) -> k -> Type
+type HasTypeable @k = Has Typeable
 
 -- | 'Has' but specialised to a constant type, @Some (HasIs k f)@ is isomorphic to @f k@
 type HasIs :: k -> (k -> Type) -> k -> Type
diff --git a/src/Data/HTree/Existential.hs b/src/Data/HTree/Existential.hs
--- a/src/Data/HTree/Existential.hs
+++ b/src/Data/HTree/Existential.hs
@@ -65,11 +65,11 @@
 
 -- | HTree but the type level tree is existential
 type ETree :: forall k. (k -> Type) -> Type
-type ETree = Some2 HTree
+type ETree @k = Some2 HTree
 
 -- | HList but the type level list is existential
 type EList :: forall k. (k -> Type) -> Type
-type EList = Some2 HList
+type EList @k = Some2 HList
 
 -- | 'with2' specialized to 'HTree's
 withSomeHTree :: ETree f -> (forall t. HTree f t -> r) -> r
diff --git a/src/Data/HTree/Labeled.hs b/src/Data/HTree/Labeled.hs
--- a/src/Data/HTree/Labeled.hs
+++ b/src/Data/HTree/Labeled.hs
@@ -23,7 +23,6 @@
 
     -- ** Reexports
   , HasField (..)
-  , Proxy (..)
 
     -- * Internal
   , HasField' (..)
@@ -72,31 +71,33 @@
 getElemWithPath (Deeper pt) (HNode _ (t `HCons` _)) = getElemWithPath pt t
 
 -- | searches a tree for an element and returns that element
-getElem' :: forall {proxy} strat typ t f. HasField' (strat :: SearchStrategy) typ t => proxy strat -> HTree f t -> f typ
-getElem' _ = getElemWithPath (evidence @strat @typ @t Proxy)
+getElem' :: forall t f. forall (strat :: SearchStrategy) -> forall typ -> HasField' strat typ t => HTree f t -> f typ
+getElem' strat typ = getElemWithPath (evidence @strat @typ @t Proxy)
 
 -- | searches a tree for an element and returns that element, specialised to 'Labeled' and unwraps
 --
 -- >>> import Data.Functor.Identity
 -- >>> type T = TyNodeL "top" Int [ TyNodeL "inter" Int '[ TyNodeL "foo" Int '[]], TyNodeL "foo" Int '[]]
 -- >>> t :: HTree Identity T = 42 `HNodeL` HNodeL 4 (HNodeL 69 HNil `HCons` HNil) `HCons` HNodeL 67 HNil `HCons` HNil
--- >>> getElem @'DFS @"foo" @Int Proxy t
+-- >>> getElem DFS "foo" Int t
 -- Identity 69
--- >>> getElem @'BFS @"foo" @Int Proxy t
+-- >>> getElem BFS "foo" Int t
 -- Identity 67
 getElem
-  :: forall {proxy} strat l typ t f
-   . ( HasField' (strat :: SearchStrategy) (Labeled l typ) t
-     , Functor f
-     )
-  => proxy strat
-  -> HTree f t
+  :: forall {k} t f
+   . forall (strat :: SearchStrategy)
+    ->forall (l :: k)
+    ->forall (typ :: Type)
+    ->( HasField' strat (Labeled l typ) t
+      , Functor f
+      )
+  => HTree f t
   -> f typ
-getElem _ = fmap unLabel . getElemWithPath (evidence @strat @(Labeled l typ) @t Proxy)
+getElem strat l typ = fmap unLabel . getElemWithPath (evidence @strat @(Labeled l typ) @t Proxy)
 
 -- the default behaviour is a breadth first search
 instance (HasField' 'BFS (Labeled l typ) t, Functor f) => HasField l (HTree f t) (f typ) where
-  getField = getElem @'BFS @l @typ @t Proxy
+  getField = getElem BFS l typ
 
 -- | simple typelevel predicate that tests whether some element is in a tree
 type Elem :: forall k. k -> TyTree k -> Bool
diff --git a/src/Data/HTree/List.hs b/src/Data/HTree/List.hs
--- a/src/Data/HTree/List.hs
+++ b/src/Data/HTree/List.hs
@@ -57,33 +57,33 @@
 
 -- | map with a function that maps forall f a
 hmap :: forall f g xs. (forall a. f a -> g a) -> HList f xs -> HList g xs
-hmap f l = withDict (allTopHList l) $ hcmap @Top @f @g f l
+hmap f l = withDict (allTopHList l) $ hcmap Top f l
 
 -- | map with a constraint that holds for all elements of the  list
 --
 -- >>> import Data.Functor.Const
 -- >>> hcmap @Show (Const . show . runIdentity) (42 `HCons` HSing "bla" :: HList Identity '[ Int, String ])
 -- HCons (Const "42") (HCons (Const "\"bla\"") HNil)
-hcmap :: forall c f g xs. All c xs => (forall a. c a => f a -> g a) -> HList f xs -> HList g xs
-hcmap f = runIdentity . hctraverse @c @Identity @f @g (Identity . f)
+hcmap :: forall f g xs. forall c -> All c xs => (forall a. c a => f a -> g a) -> HList f xs -> HList g xs
+hcmap c f = runIdentity . hctraverse c (Identity . f)
 
 -- | traverse a structure with a function
 htraverse :: forall t f g xs. Applicative t => (forall a. f a -> t (g a)) -> HList f xs -> t (HList g xs)
-htraverse f l = withDict (allTopHList l) $ hctraverse @Top @t @f @g f l
+htraverse f l = withDict (allTopHList l) $ hctraverse Top f l
 
 -- | traverse a structure such that a constraint holds; this is the workhorse of mapping and traversing
 --
 -- >>> import Data.Functor.Const
 -- >>> hctraverse @Show (Just . Const . show . runIdentity) (42 `HCons` HSing "bla" :: HList Identity '[ Int, String ])
 -- Just (HCons (Const "42") (HCons (Const "\"bla\"") HNil))
-hctraverse :: forall c t f g xs. (All c xs, Applicative t) => (forall a. c a => f a -> t (g a)) -> HList f xs -> t (HList g xs)
-hctraverse _ HNil = pure HNil
-hctraverse f (HCons x xs) = HCons <$> f x <*> hctraverse @c @t @f @g f xs
+hctraverse :: forall t f g xs. forall c -> (All c xs, Applicative t) => (forall a. c a => f a -> t (g a)) -> HList f xs -> t (HList g xs)
+hctraverse _ _ HNil = pure HNil
+hctraverse c f (HCons x xs) = HCons <$> f x <*> hctraverse c f xs
 
 -- | foldr for HLists.
-hcFold :: forall c f b xs. All c xs => (forall a. c a => f a -> b -> b) -> b -> HList f xs -> b
-hcFold _ def HNil = def
-hcFold f def (x `HCons` xs) = f x $ hcFold @c f def xs
+hcFold :: forall f b xs. forall c -> All c xs => (forall a. c a => f a -> b -> b) -> b -> HList f xs -> b
+hcFold _ _ def HNil = def
+hcFold c f def (x `HCons` xs) = f x $ hcFold c f def xs
 
 -- | witnesses that for all HLists, we can always derive the All Top constraint
 allTopHList :: forall f xs. HList f xs -> Dict (All Top xs)
diff --git a/src/Data/HTree/Tree.hs b/src/Data/HTree/Tree.hs
--- a/src/Data/HTree/Tree.hs
+++ b/src/Data/HTree/Tree.hs
@@ -90,21 +90,21 @@
    . (forall a. f a -> g a)
   -> HTree f t
   -> HTree g t
-hmap f t = withDict (allTopHTree t) $ hcmap @Top @f @g f t
+hmap f t = withDict (allTopHTree t) $ hcmap Top f t
 
 -- | map a function with a constraint over an HTree
 hcmap
   :: forall
     {k}
-    (c :: k -> Constraint)
     (f :: k -> Type)
     (g :: k -> Type)
     (t :: TyTree k)
-   . AllTree c t
+   . forall (c :: k -> Constraint)
+    ->AllTree c t
   => (forall a. c a => f a -> g a)
   -> HTree f t
   -> HTree g t
-hcmap f = runIdentity . hctraverse @c @Identity @f @g (Identity . f)
+hcmap c f = runIdentity . hctraverse c (Identity . f)
 
 -- | traverse a structure with a function
 htraverse
@@ -118,22 +118,22 @@
   => (forall a. f a -> h (g a))
   -> HTree f t
   -> h (HTree g t)
-htraverse f t = withDict (allTopHTree t) $ hctraverse @Top f t
+htraverse f t = withDict (allTopHTree t) $ hctraverse Top f t
 
 -- | traverse a structure such that a constraint holds; this is the workhorse of mapping and traversing
 hctraverse
   :: forall
     {k}
-    (c :: k -> Constraint)
     (h :: Type -> Type)
     (f :: k -> Type)
     (g :: k -> Type)
     (t :: TyTree k)
-   . (AllTree c t, Applicative h)
+   . forall (c :: k -> Constraint)
+    ->(AllTree c t, Applicative h)
   => (forall a. c a => f a -> h (g a))
   -> HTree f t
   -> h (HTree g t)
-hctraverse f (HNode x ts) = HNode <$> f x <*> L.hctraverse @(AllTreeC c) @h @(HTree f) @(HTree g) (hctraverse @c f) ts
+hctraverse c f (HNode x ts) = HNode <$> f x <*> L.hctraverse (AllTreeC c) (hctraverse c f) ts
 
 -- | map a functor over a TyTree
 type TreeMap :: forall k l. (k -> l) -> TyTree k -> TyTree l
@@ -152,16 +152,16 @@
 hcFoldMap
   :: forall
     {k}
-    (c :: k -> Constraint)
     (f :: k -> Type)
     (t :: TyTree k)
     (b :: Type)
-   . (AllTree c t, Semigroup b)
+   . forall (c :: k -> Constraint)
+    ->(AllTree c t, Semigroup b)
   => (forall a. c a => f a -> b)
   -> HTree f t
   -> b
-hcFoldMap f (HNode x HNil) = f x
-hcFoldMap f (HNode x (y `HCons` ys)) = hcFoldMap @c f y <> hcFoldMap @c f (HNode x ys)
+hcFoldMap _ f (HNode x HNil) = f x
+hcFoldMap c f (HNode x (y `HCons` ys)) = hcFoldMap c f y <> hcFoldMap c f (HNode x ys)
 
 -- | monoidally folds down a tree to a single value, this is similar to 'foldMap'
 hFoldMap
@@ -174,7 +174,7 @@
   => (forall a. f a -> b)
   -> HTree f t
   -> b
-hFoldMap f t = withDict (allTopHTree t) $ hcFoldMap @Top f t
+hFoldMap f t = withDict (allTopHTree t) $ hcFoldMap Top f t
 
 -- | flatten a heterogeneous tree down to a heterogeneous list
 hFlatten
diff --git a/test/Spec/HTree/Fold.hs b/test/Spec/HTree/Fold.hs
--- a/test/Spec/HTree/Fold.hs
+++ b/test/Spec/HTree/Fold.hs
@@ -17,8 +17,8 @@
 spec :: Spec
 spec = do
   describe "folding an HTree of numbers" do
-    it "calculates the correct sum" (31649046316921651 % 281474976710656 == getSum (hcFoldMap @Real (Sum . toRational) exReal))
-    it "calculates the correct product" (308407698144 == getProduct (hcFoldMap @Integral (Product . toInteger) exIntegral))
+    it "calculates the correct sum" (31649046316921651 % 281474976710656 == getSum (hcFoldMap Real (Sum . toRational) exReal))
+    it "calculates the correct product" (308407698144 == getProduct (hcFoldMap Integral (Product . toInteger) exIntegral))
     modifyMaxSuccess (* 10) do
       prop "yields the same results as expected for many Lists" $
         foldsSameList @Identity
diff --git a/test/Spec/HTree/Labeled.hs b/test/Spec/HTree/Labeled.hs
--- a/test/Spec/HTree/Labeled.hs
+++ b/test/Spec/HTree/Labeled.hs
@@ -3,7 +3,7 @@
 
 module Spec.HTree.Labeled (spec) where
 
-import Data.HTree.Labeled (Proxy (Proxy), SearchStrategy (BFS, DFS), getElem)
+import Data.HTree.Labeled (SearchStrategy (BFS, DFS), getElem)
 import Spec.HTree.Fixtures (exBfsDfs, exL, unI)
 import Test.Hspec (Spec, describe, it)
 
@@ -20,6 +20,6 @@
   it "has e node \"test\"" do
     ("test" :: String) == unI exL.e
   it "finds int via BFS" do
-    unI (getElem @BFS @"foo" @Int Proxy exBfsDfs) == 67
+    unI (getElem BFS "foo" Int exBfsDfs) == 67
   it "finds int via DFS" do
-    unI (getElem @DFS @"foo" @Int Proxy exBfsDfs) == 69
+    unI (getElem DFS "foo" Int exBfsDfs) == 69
diff --git a/test/Spec/HTree/Traverse.hs b/test/Spec/HTree/Traverse.hs
--- a/test/Spec/HTree/Traverse.hs
+++ b/test/Spec/HTree/Traverse.hs
@@ -11,5 +11,5 @@
   describe "use hctraverse" $ do
     it "yields the same result as expected" $ do
       let traversed :: Maybe (HTree (Const String) Ex)
-          traversed = hctraverse @Show (Just . Const . show . unI) ex
+          traversed = hctraverse Show (Just . Const . show . unI) ex
       Just `traverse` exShown == (forgetHTree <$> traversed)