diff --git a/README.md b/README.md
index b4eddc1..ad1e0d9 100644
--- a/README.md
+++ b/README.md
@@ -83,24 +83,17 @@ This library just uses the same structural row system that we use with records
 We lift values into `Variant` with `inj` by specifying a _tag_.
 
 ```purescript
-import Type.Proxy (Proxy(..))
-
 someFoo :: forall v. Variant (foo :: Int | v)
-someFoo = inj (Proxy :: Proxy "foo") 42
+someFoo = inj @"foo" 42
 ```
 
 `Proxy` is just a way to tell the compiler what our tag is at the type level.
 I can stamp out a bunch of these with different labels:
 
 ```purescript
-someFoo :: forall v. Variant (foo :: Int | v)
-someFoo = inj (Proxy :: Proxy "foo") 42
-
-someBar :: forall v. Variant (bar :: Boolean | v)
-someBar = inj (Proxy :: Proxy "bar") true
-
-someBaz :: forall v. Variant (baz :: String | v)
-someBaz = inj (Proxy :: Proxy "baz") "Baz"
+someFoo = inj @"foo" 42
+someBar = inj @"bar" true
+someBaz = inj @"baz" "Baz"
 ```
 
 We can try to extract a value from this via `on`, which takes a function to
@@ -109,7 +102,7 @@ case of failure.
 
 ```purescript
 fooToString :: forall v. Variant (foo :: Int | v) -> String
-fooToString = on (Proxy :: Proxy "foo") show (\_ -> "not foo")
+fooToString = on @"foo" show (\_ -> "not foo")
 
 fooToString someFoo == "42"
 fooToString someBar == "not foo"
@@ -119,22 +112,18 @@ We can chain usages of `on` and terminate it with `case_` (for compiler-checked
 exhaustivity) or `default` (to provide a default value in case of failure).
 
 ```purescript
-_foo = Proxy :: Proxy "foo"
-_bar = Proxy :: Proxy "bar"
-_baz = Proxy :: Proxy "baz"
-
 allToString :: Variant (foo :: Int, bar :: Boolean, baz :: String) -> String
 allToString =
   case_
-    # on _foo show
-    # on _bar (if _ then "true" else "false")
-    # on _baz (\str -> str)
+    # on @"foo" show
+    # on @"bar" (if _ then "true" else "false")
+    # on @"baz" (\str -> str)
 
 someToString :: forall v. Variant (foo :: Int, bar :: Boolean | v) -> String
 someToString =
   default "unknown"
-    # on _foo show
-    # on _bar (if _ then "true" else "false")
+    # on @"foo" show
+    # on @"bar" (if _ then "true" else "false")
 
 allToString someBaz == "Baz"
 someToString someBaz == "unknown"
@@ -145,13 +134,13 @@ function composition and reuse them in different contexts.
 
 ```purescript
 onFooOrBar :: forall v. (Variant v -> String) -> Variant (foo :: Int, bar :: Boolean | v) -> String
-onFooOrBar = on _foo show >>> on _bar (if _ then "true" else "false")
+onFooOrBar = on @"foo" show >>> on @"bar" (if _ then "true" else "false")
 
 allToString :: Variant (foo :: Int, bar :: Boolean, baz :: String) -> String
 allToString =
   case_
     # onFooOrBar
-    # on _baz (\str -> str)
+    # on @"baz" (\str -> str)
 ```
 
 Instead of chaining with just `on`, there is `onMatch` which adds record sugar.
@@ -185,13 +174,13 @@ except it's indexed by things of kind `Type -> Type`.
 
 ```purescript
 someFoo :: forall v. VariantF (foo :: Maybe | v) Int
-someFoo = inj (Proxy :: Proxy "foo") (Just 42)
+someFoo = inj @"foo" (Just 42)
 
 someBar :: forall v. VariantF (bar :: Tuple String | v) Int
-someBar = inj (Proxy :: Proxy "bar") (Tuple "bar" 42)
+someBar = inj @"bar" (Tuple "bar" 42)
 
 someBaz :: forall v a. VariantF (baz :: Either String | v) a
-someBaz = inj (Proxy :: Proxy "baz") (Left "Baz")
+someBaz = inj @"baz" (Left "Baz")
 ```
 
 `VariantF` supports all the same combinators as `Variant`.
diff --git a/src/Data/Functor/Variant.purs b/src/Data/Functor/Variant.purs
index 705f6f1..92a49de 100644
--- a/src/Data/Functor/Variant.purs
+++ b/src/Data/Functor/Variant.purs
@@ -19,8 +19,11 @@ module Data.Functor.Variant
   , UnvariantF'
   , unvariantF
   , revariantF
-  , class VariantFShows, variantFShows
-  , class VariantFMaps, variantFMaps, Mapper
+  , class VariantFShows
+  , variantFShows
+  , class VariantFMaps
+  , variantFMaps
+  , Mapper
   , class TraversableVFRL
   , class FoldableVFRL
   , traverseVFRL
@@ -58,7 +61,7 @@ data UnknownF a
 data VariantF :: Row (Type -> Type) -> Type -> Type
 data VariantF f a
 
-instance functorVariantF ∷ Functor (VariantF r) where
+instance Functor (VariantF r) where
   map f a =
     case coerceY a of
       VariantFRep v → coerceV $ VariantFRep
@@ -79,54 +82,56 @@ class FoldableVFRL rl row | rl -> row where
   foldlVFRL :: forall a b. Proxy rl -> (b -> a -> b) -> b -> VariantF row a -> b
   foldMapVFRL :: forall a m. Monoid m => Proxy rl -> (a -> m) -> VariantF row a -> m
 
-instance foldableNil :: FoldableVFRL RL.Nil () where
+instance FoldableVFRL RL.Nil () where
   foldrVFRL _ _ _ = case_
   foldlVFRL _ _ _ = case_
   foldMapVFRL _ _ = case_
 
-instance foldableCons ::
+instance
   ( IsSymbol k
   , TF.Foldable f
   , FoldableVFRL rl r
   , R.Cons k f r r'
-  ) => FoldableVFRL (RL.Cons k f rl) r' where
-  foldrVFRL _ f b = on k (TF.foldr f b) (foldrVFRL (Proxy :: Proxy rl) f b)
-    where k = Proxy :: Proxy k
-  foldlVFRL _ f b = on k (TF.foldl f b) (foldlVFRL (Proxy :: Proxy rl) f b)
-    where k = Proxy :: Proxy k
-  foldMapVFRL _ f = on k (TF.foldMap f) (foldMapVFRL (Proxy :: Proxy rl) f)
-    where k = Proxy :: Proxy k
+  ) =>
+  FoldableVFRL (RL.Cons k f rl) r' where
+  foldrVFRL _ f b = on @k (TF.foldr f b) (foldrVFRL (Proxy :: Proxy rl) f b)
+  foldlVFRL _ f b = on @k (TF.foldl f b) (foldlVFRL (Proxy :: Proxy rl) f b)
+  foldMapVFRL _ f = on @k (TF.foldMap f) (foldMapVFRL (Proxy :: Proxy rl) f)
 
 class TraversableVFRL :: RL.RowList (Type -> Type) -> Row (Type -> Type) -> Constraint
 class FoldableVFRL rl row <= TraversableVFRL rl row | rl -> row where
   traverseVFRL :: forall f a b. Applicative f => Proxy rl -> (a -> f b) -> VariantF row a -> f (VariantF row b)
 
-instance traversableNil :: TraversableVFRL RL.Nil () where
+instance TraversableVFRL RL.Nil () where
   traverseVFRL _ _ = case_
 
-instance traversableCons ::
+instance
   ( IsSymbol k
   , TF.Traversable f
   , TraversableVFRL rl r
   , R.Cons k f r r'
   , R.Union r rx r'
-  ) => TraversableVFRL (RL.Cons k f rl) r' where
-  traverseVFRL _ f = on k (TF.traverse f >>> map (inj k))
+  ) =>
+  TraversableVFRL (RL.Cons k f rl) r' where
+  traverseVFRL _ f = on @k (TF.traverse f >>> map (inj @k))
     (traverseVFRL (Proxy :: Proxy rl) f >>> map expand)
-    where k = Proxy :: Proxy k
 
-instance foldableVariantF ::
-  (RL.RowToList row rl, FoldableVFRL rl row) =>
+instance
+  ( RL.RowToList row rl
+  , FoldableVFRL rl row
+  ) =>
   TF.Foldable (VariantF row) where
-    foldr = foldrVFRL (Proxy :: Proxy rl)
-    foldl = foldlVFRL (Proxy :: Proxy rl)
-    foldMap = foldMapVFRL (Proxy :: Proxy rl)
-
-instance traversableVariantF ::
-  (RL.RowToList row rl, TraversableVFRL rl row) =>
+  foldr = foldrVFRL (Proxy :: Proxy rl)
+  foldl = foldlVFRL (Proxy :: Proxy rl)
+  foldMap = foldMapVFRL (Proxy :: Proxy rl)
+
+instance
+  ( RL.RowToList row rl
+  , TraversableVFRL rl row
+  ) =>
   TF.Traversable (VariantF row) where
-    traverse = traverseVFRL (Proxy :: Proxy rl)
-    sequence = TF.sequenceDefault
+  traverse = traverseVFRL (Proxy :: Proxy rl)
+  sequence = TF.sequenceDefault
 
 -- | Inject into the variant at a given label.
 -- | ```purescript
@@ -134,14 +139,13 @@ instance traversableVariantF ::
 -- | maybeAtFoo = inj (Proxy :: Proxy "foo") (Just 42)
 -- | ```
 inj
-  ∷ ∀ sym f a r1 r2
+  ∷ ∀ @sym f a r1 r2
   . R.Cons sym f r1 r2
   ⇒ IsSymbol sym
   ⇒ Functor f
-  ⇒ Proxy sym
-  → f a
+  ⇒ f a
   → VariantF r2 a
-inj p value = coerceV $ VariantFRep { type: reflectSymbol p, value, map: Mapper map }
+inj value = coerceV $ VariantFRep { type: reflectSymbol (Proxy :: Proxy sym), value, map: Mapper map }
   where
   coerceV ∷ VariantFRep f a → VariantF r2 a
   coerceV = unsafeCoerce
@@ -153,30 +157,28 @@ inj p value = coerceV $ VariantFRep { type: reflectSymbol p, value, map: Mapper
 -- |   _ -> 0
 -- | ```
 prj
-  ∷ ∀ sym f a r1 r2 g
+  ∷ ∀ @sym f a r1 r2 g
   . R.Cons sym f r1 r2
   ⇒ Alternative g
   ⇒ IsSymbol sym
-  ⇒ Proxy sym
-  → VariantF r2 a
+  ⇒ VariantF r2 a
   → g (f a)
-prj p = on p pure (const empty)
+prj = on @sym pure (const empty)
 
 -- | Attempt to read a variant at a given label by providing branches.
 -- | The failure branch receives the provided variant, but with the label
 -- | removed.
 on
-  ∷ ∀ sym f a b r1 r2
+  ∷ ∀ @sym f a b r1 r2
   . R.Cons sym f r1 r2
   ⇒ IsSymbol sym
-  ⇒ Proxy sym
-  → (f a → b)
+  ⇒ (f a → b)
   → (VariantF r1 a → b)
   → VariantF r2 a
   → b
-on p f g r =
+on f g r =
   case coerceY r of
-    VariantFRep v | v.type == reflectSymbol p → f v.value
+    VariantFRep v | v.type == reflectSymbol (Proxy :: Proxy sym) → f v.value
     _ → g (coerceR r)
   where
   coerceY ∷ VariantF r2 a → VariantFRep f a
@@ -230,12 +232,11 @@ overOne
   ⇒ R.Cons sym g r4 r3
   ⇒ IsSymbol sym
   ⇒ Functor g
-  ⇒ Proxy sym
-  → (f a → g b)
+  ⇒ (f a → g b)
   → (VariantF r1 a → VariantF r3 b)
   → VariantF r2 a
   → VariantF r3 b
-overOne p f = on p (inj p <<< f)
+overOne f = on @sym (inj @sym <<< f)
 
 -- | Map over several cases of a variant using a `Record` containing functions
 -- | for each case. Each case gets put back at the same label it was matched
@@ -261,7 +262,8 @@ overSome r k v =
         tags = variantTags (Proxy ∷ Proxy rlo)
         maps = variantFMaps (Proxy ∷ Proxy rlo)
         map = lookup "map" v'.type tags maps
-      in coerceV' (VariantFRep { type: v'.type, map, value: unsafeGet v'.type r v'.value })
+      in
+        coerceV' (VariantFRep { type: v'.type, map, value: unsafeGet v'.type r v'.value })
     _ → k (coerceR v)
 
   where
@@ -300,7 +302,8 @@ over
   → (a → b)
   → VariantF r1 a
   → VariantF r3 b
-over r f = overSome r (map f >>> unsafeExpand) where
+over r f = overSome r (map f >>> unsafeExpand)
+  where
   unsafeExpand = unsafeCoerce ∷ VariantF r2 b → VariantF r3 b
 
 -- | Traverse over one case of a variant (in a functorial/monadic context `m`),
@@ -312,12 +315,11 @@ traverseOne
   ⇒ IsSymbol sym
   ⇒ Functor g
   ⇒ Functor m
-  ⇒ Proxy sym
-  → (f a → m (g b))
+  ⇒ (f a → m (g b))
   → (VariantF r1 a → m (VariantF r3 b))
   → VariantF r2 a
   → m (VariantF r3 b)
-traverseOne p f = on p (map (inj p) <<< f)
+traverseOne f = on @sym (map (inj @sym) <<< f)
 
 -- | Traverse over several cases of a variant using a `Record` containing
 -- | traversals. Each case gets put back at the same label it was matched
@@ -344,7 +346,8 @@ traverseSome r k v =
         tags = variantTags (Proxy ∷ Proxy rlo)
         maps = variantFMaps (Proxy ∷ Proxy rlo)
         map = lookup "map" v'.type tags maps
-      in unsafeGet v'.type r v'.value <#> \value ->
+      in
+        unsafeGet v'.type r v'.value <#> \value ->
           coerceV' (VariantFRep { type: v'.type, map, value })
     _ → k (coerceR v)
 
@@ -379,7 +382,8 @@ traverse
   → (a → m b)
   → VariantF r1 a
   → m (VariantF r3 b)
-traverse r f = traverseSome r (TF.traverse f >>> map unsafeExpand) where
+traverse r f = traverseSome r (TF.traverse f >>> map unsafeExpand)
+  where
   unsafeExpand = unsafeCoerce ∷ VariantF r2 b → VariantF r3 b
 
 -- | Combinator for exhaustive pattern matching.
@@ -496,23 +500,26 @@ unvariantF v = case (unsafeCoerce v ∷ VariantFRep UnknownF Unit) of
 
 -- | Reconstructs a VariantF given an UnvariantF eliminator.
 revariantF ∷ ∀ r a. UnvariantF r a -> VariantF r a
-revariantF (UnvariantF f) = f inj
+revariantF (UnvariantF f) = f inj'
+  where
+  inj' ∷ ∀ @sym f r1 r2. R.Cons sym f r1 r2 ⇒ IsSymbol sym ⇒ Functor f ⇒ Proxy sym -> f a → VariantF r2 a
+  inj' _ = inj @sym
 
 class VariantFShows :: RL.RowList (Type -> Type) -> Type -> Constraint
 class VariantFShows rl x where
-  variantFShows ∷ forall proxy1 proxy2. proxy1 rl → proxy2 x → L.List (VariantCase → String)
+  variantFShows ∷ Proxy rl → Proxy x → L.List (VariantCase → String)
 
-instance showVariantFNil ∷ VariantFShows RL.Nil x where
+instance VariantFShows RL.Nil x where
   variantFShows _ _ = L.Nil
 
-instance showVariantFCons ∷ (VariantFShows rs x, Show (f x), Show x) ⇒ VariantFShows (RL.Cons sym f rs) x where
+instance (VariantFShows rs x, Show (f x), Show x) ⇒ VariantFShows (RL.Cons sym f rs) x where
   variantFShows _ p =
     L.Cons (coerceShow show) (variantFShows (Proxy ∷ Proxy rs) p)
     where
     coerceShow ∷ (f x → String) → VariantCase → String
     coerceShow = unsafeCoerce
 
-instance showVariantF ∷ (RL.RowToList r rl, VariantTags rl, VariantFShows rl a, Show a) ⇒ Show (VariantF r a) where
+instance (RL.RowToList r rl, VariantTags rl, VariantFShows rl a, Show a) ⇒ Show (VariantF r a) where
   show v1 =
     let
       VariantFRep v = unsafeCoerce v1 ∷ VariantFRep VariantFCase a
@@ -525,10 +532,10 @@ instance showVariantF ∷ (RL.RowToList r rl, VariantTags rl, VariantFShows rl a
 class VariantFMaps (rl ∷ RL.RowList (Type → Type)) where
   variantFMaps ∷ Proxy rl → L.List (Mapper VariantFCase)
 
-instance mapVariantFNil ∷ VariantFMaps RL.Nil where
+instance VariantFMaps RL.Nil where
   variantFMaps _ = L.Nil
 
-instance mapVariantFCons ∷ (VariantFMaps rs, Functor f) ⇒ VariantFMaps (RL.Cons sym f rs) where
+instance (VariantFMaps rs, Functor f) ⇒ VariantFMaps (RL.Cons sym f rs) where
   variantFMaps _ =
     L.Cons (coerceMap (Mapper map)) (variantFMaps (Proxy ∷ Proxy rs))
     where
diff --git a/src/Data/Variant.purs b/src/Data/Variant.purs
index b59e44f..e0e7826 100644
--- a/src/Data/Variant.purs
+++ b/src/Data/Variant.purs
@@ -19,11 +19,16 @@ module Data.Variant
   , Unvariant'
   , unvariant
   , revariant
-  , class VariantEqs, variantEqs
-  , class VariantOrds, variantOrds
-  , class VariantShows, variantShows
-  , class VariantBounded, variantBounded
-  , class VariantBoundedEnums, variantBoundedEnums
+  , class VariantEqs
+  , variantEqs
+  , class VariantOrds
+  , variantOrds
+  , class VariantShows
+  , variantShows
+  , class VariantBounded
+  , variantBounded
+  , class VariantBoundedEnums
+  , variantBoundedEnums
   , module Exports
   ) where
 
@@ -34,8 +39,8 @@ import Data.Enum (class Enum, pred, succ, class BoundedEnum, Cardinality(..), fr
 import Data.List as L
 import Data.Maybe (Maybe)
 import Data.Symbol (class IsSymbol, reflectSymbol)
-import Data.Variant.Internal (class Contractable, class VariantMapCases, class VariantMatchCases, class VariantTraverseCases) as Exports
 import Data.Variant.Internal (class Contractable, class VariantMapCases, class VariantMatchCases, class VariantTags, class VariantTraverseCases, BoundedDict, BoundedEnumDict, VariantCase, VariantRep(..), contractWith, lookup, lookupCardinality, lookupEq, lookupFirst, lookupFromEnum, lookupLast, lookupOrd, lookupPred, lookupSucc, lookupToEnum, unsafeGet, unsafeHas, variantTags)
+import Data.Variant.Internal (class Contractable, class VariantMapCases, class VariantMatchCases, class VariantTraverseCases) as Exports
 import Partial.Unsafe (unsafeCrashWith)
 import Prim.Row as R
 import Prim.RowList as RL
@@ -50,13 +55,12 @@ foreign import data Variant ∷ Row Type → Type
 -- | intAtFoo = inj (Proxy :: Proxy "foo") 42
 -- | ```
 inj
-  ∷ ∀ sym a r1 r2
+  ∷ ∀ @sym a r1 r2
   . R.Cons sym a r1 r2
   ⇒ IsSymbol sym
-  ⇒ Proxy sym
-  → a
+  ⇒ a
   → Variant r2
-inj p value = coerceV $ VariantRep { type: reflectSymbol p, value }
+inj value = coerceV $ VariantRep { type: reflectSymbol (Proxy :: Proxy sym), value }
   where
   coerceV ∷ VariantRep a → Variant r2
   coerceV = unsafeCoerce
@@ -68,30 +72,28 @@ inj p value = coerceV $ VariantRep { type: reflectSymbol p, value }
 -- |   Nothing -> 0
 -- | ```
 prj
-  ∷ ∀ sym a r1 r2 f
+  ∷ ∀ @sym a r1 r2 f
   . R.Cons sym a r1 r2
   ⇒ IsSymbol sym
   ⇒ Alternative f
-  ⇒ Proxy sym
-  → Variant r2
+  ⇒ Variant r2
   → f a
-prj p = on p pure (const empty)
+prj = on @sym pure (const empty)
 
 -- | Attempt to read a variant at a given label by providing branches.
 -- | The failure branch receives the provided variant, but with the label
 -- | removed.
 on
-  ∷ ∀ sym a b r1 r2
+  ∷ ∀ @sym a b r1 r2
   . R.Cons sym a r1 r2
   ⇒ IsSymbol sym
-  ⇒ Proxy sym
-  → (a → b)
+  ⇒ (a → b)
   → (Variant r1 → b)
   → Variant r2
   → b
-on p f g r =
+on f g r =
   case coerceV r of
-    VariantRep v | v.type == reflectSymbol p → f v.value
+    VariantRep v | v.type == reflectSymbol (Proxy :: Proxy sym) → f v.value
     _ → g (coerceR r)
   where
   coerceV ∷ Variant r2 → VariantRep a
@@ -140,16 +142,15 @@ onMatch r k v =
 -- | Map over one case of a variant, putting the result back at the same label,
 -- | with a fallback function to handle the remaining cases.
 overOne
-  ∷ ∀ sym a b r1 r2 r3 r4
+  ∷ ∀ @sym a b r1 r2 r3 r4
   . IsSymbol sym
   ⇒ R.Cons sym a r1 r2
   ⇒ R.Cons sym b r4 r3
-  ⇒ Proxy sym
-  → (a → b)
+  ⇒ (a → b)
   → (Variant r1 → Variant r3)
   → Variant r2
   → Variant r3
-overOne p f = on p (inj p <<< f)
+overOne f = on @sym (inj @sym <<< f)
 
 -- | Map over several cases of a variant using a `Record` containing functions
 -- | for each case. Each case gets put back at the same label it was matched
@@ -199,7 +200,8 @@ over
   ⇒ Record r
   → Variant r1
   → Variant r3
-over r = overSome r unsafeExpand where
+over r = overSome r unsafeExpand
+  where
   unsafeExpand = unsafeCoerce ∷ Variant r2 → Variant r3
 
 -- | Traverse over one case of a variant (in a functorial/monadic context `m`),
@@ -210,12 +212,11 @@ traverseOne
   ⇒ R.Cons sym a r1 r2
   ⇒ R.Cons sym b r4 r3
   ⇒ Functor m
-  ⇒ Proxy sym
-  → (a → m b)
+  ⇒ (a → m b)
   → (Variant r1 → m (Variant r3))
   → Variant r2
   → m (Variant r3)
-traverseOne p f = on p (map (inj p) <<< f)
+traverseOne f = on @sym (map (inj @sym) <<< f)
 
 -- | Traverse over several cases of a variant using a `Record` containing
 -- | traversals. Each case gets put back at the same label it was matched
@@ -261,7 +262,8 @@ traverse
   ⇒ Record r
   → Variant r1
   → m (Variant r3)
-traverse r = traverseSome r (pure <<< unsafeExpand) where
+traverse r = traverseSome r (pure <<< unsafeExpand)
+  where
   unsafeExpand = unsafeCoerce ∷ Variant r2 → Variant r3
 
 -- | Combinator for exhaustive pattern matching.
@@ -371,23 +373,26 @@ unvariant v = case (unsafeCoerce v ∷ VariantRep Unit) of
 
 -- | Reconstructs a Variant given an Unvariant eliminator.
 revariant ∷ ∀ r. Unvariant r -> Variant r
-revariant (Unvariant f) = f inj
+revariant (Unvariant f) = f inj'
+  where
+  inj' :: ∀ @sym a r1 r2. R.Cons sym a r1 r2 ⇒ IsSymbol sym ⇒ Proxy sym → a → Variant r2
+  inj' _ = inj @sym
 
 class VariantEqs :: RL.RowList Type -> Constraint
 class VariantEqs rl where
   variantEqs ∷ Proxy rl → L.List (VariantCase → VariantCase → Boolean)
 
-instance eqVariantNil ∷ VariantEqs RL.Nil where
+instance VariantEqs RL.Nil where
   variantEqs _ = L.Nil
 
-instance eqVariantCons ∷ (VariantEqs rs, Eq a) ⇒ VariantEqs (RL.Cons sym a rs) where
+instance (VariantEqs rs, Eq a) ⇒ VariantEqs (RL.Cons sym a rs) where
   variantEqs _ =
     L.Cons (coerceEq eq) (variantEqs (Proxy ∷ Proxy rs))
     where
     coerceEq ∷ (a → a → Boolean) → VariantCase → VariantCase → Boolean
     coerceEq = unsafeCoerce
 
-instance eqVariant ∷ (RL.RowToList r rl, VariantTags rl, VariantEqs rl) ⇒ Eq (Variant r) where
+instance (RL.RowToList r rl, VariantTags rl, VariantEqs rl) ⇒ Eq (Variant r) where
   eq v1 v2 =
     let
       c1 = unsafeCoerce v1 ∷ VariantRep VariantCase
@@ -401,10 +406,10 @@ class VariantBounded :: RL.RowList Type -> Constraint
 class VariantBounded rl where
   variantBounded ∷ Proxy rl → L.List (BoundedDict VariantCase)
 
-instance boundedVariantNil ∷ VariantBounded RL.Nil where
+instance VariantBounded RL.Nil where
   variantBounded _ = L.Nil
 
-instance boundedVariantCons ∷ (VariantBounded rs, Bounded a) ⇒ VariantBounded (RL.Cons sym a rs) where
+instance (VariantBounded rs, Bounded a) ⇒ VariantBounded (RL.Cons sym a rs) where
   variantBounded _ = L.Cons dict (variantBounded (Proxy ∷ Proxy rs))
     where
     dict ∷ BoundedDict VariantCase
@@ -416,7 +421,7 @@ instance boundedVariantCons ∷ (VariantBounded rs, Bounded a) ⇒ VariantBounde
     coerce ∷ a → VariantCase
     coerce = unsafeCoerce
 
-instance boundedVariant ∷ (RL.RowToList r rl, VariantTags rl, VariantEqs rl, VariantOrds rl, VariantBounded rl) ⇒ Bounded (Variant r) where
+instance (RL.RowToList r rl, VariantTags rl, VariantEqs rl, VariantOrds rl, VariantBounded rl) ⇒ Bounded (Variant r) where
   top =
     let
       tags = variantTags (Proxy ∷ Proxy rl)
@@ -437,10 +442,10 @@ class VariantBoundedEnums :: RL.RowList Type -> Constraint
 class VariantBounded rl ⇐ VariantBoundedEnums rl where
   variantBoundedEnums ∷ Proxy rl → L.List (BoundedEnumDict VariantCase)
 
-instance enumVariantNil ∷ VariantBoundedEnums RL.Nil where
+instance VariantBoundedEnums RL.Nil where
   variantBoundedEnums _ = L.Nil
 
-instance enumVariantCons ∷ (VariantBoundedEnums rs, BoundedEnum a) ⇒ VariantBoundedEnums (RL.Cons sym a rs) where
+instance (VariantBoundedEnums rs, BoundedEnum a) ⇒ VariantBoundedEnums (RL.Cons sym a rs) where
   variantBoundedEnums _ = L.Cons dict (variantBoundedEnums (Proxy ∷ Proxy rs))
     where
     dict ∷ BoundedEnumDict VariantCase
@@ -464,7 +469,7 @@ instance enumVariantCons ∷ (VariantBoundedEnums rs, BoundedEnum a) ⇒ Variant
     coerceCardinality ∷ Cardinality a → Int
     coerceCardinality = unsafeCoerce
 
-instance enumVariant ∷ (RL.RowToList r rl, VariantTags rl, VariantEqs rl, VariantOrds rl, VariantBoundedEnums rl) ⇒ Enum (Variant r) where
+instance (RL.RowToList r rl, VariantTags rl, VariantEqs rl, VariantOrds rl, VariantBoundedEnums rl) ⇒ Enum (Variant r) where
   pred a =
     let
       rep = unsafeCoerce a ∷ VariantRep VariantCase
@@ -485,7 +490,7 @@ instance enumVariant ∷ (RL.RowToList r rl, VariantTags rl, VariantEqs rl, Vari
     in
       coerce $ lookupSucc rep tags bounds dicts
 
-instance boundedEnumVariant ∷ (RL.RowToList r rl, VariantTags rl, VariantEqs rl, VariantOrds rl, VariantBoundedEnums rl) ⇒ BoundedEnum (Variant r) where
+instance (RL.RowToList r rl, VariantTags rl, VariantEqs rl, VariantOrds rl, VariantBoundedEnums rl) ⇒ BoundedEnum (Variant r) where
   cardinality =
     Cardinality $ lookupCardinality $ variantBoundedEnums (Proxy ∷ Proxy rl)
 
@@ -509,17 +514,17 @@ class VariantOrds :: RL.RowList Type -> Constraint
 class VariantOrds rl where
   variantOrds ∷ Proxy rl → L.List (VariantCase → VariantCase → Ordering)
 
-instance ordVariantNil ∷ VariantOrds RL.Nil where
+instance VariantOrds RL.Nil where
   variantOrds _ = L.Nil
 
-instance ordVariantCons ∷ (VariantOrds rs, Ord a) ⇒ VariantOrds (RL.Cons sym a rs) where
+instance (VariantOrds rs, Ord a) ⇒ VariantOrds (RL.Cons sym a rs) where
   variantOrds _ =
     L.Cons (coerceOrd compare) (variantOrds (Proxy ∷ Proxy rs))
     where
     coerceOrd ∷ (a → a → Ordering) → VariantCase → VariantCase → Ordering
     coerceOrd = unsafeCoerce
 
-instance ordVariant ∷ (RL.RowToList r rl, VariantTags rl, VariantEqs rl, VariantOrds rl) ⇒ Ord (Variant r) where
+instance (RL.RowToList r rl, VariantTags rl, VariantEqs rl, VariantOrds rl) ⇒ Ord (Variant r) where
   compare v1 v2 =
     let
       c1 = unsafeCoerce v1 ∷ VariantRep VariantCase
@@ -533,17 +538,17 @@ class VariantShows :: RL.RowList Type -> Constraint
 class VariantShows rl where
   variantShows ∷ Proxy rl → L.List (VariantCase → String)
 
-instance showVariantNil ∷ VariantShows RL.Nil where
+instance VariantShows RL.Nil where
   variantShows _ = L.Nil
 
-instance showVariantCons ∷ (VariantShows rs, Show a) ⇒ VariantShows (RL.Cons sym a rs) where
+instance (VariantShows rs, Show a) ⇒ VariantShows (RL.Cons sym a rs) where
   variantShows _ =
     L.Cons (coerceShow show) (variantShows (Proxy ∷ Proxy rs))
     where
     coerceShow ∷ (a → String) → VariantCase → String
     coerceShow = unsafeCoerce
 
-instance showVariant ∷ (RL.RowToList r rl, VariantTags rl, VariantShows rl) ⇒ Show (Variant r) where
+instance (RL.RowToList r rl, VariantTags rl, VariantShows rl) ⇒ Show (Variant r) where
   show v1 =
     let
       VariantRep v = unsafeCoerce v1 ∷ VariantRep VariantCase
diff --git a/src/Data/Variant/Internal.purs b/src/Data/Variant/Internal.purs
index 83d70cf..45f4afa 100644
--- a/src/Data/Variant/Internal.purs
+++ b/src/Data/Variant/Internal.purs
@@ -2,8 +2,10 @@ module Data.Variant.Internal
   ( VariantRep(..)
   , VariantCase
   , VariantFCase
-  , class VariantTags, variantTags
-  , class Contractable, contractWith
+  , class VariantTags
+  , variantTags
+  , class Contractable
+  , contractWith
   , class VariantMatchCases
   , class VariantFMatchCases
   , class VariantMapCases
@@ -49,88 +51,100 @@ newtype VariantRep a = VariantRep
 class VariantMatchCases :: RL.RowList Type -> Row Type -> Type -> Constraint
 class VariantMatchCases rl vo b | rl → vo b
 
-instance variantMatchCons
-  ∷ ( VariantMatchCases rl vo' b
-    , R.Cons sym a vo' vo
-    , TypeEquals k (a → b)
-    )
-  ⇒ VariantMatchCases (RL.Cons sym k rl) vo b
+instance
+  ( VariantMatchCases rl vo' b
+  , R.Cons sym a vo' vo
+  , TypeEquals k (a → b)
+  ) ⇒
+  VariantMatchCases (RL.Cons sym k rl) vo b
 
-instance variantMatchNil
-  ∷ VariantMatchCases RL.Nil () b
+instance VariantMatchCases RL.Nil () b
 
 class VariantFMatchCases :: RL.RowList Type -> Row (Type -> Type) -> Type -> Type -> Constraint
 class VariantFMatchCases rl vo a b | rl → vo a b
 
-instance variantFMatchCons
-  ∷ ( VariantFMatchCases rl vo' a b
-    , R.Cons sym f vo' vo
-    , TypeEquals k (f a → b)
-    )
-  ⇒ VariantFMatchCases (RL.Cons sym k rl) vo a b
+instance
+  ( VariantFMatchCases rl vo' a b
+  , R.Cons sym f vo' vo
+  , TypeEquals k (f a → b)
+  ) ⇒
+  VariantFMatchCases (RL.Cons sym k rl) vo a b
 
-instance variantFMatchNil
-  ∷ VariantFMatchCases RL.Nil () a b
+instance VariantFMatchCases RL.Nil () a b
 
-class VariantMapCases (rl ∷ RL.RowList Type)
-  (ri ∷ Row Type) (ro ∷ Row Type)
+class
+  VariantMapCases
+    (rl ∷ RL.RowList Type)
+    (ri ∷ Row Type)
+    (ro ∷ Row Type)
   | rl → ri ro
 
-instance variantMapCons
-  ∷ ( R.Cons sym a ri' ri
-    , R.Cons sym b ro' ro
-    , VariantMapCases rl ri' ro'
-    , TypeEquals k (a → b)
-    )
-  ⇒ VariantMapCases (RL.Cons sym k rl) ri ro
-
-instance variantMapNil
-  ∷ VariantMapCases RL.Nil () ()
-
-class VariantFMapCases (rl ∷ RL.RowList Type)
-  (ri ∷ Row (Type → Type)) (ro ∷ Row (Type → Type)) (a ∷ Type) (b ∷ Type)
+instance
+  ( R.Cons sym a ri' ri
+  , R.Cons sym b ro' ro
+  , VariantMapCases rl ri' ro'
+  , TypeEquals k (a → b)
+  ) ⇒
+  VariantMapCases (RL.Cons sym k rl) ri ro
+
+instance VariantMapCases RL.Nil () ()
+
+class
+  VariantFMapCases
+    (rl ∷ RL.RowList Type)
+    (ri ∷ Row (Type → Type))
+    (ro ∷ Row (Type → Type))
+    (a ∷ Type)
+    (b ∷ Type)
   | rl → ri ro
 
-instance variantFMapCons
-  ∷ ( R.Cons sym f ri' ri
-    , R.Cons sym g ro' ro
-    , VariantFMapCases rl ri' ro' a b
-    , TypeEquals k (f a → g b)
-    )
-  ⇒ VariantFMapCases (RL.Cons sym k rl) ri ro a b
-
-instance variantFMapNil
-  ∷ VariantFMapCases RL.Nil () () a b
-
-class VariantTraverseCases (m ∷ Type → Type) (rl ∷ RL.RowList Type)
-  (ri ∷ Row Type) (ro ∷ Row Type)
+instance
+  ( R.Cons sym f ri' ri
+  , R.Cons sym g ro' ro
+  , VariantFMapCases rl ri' ro' a b
+  , TypeEquals k (f a → g b)
+  ) ⇒
+  VariantFMapCases (RL.Cons sym k rl) ri ro a b
+
+instance VariantFMapCases RL.Nil () () a b
+
+class
+  VariantTraverseCases
+    (m ∷ Type → Type)
+    (rl ∷ RL.RowList Type)
+    (ri ∷ Row Type)
+    (ro ∷ Row Type)
   | rl → ri ro
 
-instance variantTravCons
-  ∷ ( R.Cons sym a ri' ri
-    , R.Cons sym b ro' ro
-    , VariantTraverseCases m rl ri' ro'
-    , TypeEquals k (a → m b)
-    )
-  ⇒ VariantTraverseCases m (RL.Cons sym k rl) ri ro
-
-instance variantTravNil
-  ∷ VariantTraverseCases m RL.Nil () ()
-
-class VariantFTraverseCases (m ∷ Type → Type) (rl ∷ RL.RowList Type)
-  (ri ∷ Row (Type → Type)) (ro ∷ Row (Type → Type)) (a ∷ Type) (b ∷ Type)
+instance
+  ( R.Cons sym a ri' ri
+  , R.Cons sym b ro' ro
+  , VariantTraverseCases m rl ri' ro'
+  , TypeEquals k (a → m b)
+  ) ⇒
+  VariantTraverseCases m (RL.Cons sym k rl) ri ro
+
+instance VariantTraverseCases m RL.Nil () ()
+
+class
+  VariantFTraverseCases
+    (m ∷ Type → Type)
+    (rl ∷ RL.RowList Type)
+    (ri ∷ Row (Type → Type))
+    (ro ∷ Row (Type → Type))
+    (a ∷ Type)
+    (b ∷ Type)
   | rl → ri ro
 
-instance variantFTravCons
-  ∷ ( R.Cons sym f ri' ri
-    , R.Cons sym g ro' ro
-    , VariantFTraverseCases m rl ri' ro' a b
-    , TypeEquals k (f a → m (g b))
-    )
-  ⇒ VariantFTraverseCases m (RL.Cons sym k rl) ri ro a b
+instance
+  ( R.Cons sym f ri' ri
+  , R.Cons sym g ro' ro
+  , VariantFTraverseCases m rl ri' ro' a b
+  , TypeEquals k (f a → m (g b))
+  ) ⇒
+  VariantFTraverseCases m (RL.Cons sym k rl) ri ro a b
 
-instance variantFTravNil
-  ∷ VariantFTraverseCases m RL.Nil () () a b
+instance VariantFTraverseCases m RL.Nil () () a b
 
 foreign import data VariantCase ∷ Type
 
@@ -140,10 +154,10 @@ class VariantTags :: forall k. RL.RowList k -> Constraint
 class VariantTags rl where
   variantTags ∷ Proxy rl → L.List String
 
-instance variantTagsNil ∷ VariantTags RL.Nil where
+instance VariantTags RL.Nil where
   variantTags _ = L.Nil
 
-instance variantTagsCons ∷ (VariantTags rs, IsSymbol sym) ⇒ VariantTags (RL.Cons sym a rs) where
+instance (VariantTags rs, IsSymbol sym) ⇒ VariantTags (RL.Cons sym a rs) where
   variantTags _ = L.Cons (reflectSymbol (Proxy ∷ Proxy sym)) (variantTags (Proxy ∷ Proxy rs))
 
 -- | A specialized lookup function which bails early. Foldable's `elem`
@@ -234,7 +248,7 @@ lookupPred (VariantRep rep) = go1
       | t1 == rep.type →
           case d1.pred rep.value of
             Nothing → Nothing
-            Just z  → Just $ VariantRep { type: rep.type, value: z }
+            Just z → Just $ VariantRep { type: rep.type, value: z }
       | otherwise → go2 t1 b1 d1 ts1 bs1 ds1
     _, _, _ → impossible "pred"
 
@@ -243,7 +257,7 @@ lookupPred (VariantRep rep) = go1
       | t2 == rep.type →
           case d2.pred rep.value of
             Nothing → Just $ VariantRep { type: t1, value: b1.top }
-            Just z  → Just $ VariantRep { type: rep.type, value: z }
+            Just z → Just $ VariantRep { type: rep.type, value: z }
       | otherwise → go2 t2 b2 d2 ts2 bs2 ds2
     _, _, _ → impossible "pred"
 
@@ -260,7 +274,7 @@ lookupSucc (VariantRep rep) = go
     L.Cons t1 ts1, L.Cons _ bs1, L.Cons d1 ds1
       | t1 == rep.type →
           case d1.succ rep.value of
-            Just z  → Just $ VariantRep { type: t1, value: z }
+            Just z → Just $ VariantRep { type: t1, value: z }
             Nothing → case ts1, bs1 of
               L.Cons t2 _, L.Cons b2 _ → Just $ VariantRep { type: t2, value: b2.bottom }
               _, _ → Nothing
@@ -312,12 +326,12 @@ class Contractable :: forall k. Row k -> Row k -> Constraint
 class Contractable gt lt where
   contractWith ∷ ∀ proxy1 proxy2 f a. Alternative f ⇒ proxy1 gt → proxy2 lt → String → a → f a
 
-instance contractWithInstance
-  ∷ ( RL.RowToList lt ltl
-    , R.Union lt a gt
-    , VariantTags ltl
-    )
-  ⇒ Contractable gt lt
+instance
+  ( RL.RowToList lt ltl
+  , R.Union lt a gt
+  , VariantTags ltl
+  ) ⇒
+  Contractable gt lt
   where
   contractWith _ _ tag a
     | lookupTag tag (variantTags (Proxy ∷ Proxy ltl)) = pure a
diff --git a/test/Variant.purs b/test/Variant.purs
index 0f52825..b283771 100644
--- a/test/Variant.purs
+++ b/test/Variant.purs
@@ -9,7 +9,6 @@ import Data.Variant (Variant, on, onMatch, case_, default, expand, inj, prj, mat
 import Effect (Effect)
 import Record.Builder (build, modify, Builder)
 import Test.Assert (assert')
-import Type.Proxy (Proxy(..))
 
 type TestVariants =
   ( foo ∷ Int
@@ -23,23 +22,14 @@ type TestVariants' =
   , baz ∷ String
   )
 
-_foo ∷ Proxy "foo"
-_foo = Proxy
-
-_bar ∷ Proxy "bar"
-_bar = Proxy
-
-_baz ∷ Proxy "baz"
-_baz = Proxy
-
 foo ∷ ∀ r. Variant (foo ∷ Int | r)
-foo = inj _foo 42
+foo = inj @"foo" 42
 
 bar ∷ ∀ r. Variant (bar ∷ String | r)
-bar = inj _bar "bar"
+bar = inj @"bar" "bar"
 
 baz ∷ ∀ r. Variant (baz ∷ Boolean | r)
-baz = inj _baz true
+baz = inj @"baz" true
 
 modifyRec ∷ Builder (Record TestVariants) (Record TestVariants)
 modifyRec = setVariant foo >>> setVariant bar >>> setVariant baz
@@ -61,15 +51,15 @@ recAfter = build modifyRec recBefore
 
 test ∷ Effect Unit
 test = do
-  assert' "prj: Foo" $ prj _foo foo == Just 42
-  assert' "prj: !Foo" $ prj _foo bar == (Nothing ∷ Maybe Int)
+  assert' "prj: Foo" $ prj @"foo" foo == Just 42
+  assert' "prj: !Foo" $ prj @"foo" bar == (Nothing ∷ Maybe Int)
 
   let
     case1 ∷ Variant TestVariants → String
     case1 = case_
-      # on _foo (\a → "foo: " <> show a)
-      # on _bar (\a → "bar: " <> a)
-      # on _baz (\a → "baz: " <> show a)
+      # on @"foo" (\a → "foo: " <> show a)
+      # on @"bar" (\a → "bar: " <> a)
+      # on @"baz" (\a → "baz: " <> show a)
 
   assert' "case1: foo" $ case1 foo == "foo: 42"
   assert' "case1: bar" $ case1 bar == "bar: bar"
@@ -78,8 +68,8 @@ test = do
   let
     case2 ∷ Variant TestVariants → String
     case2 = default "no match"
-      # on _foo (\a → "foo: " <> show a)
-      # on _bar (\a → "bar: " <> a)
+      # on @"foo" (\a → "foo: " <> show a)
+      # on @"bar" (\a → "bar: " <> a)
 
   assert' "case2: foo" $ case2 foo == "foo: 42"
   assert' "case2: bar" $ case2 bar == "bar: bar"
@@ -102,11 +92,13 @@ test = do
     overSome' = overSome
       { foo: \a → show a
       , baz: \a → show a
-      } expand
+      }
+      expand
 
-    over' ∷ forall r.
-      Variant ( foo ∷ Int, baz ∷ Boolean | r ) →
-      Variant ( foo ∷ String, baz ∷ String | r )
+    over'
+      ∷ forall r
+       . Variant (foo ∷ Int, baz ∷ Boolean | r)
+      → Variant (foo ∷ String, baz ∷ String | r)
     over' = over
       { foo: \a → show a
       , baz: \a → show a
@@ -115,12 +107,12 @@ test = do
     onMatch' ∷ Variant TestVariants' → String
     onMatch' = case_
       # onMatch
-        { foo: \a → "foo: " <> a
-        , bar: \a → "bar: " <> a
-        }
+          { foo: \a → "foo: " <> a
+          , bar: \a → "bar: " <> a
+          }
       # onMatch
-        { baz: \a → "baz: " <> a
-        }
+          { baz: \a → "baz: " <> a
+          }
 
   assert' "onMatch overSome: foo" $ onMatch' (overSome' foo) == "foo: 42"
   assert' "onMatch overSome: bar" $ onMatch' (overSome' bar) == "bar: bar"
@@ -133,12 +125,12 @@ test = do
   assert' "eq: foo" $ (foo ∷ Variant TestVariants) == foo
   assert' "eq: bar" $ (bar ∷ Variant TestVariants) == bar
   assert' "eq: baz" $ (baz ∷ Variant TestVariants) == baz
-  assert' "notEq: foo" $ (foo ∷ Variant TestVariants) /= inj _foo 53
+  assert' "notEq: foo" $ (foo ∷ Variant TestVariants) /= inj @"foo" 53
   assert' "notEq: bar" $ (foo ∷ Variant TestVariants) /= bar
 
   assert' "compare: foo EQ" $ compare (foo ∷ Variant TestVariants) foo == EQ
-  assert' "compare: foo LT" $ compare (foo ∷ Variant TestVariants) (inj _foo 53) == LT
-  assert' "compare: foo GT" $ compare (foo ∷ Variant TestVariants) (inj _foo 12) == GT
+  assert' "compare: foo LT" $ compare (foo ∷ Variant TestVariants) (inj @"foo" 53) == LT
+  assert' "compare: foo GT" $ compare (foo ∷ Variant TestVariants) (inj @"foo" 12) == GT
   assert' "compare: LT" $ compare bar (foo ∷ Variant TestVariants) == LT
   assert' "compare: GT" $ compare (foo ∷ Variant TestVariants) bar == GT
 
@@ -150,11 +142,13 @@ test = do
     $ L.null
     $ (contract (bar ∷ Variant TestVariants) ∷ L.List (Variant (foo ∷ Int)))
 
-  assert' "show" $ show (foo ∷ Variant TestVariants) ==  """(inj @"foo" 42)"""
+  assert' "show" $ show (foo ∷ Variant TestVariants) == """(inj @"foo" 42)"""
 
   assert' "unvariant: foo" $
-    let Unvariant f = unvariant (foo ∷ Variant TestVariants)
-    in f \s _ → reflectSymbol s == "foo"
+    let
+      Unvariant f = unvariant (foo ∷ Variant TestVariants)
+    in
+      f \s _ → reflectSymbol s == "foo"
 
   assert' "unvariant: build record (foo)" $ recAfter.foo == 42
   assert' "unvariant: build record (bar)" $ recAfter.bar == "bar"
diff --git a/test/VariantEnums.purs b/test/VariantEnums.purs
index 81602a5..0f13fef 100644
--- a/test/VariantEnums.purs
+++ b/test/VariantEnums.purs
@@ -7,7 +7,6 @@ import Data.Maybe (Maybe(..))
 import Data.Variant (Variant, inj)
 import Effect (Effect)
 import Test.Assert (assert')
-import Type.Proxy (Proxy(..))
 
 type T = Variant
   ( a ∷ Unit
@@ -21,44 +20,40 @@ type TT = Variant
   , c ∷ T
   )
 
-_a = Proxy ∷ Proxy "a"
-_b = Proxy ∷ Proxy "b"
-_c = Proxy ∷ Proxy "c"
-
 test ∷ Effect Unit
 test = do
-  assert' "bottom: T" $ inj _a unit == (bottom ∷ T)
-  assert' "top: T" $ inj _c unit == (top ∷ T)
-  assert' "succ bottom: T" $ Just (inj _b unit) == succ (bottom ∷ T)
-  assert' "succ: T" $ Just (inj _c unit) == succ (inj _b unit ∷ T)
-  assert' "succ top: T" $ Nothing == succ (inj _c unit ∷ T)
+  assert' "bottom: T" $ inj @"a" unit == (bottom ∷ T)
+  assert' "top: T" $ inj @"c" unit == (top ∷ T)
+  assert' "succ bottom: T" $ Just (inj @"b" unit) == succ (bottom ∷ T)
+  assert' "succ: T" $ Just (inj @"c" unit) == succ (inj @"b" unit ∷ T)
+  assert' "succ top: T" $ Nothing == succ (inj @"c" unit ∷ T)
   assert' "pred bottom: T" $ Nothing == pred (bottom ∷ T)
-  assert' "pred: T" $ Just (inj _a unit) == pred (inj _b unit ∷ T)
-  assert' "pred top: T" $ Just (inj _b unit) == pred (top ∷ T)
+  assert' "pred: T" $ Just (inj @"a" unit) == pred (inj @"b" unit ∷ T)
+  assert' "pred top: T" $ Just (inj @"b" unit) == pred (top ∷ T)
   assert' "fromEnum bottom: T" $ 0 == fromEnum (bottom ∷ T)
-  assert' "fromEnum: T" $ 1 == fromEnum (inj _b unit ∷ T)
+  assert' "fromEnum: T" $ 1 == fromEnum (inj @"b" unit ∷ T)
   assert' "fromEnum top: T" $ 2 == fromEnum (top ∷ T)
-  assert' "toEnum: T 0" $ toEnum 0 == Just (inj _a unit ∷ T)
-  assert' "toEnum: T 1" $ toEnum 1 == Just (inj _b unit ∷ T)
-  assert' "toEnum: T 2" $ toEnum 2 == Just (inj _c unit ∷ T)
+  assert' "toEnum: T 0" $ toEnum 0 == Just (inj @"a" unit ∷ T)
+  assert' "toEnum: T 1" $ toEnum 1 == Just (inj @"b" unit ∷ T)
+  assert' "toEnum: T 2" $ toEnum 2 == Just (inj @"c" unit ∷ T)
   assert' "toEnum: T 3" $ toEnum 3 == (Nothing ∷ Maybe T)
   assert' "cardinality: T" $ Cardinality 3 == (cardinality ∷ Cardinality T)
 
-  assert' "bottom: TT" $ inj _a (inj _a unit) == (bottom ∷ TT)
-  assert' "top: TT" $ inj _c (inj _c unit) == (top ∷ TT)
-  assert' "succ bottom: TT" $ (Just (inj _a (inj _b unit))) == succ (bottom ∷ TT)
+  assert' "bottom: TT" $ inj @"a" (inj @"a" unit) == (bottom ∷ TT)
+  assert' "top: TT" $ inj @"c" (inj @"c" unit) == (top ∷ TT)
+  assert' "succ bottom: TT" $ (Just (inj @"a" (inj @"b" unit))) == succ (bottom ∷ TT)
   assert' "succ top: TT" $ Nothing == succ (top ∷ TT)
-  assert' "succ: medium top TT" $ Just (inj _b bottom) == succ (inj _a top ∷ TT)
-  assert' "pred: medium bottom TT" $ Just (inj _a top) == pred (inj _b bottom ∷ TT)
+  assert' "succ: medium top TT" $ Just (inj @"b" bottom) == succ (inj @"a" top ∷ TT)
+  assert' "pred: medium bottom TT" $ Just (inj @"a" top) == pred (inj @"b" bottom ∷ TT)
   assert' "cardinality: TT" $ Cardinality 9 == (cardinality ∷ Cardinality TT)
-  assert' "fromEnum: TT 0" $ 0 == fromEnum (inj _a (inj _a unit) ∷ TT)
-  assert' "fromEnum: TT 3" $ 3 == fromEnum (inj _b (inj _a unit) ∷ TT)
-  assert' "fromEnum: TT 8" $ 8 == fromEnum (inj _c (inj _c unit) ∷ TT)
-  assert' "fromEnum: TT 4" $ 4 == fromEnum (inj _b (inj _b unit) ∷ TT)
-  assert' "toEnum: TT 0" $ toEnum 0 == Just (inj _a (inj _a unit) ∷ TT)
-  assert' "toEnum: TT 1" $ toEnum 1 == Just (inj _a (inj _b unit) ∷ TT)
-  assert' "toEnum: TT 3" $ toEnum 3 == Just (inj _b (inj _a unit) ∷ TT)
-  assert' "toEnum: TT 5" $ toEnum 5 == Just (inj _b (inj _c unit) ∷ TT)
-  assert' "toEnum: TT 6" $ toEnum 6 == Just (inj _c (inj _a unit) ∷ TT)
-  assert' "toEnum: TT 8" $ toEnum 8 == Just (inj _c (inj _c unit) ∷ TT)
+  assert' "fromEnum: TT 0" $ 0 == fromEnum (inj @"a" (inj @"a" unit) ∷ TT)
+  assert' "fromEnum: TT 3" $ 3 == fromEnum (inj @"b" (inj @"a" unit) ∷ TT)
+  assert' "fromEnum: TT 8" $ 8 == fromEnum (inj @"c" (inj @"c" unit) ∷ TT)
+  assert' "fromEnum: TT 4" $ 4 == fromEnum (inj @"b" (inj @"b" unit) ∷ TT)
+  assert' "toEnum: TT 0" $ toEnum 0 == Just (inj @"a" (inj @"a" unit) ∷ TT)
+  assert' "toEnum: TT 1" $ toEnum 1 == Just (inj @"a" (inj @"b" unit) ∷ TT)
+  assert' "toEnum: TT 3" $ toEnum 3 == Just (inj @"b" (inj @"a" unit) ∷ TT)
+  assert' "toEnum: TT 5" $ toEnum 5 == Just (inj @"b" (inj @"c" unit) ∷ TT)
+  assert' "toEnum: TT 6" $ toEnum 6 == Just (inj @"c" (inj @"a" unit) ∷ TT)
+  assert' "toEnum: TT 8" $ toEnum 8 == Just (inj @"c" (inj @"c" unit) ∷ TT)
   assert' "toEnum: TT 9" $ toEnum 9 == (Nothing ∷ Maybe TT)
diff --git a/test/VariantF.purs b/test/VariantF.purs
index d706cf7..dd55f0c 100644
--- a/test/VariantF.purs
+++ b/test/VariantF.purs
@@ -9,51 +9,42 @@ import Data.Maybe (Maybe(..), isJust)
 import Data.Tuple (Tuple(..))
 import Effect (Effect)
 import Test.Assert (assert')
-import Type.Proxy (Proxy(..))
 
 type TestVariants =
   ( foo ∷ Maybe
   , bar ∷ Tuple String
   , baz ∷ Either String
   )
+
 type TestVariants' =
   ( foo ∷ Either String
   , bar ∷ Tuple String
   , baz ∷ Either String
   )
 
-_foo ∷ Proxy "foo"
-_foo = Proxy
-
-_bar ∷ Proxy "bar"
-_bar = Proxy
-
-_baz ∷ Proxy "baz"
-_baz = Proxy
-
 foo ∷ ∀ r. VariantF (foo ∷ Maybe | r) Int
-foo = inj _foo (Just 42)
+foo = inj @"foo" (Just 42)
 
 bar ∷ ∀ r. VariantF (bar ∷ Tuple String | r) Int
-bar = inj _bar (Tuple "bar" 42)
+bar = inj @"bar" (Tuple "bar" 42)
 
 baz ∷ ∀ r. VariantF (baz ∷ Either String | r) Int
-baz = inj _baz (Left "baz")
+baz = inj @"baz" (Left "baz")
 
 completeness ∷ ∀ r a. VariantF r a → VariantF r a
 completeness = revariantF <<< unvariantF
 
 test ∷ Effect Unit
 test = do
-  assert' "prj: Foo" $ prj _foo foo == Just (Just 42)
-  assert' "prj: !Foo" $ prj _foo bar == (Nothing ∷ Maybe (Maybe Int))
+  assert' "prj: Foo" $ prj @"foo" foo == Just (Just 42)
+  assert' "prj: !Foo" $ prj @"foo" bar == (Nothing ∷ Maybe (Maybe Int))
 
   let
     case1 ∷ VariantF TestVariants Int → String
     case1 = case_
-      # on _foo (\a → "foo: " <> show a)
-      # on _bar (\a → "bar: " <> show a)
-      # on _baz (\a → "baz: " <> show a)
+      # on @"foo" (\a → "foo: " <> show a)
+      # on @"bar" (\a → "bar: " <> show a)
+      # on @"baz" (\a → "baz: " <> show a)
 
   assert' "case1: foo" $ case1 foo == "foo: (Just 42)"
   assert' "case1: bar" $ case1 bar == "bar: (Tuple \"bar\" 42)"
@@ -62,8 +53,8 @@ test = do
   let
     case2 ∷ VariantF TestVariants Int → String
     case2 = default "no match"
-      # on _foo (\a → "foo: " <> show a)
-      # on _bar (\a → "bar: " <> show a)
+      # on @"foo" (\a → "foo: " <> show a)
+      # on @"bar" (\a → "bar: " <> show a)
 
   assert' "case2: foo" $ case2 foo == "foo: (Just 42)"
   assert' "case2: bar" $ case2 bar == "bar: (Tuple \"bar\" 42)"
@@ -71,7 +62,7 @@ test = do
 
   let
     case3 ∷ VariantF (foo ∷ Maybe) String → String
-    case3 = case_ # on _foo (\a → "foo: " <> show a)
+    case3 = case_ # on @"foo" (\a → "foo: " <> show a)
 
   assert' "map" $ case3 (show <$> foo) == "foo: (Just \"42\")"
 
@@ -91,12 +82,12 @@ test = do
     onMatch' ∷ VariantF TestVariants Int → String
     onMatch' = case_
       # onMatch
-        { foo: \a → "foo: " <> show a
-        , baz: \a → "baz: " <> show a
-        }
+          { foo: \a → "foo: " <> show a
+          , baz: \a → "baz: " <> show a
+          }
       # onMatch
-        { bar: \a → "bar: " <> show a
-        }
+          { bar: \a → "bar: " <> show a
+          }
 
   assert' "onMatch: foo" $ onMatch' foo == "foo: (Just 42)"
   assert' "onMatch: bar" $ onMatch' bar == "bar: (Tuple \"bar\" 42)"
@@ -105,9 +96,9 @@ test = do
   let
     map' ∷ VariantF TestVariants Int → String
     map' = case_
-      # on _foo (\a → "foo: " <> show a)
-      # on _bar (\a → "bar: " <> show a)
-      # on _baz (\a → "baz: " <> show a)
+      # on @"foo" (\a → "foo: " <> show a)
+      # on @"bar" (\a → "bar: " <> show a)
+      # on @"baz" (\a → "baz: " <> show a)
 
     map'' ∷ VariantF TestVariants Int → String
     map'' = map (_ + 2) >>> map'
@@ -115,14 +106,17 @@ test = do
     overSome' ∷ VariantF TestVariants Int → VariantF TestVariants Int
     overSome' = overSome
       { baz: \(_ ∷ Either String Int) → Right 20
-      } expand
+      }
+      expand
 
-    over' ∷ forall r.
-      VariantF (baz ∷ Either String | r) Int →
-      VariantF (baz ∷ Either String | r) Int
+    over'
+      ∷ forall r
+       . VariantF (baz ∷ Either String | r) Int
+      → VariantF (baz ∷ Either String | r) Int
     over' = over
       { baz: \(_ ∷ Either String Int) → Right 20
-      } identity
+      }
+      identity
 
   assert' "map: foo" $ map'' foo == "foo: (Just 44)"
   assert' "map: bar" $ map'' bar == "bar: (Tuple \"bar\" 44)"
@@ -144,4 +138,4 @@ test = do
     $ L.null
     $ (contract (bar ∷ VariantF TestVariants Int) ∷ L.List (VariantF (foo ∷ Maybe) Int))
 
-  assert' "show" $ show (foo ∷ VariantF TestVariants Int) ==  """(inj @"foo" (Just 42))"""
+  assert' "show" $ show (foo ∷ VariantF TestVariants Int) == """(inj @"foo" (Just 42))"""