red-black-record 2.0.4.0 → 2.1.0.0

raw patch · 7 files changed

+611/−494 lines, 7 filesdep ~doctestPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: doctest

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−0
• README.md +194/−196
• lib/Data/RBR.hs +91/−82
• lib/Data/RBR/Examples.hs +6/−6
• lib/Data/RBR/Internal.hs +260/−204
• red-black-record.cabal +6/−5
• tests/tests.hs +48/−1

@@ -1,5 +1,11 @@ # Revision history for red-black-record
 
+## 2.1.0.0
+
+- Made the type-level map poly-kinded in the values, as there wasn't a real
+  reason to force them to the  Type kind. 
+- Removed deprecated EmptyMap (use Empty instead).
+
 ## 2.0.4.0
 
 - Compatibility with sop-core 0.5.0.0.

@@ -1,196 +1,194 @@-# red-black-record--## What's this?--A library that provides extensible records and variants, both indexed by a-type-level [red-black](https://en.wikipedia.org/wiki/Red%E2%80%93black_tree)-tree that maps `Symbol` keys to `Type`s. The keys correspond to fields names in-records, and to branch names in variants. Many record functions have their-variant mirror-images and viceversa.--Each value type in a field or branch comes wrapped in a type constructor of-kind `Type -> Type`. Typically, it will be an [identity-functor](http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP.html#t:I),-but it can also be `Maybe` or some other `Applicative` for parsing, validation-and so on.--If we forget about the keys and only keep the values, records are isomorphic to-[n-ary unlabeled-products](http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP.html#t:NP),-and variants are isomorphic to [n-ary unlabeled-sums](http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP.html#t:NS).-The [sop-core](http://hackage.haskell.org/package/sop-core) library provides-such unlabeled types, along with a rich API for manipulating them. Instead of-reinventing the wheel, red-black-record defines conversion functions to-facilitate working in the "unlabeled" world and then coming back to records and-variants.--There is another world towards which bridges must be built: the everyday-Haskell world of conventional records and sums. In fact, one of the motivations-of extensible records and variants is to serve as "generalized" versions of-vanilla data types. Advanced use cases can rely on these generalized versions,-thereby avoiding intrusive changes to the original types. red-black-record-provides conversion typeclasses with default implementations by way of-[`GHC.Generic`](http://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-Generics.html).--For examples on how to use the library, check the haddocks for the-`Data.RBR.Examples` module.--## FAQ--### What extensions do I need to use this library?--* `DataKinds`.--* `TypeApplications` to be able to specify field and branch names.--* `TypeFamilies`.--* `FlexibleContexts`.--* `DeriveGeneric` for interfacing with normal records.--* `PartialTypeSignatures` for hiding complex tree types.--### My type signatures are getting big and scary because of those type-level trees. What to do?--The-[`-XPartialTypeSignatures`](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?#extension-PartialTypeSignatures)-extension can help with that, in combination with the-[-Wno-partial-type-signatures](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/using-warnings.html#ghc-flag--Wpartial-type-signatures)-GHC flag that disables the warning message emitted when the underscore is-encountered in a signature.--The flag can be set globally in the-[ghc-options](https://www.haskell.org/cabal/users-guide/developing-packages.html?#pkg-field-ghc-options)-section of the .cabal file, and also for particular modules with the-[OPTIONS_GHC](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?highlight=options_ghc#options-ghc-pragma)-file-header pragma.--### The `Show` instance for record doesn't show any field names.--The field names exist only at the type level. Also, the `Show` instance uses-n-ary products and sums from-[sop-core](http://hackage.haskell.org/package/sop-core), which do not have-field labels.--For fancier output, use the "pretty-show" functions instead.--### Working with two records, I'm getting errors about incompatible types even as both records have the exact same fields.--Alas, the order of insertion in the type-level tree matters :( Different-insertion orders can produce structurally different trees, even as they encode-the same symbol-to-type map.--As a workaround, one can use the `-Subset` functions to convert between-equivalent structures.--### I can't insert into a record when a field with the same name but different type already exists. Why not simply overwrite it?--That limitation was intentional, because allowing it would make impossible to-implement of `widen` for `Variant`. One solution is to explicitly delete the-field and then insert it again.--### The library doesn't use Proxy and relies on type application instead. But what’s the order of the type parameters?--For typeclass methods, it's the order in which the type variables appear in the-typeclass declaration.--For standalone functions, it’s the order in which the type variables appear in-the `forall`.--### What's the deal with all those -I suffixed versions of functions?--This library aims to provide-[HKD](http://reasonablypolymorphic.com/blog/higher-kinded-data/)-like-functionality by wrapping all the fields of a record in a type constructor.--But sometimes we are working with "pure" records without effects, and we just-want to get and set a field's value. In that case, the type constructor that-wraps each field will be an identity functor `I` (from-[sop-core](http://hackage.haskell.org/package/sop-core)). The -I suffixed-functions wrap and unwrap the field's value on behalf of the user.--### What's the deal with all those -Subset suffixed versions of functions?--These functions target multiple fields or branches at the same time. They can-be used to build lawful lenses and prisms over fragmenst of a structure.--They can also be used to convert between type-level trees that have the same-entries but different structure.--### What about compilation times?--Compilation times balloon for large records. In the tests folder there's-an example (not run by default in the tests) of the construction of a 50-field-record whose fields are afterwards accessed one by one. It takes about 22-seconds to compile in my machine. --Code involving deletion of fields and branches (like using the `winnow`-function for `Variant`s) is currently poorly optimized and will compile-[slower](https://github.com/danidiaz/red-black-record/issues/12) than that.--The default generics-based implementations of `FromRecord` and `FromVariant`-use the same type-level machinery as the getters and its use will likely slow-down compilation as well.--## Inspirations--* The code for the red-black tree has been lifted from Stefan Kahrs's code-  [available-  here](https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html). See also-  [this post](https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html).--* Besides depending on sop-core, I have copied and adapted code from it. In-  particular the `KeysValuessAll` typeclass is a version of the `All` typeclass-  from sop-core. --* [Surgery for data-  types](https://blog.poisson.chat/posts/2018-11-26-type-surgery.html).-  [reddit](https://www.reddit.com/r/haskell/comments/a0gi4z/surgery_for_data_types/).--## Alternatives--* [generics-sop](http://hackage.haskell.org/package/generics-sop) and-  [records-sop](http://hackage.haskell.org/package/records-sop). Like-  red-black-record, both of these libraries build upon sop-core. They are in-  fact written by the same author of sop-core. generics-sop can provide-  sum-of-products representations of any datatype with a Generic instance-  (red-black-record is more limited, it only converts types that fit the named-  record or variant mold—so no types with anonymous fields for example). -  -  If you don't need to explicitly target *individual* fields in the generic-  representation, you'll be better off using generics-sop instead of-  red-black-record. -  -  On top of generics-sop, records-sop provides named field accessors and record-  subtyping based on a type-level list of fields (unlike the type-level tree-  used by red-black-record). It doesn't seem to provide variants.--* [superrecord](http://hackage.haskell.org/package/superrecord). This library-  provides very efficient field access at runtime because the fields are backed-  internally by an array. Uses a *sorted* type-level list of fields, to avoid-  the problems of multiple orderings of the same fields.--* [vinyl](http://hackage.haskell.org/package/vinyl). One of the oldest and more-  fully-featured extensible records libraries. Uses a type level list of-  fields. The fields' values are wrapped in a type constructor, like in-  sop-core. The records seem to use an auxiliary sum type that serves as a-  "code" for the fields. See also-  [vinyl-genercics](https://hackage.haskell.org/package/vinyl-generics).--* [HTree](https://github.com/i-am-tom/learn-me-a-haskell#htree). Another-  implementation of extensible records using type-level red-black trees.--* [megarecord](https://github.com/jvanbruegge/Megarecord). Seems to be a-  proof-of-concept for a future [row polymorphism-  extension](https://github.com/ghc-proposals/ghc-proposals/pull/180) for-  Haskell.--* [generic-data-surgery](https://hackage.haskell.org/package/generic-data-surgery).-  Lots of useful machinery for manipulating generic representations of-  dataytpes, without requiring intrusive changes to the original-  representation.--* [Coxswain](https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain).-+# red-black-record
+
+## What's this?
+
+A library that provides extensible records and variants, both indexed by a
+type-level [red-black](https://en.wikipedia.org/wiki/Red%E2%80%93black_tree)
+tree that maps `Symbol` keys to value types of any kind. The keys correspond to
+field names in records, and to branch names in variants. Many record functions
+have their variant mirror-images and viceversa.
+
+At the term level, value types come wrapped in a type constructor of kind `q ->
+Type`, where `q` is the kind of value types. Typically, the type constructor
+will be an [identity
+functor](http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP.html#t:I),
+but it can also be `Maybe` or some other `Applicative` for parsing, validation
+and so on.
+
+If we forget about the keys and only keep the values, records are isomorphic to
+[n-ary unlabeled
+products](http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP.html#t:NP),
+and variants are isomorphic to [n-ary unlabeled
+sums](http://hackage.haskell.org/package/sop-core-0.4.0.0/docs/Data-SOP.html#t:NS).
+The [sop-core](http://hackage.haskell.org/package/sop-core) library provides
+such unlabeled types, along with a rich API for manipulating them. Instead of
+reinventing the wheel, red-black-record defines conversion functions to
+facilitate working in the "unlabeled" world and then coming back to records and
+variants.
+
+There is another world towards which bridges must be built: the everyday
+Haskell world of conventional records and sums. In fact, one of the motivations
+of extensible records and variants is to serve as "generalized" versions of
+vanilla data types. Advanced use cases can rely on these generalized versions,
+thereby avoiding intrusive changes to the original types. red-black-record
+provides conversion typeclasses with default implementations by way of
+[`GHC.Generic`](http://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-Generics.html).
+
+For examples on how to use the library, check the haddocks for the
+`Data.RBR.Examples` module.
+
+## FAQ
+
+### What extensions do I need to use this library?
+
+* `DataKinds`.
+
+* `TypeApplications` to be able to specify field and branch names.
+
+* `TypeFamilies`.
+
+* `FlexibleContexts`.
+
+* `DeriveGeneric` for interfacing with normal records.
+
+* `PartialTypeSignatures` for hiding complex tree types.
+
+### My type signatures are getting big and scary because of those type-level trees. What to do?
+
+The
+[`-XPartialTypeSignatures`](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?#extension-PartialTypeSignatures)
+extension can help with that, in combination with the
+[-Wno-partial-type-signatures](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/using-warnings.html#ghc-flag--Wpartial-type-signatures)
+GHC flag that disables the warning message emitted when the underscore is
+encountered in a signature.
+
+The flag can be set globally in the
+[ghc-options](https://www.haskell.org/cabal/users-guide/developing-packages.html?#pkg-field-ghc-options)
+section of the .cabal file, and also for particular modules with the
+[OPTIONS_GHC](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?highlight=options_ghc#options-ghc-pragma)
+file-header pragma.
+
+### The `Show` instance for record doesn't show any field names.
+
+The field names exist only at the type level. Also, the `Show` instance uses
+n-ary products and sums from
+[sop-core](http://hackage.haskell.org/package/sop-core), which do not have
+field labels.
+
+For fancier output, use the "pretty-show" functions instead.
+
+### Working with two records, I'm getting errors about incompatible types even as both records have the exact same fields.
+
+Alas, the order of insertion in the type-level tree matters :( Different
+insertion orders can produce structurally different trees, even as they encode
+the same symbol-to-type map.
+
+As a workaround, one can use the `-Subset` functions to convert between
+equivalent structures.
+
+### I can't insert into a record when a field with the same name but different type already exists. Why not simply overwrite it?
+
+That limitation was intentional, because allowing it would make impossible to
+implement of `widen` for `Variant`. One solution is to explicitly delete the
+field and then insert it again.
+
+### The library doesn't use Proxy and relies on type application instead. But what’s the order of the type parameters?
+
+For standalone functions, it’s the order in which the type variables appear in
+the `forall`.
+
+### What's the deal with all those -I suffixed versions of functions?
+
+This library aims to provide
+[HKD](http://reasonablypolymorphic.com/blog/higher-kinded-data/)-like
+functionality by wrapping all the fields of a record in a type constructor.
+
+But sometimes we are working with "pure" records without effects, and we just
+want to get and set a field's value. In that case, the type constructor that
+wraps each field will be an identity functor `I` (from
+[sop-core](http://hackage.haskell.org/package/sop-core)). The -I suffixed
+functions wrap and unwrap the field's value on behalf of the user.
+
+### What's the deal with all those -Subset suffixed versions of functions?
+
+These functions target multiple fields or branches at the same time. They can
+be used to build lawful lenses and prisms over fragmenst of a structure.
+
+They can also be used to convert between type-level trees that have the same
+entries but different structure.
+
+### What about compilation times?
+
+Compilation times balloon for large records. In the tests folder there's
+an example (not run by default in the tests) of the construction of a 50-field
+record whose fields are afterwards accessed one by one. It takes about 22
+seconds to compile in my machine. 
+
+Code involving deletion of fields and branches (like using the `winnow`
+function for `Variant`s) is currently poorly optimized and will compile
+[slower](https://github.com/danidiaz/red-black-record/issues/12) than that.
+
+The default generics-based implementations of `FromRecord` and `FromVariant`
+use the same type-level machinery as the getters and its use will likely slow
+down compilation as well.
+
+## Inspirations
+
+* The code for the red-black tree has been lifted from Stefan Kahrs's code
+  [available
+  here](https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html). See also
+  [this post](https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html).
+
+* Besides depending on sop-core, I have copied and adapted code from it. In
+  particular the `KeysValuessAll` typeclass is a version of the `All` typeclass
+  from sop-core. 
+
+* [Surgery for data
+  types](https://blog.poisson.chat/posts/2018-11-26-type-surgery.html).
+  [reddit](https://www.reddit.com/r/haskell/comments/a0gi4z/surgery_for_data_types/).
+
+## Alternatives
+
+* [generics-sop](http://hackage.haskell.org/package/generics-sop) and
+  [records-sop](http://hackage.haskell.org/package/records-sop). Like
+  red-black-record, both of these libraries build upon sop-core. They are in
+  fact written by the same author of sop-core. generics-sop can provide
+  sum-of-products representations of any datatype with a Generic instance
+  (red-black-record is more limited, it only converts types that fit the named
+  record or variant mold—so no types with anonymous fields for example). 
+  
+  If you don't need to explicitly target *individual* fields in the generic
+  representation, you'll be better off using generics-sop instead of
+  red-black-record. 
+  
+  On top of generics-sop, records-sop provides named field accessors and record
+  subtyping based on a type-level list of fields (unlike the type-level tree
+  used by red-black-record). It doesn't seem to provide variants.
+
+* [superrecord](http://hackage.haskell.org/package/superrecord). This library
+  provides very efficient field access at runtime because the fields are backed
+  internally by an array. Uses a *sorted* type-level list of fields, to avoid
+  the problems of multiple orderings of the same fields.
+
+* [vinyl](http://hackage.haskell.org/package/vinyl). One of the oldest and more
+  fully-featured extensible records libraries. Uses a type level list of
+  fields. The fields' values are wrapped in a type constructor, like in
+  sop-core. The records seem to use an auxiliary sum type that serves as a
+  "code" for the fields. See also
+  [vinyl-genercics](https://hackage.haskell.org/package/vinyl-generics).
+
+* [HTree](https://github.com/i-am-tom/learn-me-a-haskell#htree). Another
+  implementation of extensible records using type-level red-black trees.
+
+* [megarecord](https://github.com/jvanbruegge/Megarecord). Seems to be a
+  proof-of-concept for a future [row polymorphism
+  extension](https://github.com/ghc-proposals/ghc-proposals/pull/180) for
+  Haskell.
+
+* [generic-data-surgery](https://hackage.haskell.org/package/generic-data-surgery).
+  Lots of useful machinery for manipulating generic representations of
+  dataytpes, without requiring intrusive changes to the original
+  representation.
+
+* [Coxswain](https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain).
+

@@ -1,88 +1,97 @@ module Data.RBR (
         -- * Type-level Red-Black tree
         -- $typelevel
-        Map,
-        Empty,
-        EmptyMap,
-        KeysValuesAll,
-        KnownKey,
-        demoteKeys,
-        KnownKeyTypeableValue,
-        demoteEntries,
-        -- * Records and Variants
-        Record,
-        unit,
-        cpure_Record,
-        collapse_Record,
-        prettyShowRecord,
-        prettyShowRecordI,
-        Variant,
-        impossible,
-        prettyShowVariant,
-        prettyShowVariantI,
-        -- ** Inserting and widening
-        Insertable (..),
-        addField,
-        insertI,
-        addFieldI,
-        InsertAll,
-        FromList,
-        -- ** Deleting and winnowing
-        Deletable (..),
-        winnowI,
-        -- ** Projecting and injecting
-        Key (..),
-        Field,
-        Branch,
-        project,
-        projectI,
-        getField,
-        getFieldI,
-        setField,
-        setFieldI,
-        modifyField,
-        modifyFieldI,
-        inject,
-        injectI,
-        match,
-        matchI,
-        -- ** Eliminating variants
-        eliminate,
-        Case (..),
-        addCase,
-        addCaseI,
-        -- ** Subsets of fields and branches
-        PresentIn,
-        ProductlikeSubset,
-        fieldSubset,
-        projectSubset,
-        getFieldSubset,
-        setFieldSubset,
-        modifyFieldSubset,
-        SumlikeSubset,
-        branchSubset,
-        injectSubset,
-        matchSubset,
-        eliminateSubset,
-        -- * Interfacing with normal records
-        -- $nominal
-        ToRecord (..),
-        FromRecord (..),
-        VariantCode,
-        ToVariant (..),
-        FromVariant(..),
-        -- * Interfacing with Data.SOP
-        Productlike (..),
-        fromNP,
-        toNP,
-        Sumlike (..),
-        fromNS,
-        toNS,
-        -- * Data.SOP re-exports
-        I(..),
-        K(..),
-        NP(..),
-        NS(..),
+       Map,
+       Empty,
+       KeysValuesAll(),
+       KnownKey(),
+       demoteKeys,
+       KnownKeyTypeableValue(),
+       demoteEntries,
+       -- * Records and Variants
+       Record,
+       unit,
+       cpure_Record,
+       collapse_Record,
+       prettyShowRecord,
+       prettyShowRecordI,
+       Variant,
+       impossible,
+       prettyShowVariant,
+       prettyShowVariantI,
+       -- ** Inserting and widening
+       Insertable (Insert),
+       InsertAll,
+       FromList,
+       insert,
+       addField,
+       insertI,
+       addFieldI,
+       widen,
+       -- ** Deleting and winnowing
+       Deletable (Delete),
+       delete,
+       winnow,
+       winnowI,
+       -- ** Projecting and injecting
+       Key (Value),
+       Field,
+       field,
+       Branch,
+       branch,
+       project,
+       projectI,
+       getField,
+       getFieldI,
+       setField,
+       setFieldI,
+       modifyField,
+       modifyFieldI,
+       inject,
+       injectI,
+       match,
+       matchI,
+       -- ** Eliminating variants
+       eliminate,
+       Case (..),
+       addCase,
+       addCaseI,
+       -- ** Subsets of fields and branches
+       PresentIn,
+       ProductlikeSubset,
+       fieldSubset,
+       projectSubset,
+       getFieldSubset,
+       setFieldSubset,
+       modifyFieldSubset,
+       SumlikeSubset,
+       branchSubset,
+       injectSubset,
+       matchSubset,
+       eliminateSubset,
+       -- * Interfacing with normal records
+       -- $nominal
+       ToRecord (..),
+       FromRecord (..),
+       VariantCode,
+       ToVariant (..),
+       FromVariant(..),
+       -- * Interfacing with Data.SOP
+       Productlike (..),
+       prefixNP,
+       breakNP,
+       fromNP,
+       toNP,
+       Sumlike (..),
+       prefixNS,
+       breakNS,
+       fromNS,
+       toNS,
+       -- * Data.SOP re-exports
+       I(..),
+       K(..),
+       NP(..),
+       NS(..),
     ) where
 
 import Data.RBR.Internal

@@ -188,8 +188,8 @@               -> Parser r
         parseSpecial transform = 
             let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name))
-                pr = transform $ fromNP @c (cpure_NP (Proxy @FromJSON) (Star parseJSON))
-                Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c demoteKeys) (toNP pr))
+                fieldParsers = transform $ fromNP @c (cpure_NP (Proxy @FromJSON) (Star parseJSON))
+                Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c demoteKeys) (toNP fieldParsers))
              in withObject "someobj" $ \o -> fromRecord <$> parser o
     :}
 
@@ -226,8 +226,8 @@               -> Parser r
         parseWithAliases aliases = 
             let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name))
-                pr = fromNP @c (cpure_NP (Proxy @FromJSON) (Star parseJSON))
-                Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c aliases) (toNP pr))
+                fieldParsers = cpure_NP (Proxy @FromJSON) (Star parseJSON)
+                Star parser = fromNP <$> sequence_NP (liftA2_NP mapKSS (toNP @c aliases) fieldParsers)
              in withObject "someobj" $ \o -> fromRecord <$> parser o
     :}
 
@@ -317,8 +317,8 @@               -> Parser r
         parseAll = 
             let mapKSS (K name) (Star pf) = Star (\o -> explicitParseField pf o (Data.Text.pack name))
-                pnp = liftA2_NP mapKSS (toNP @c demoteKeys) (cpure_NP (Proxy @FromJSON) (Star parseJSON))
-                injected = liftA2_NP (\f star -> K (unK . apFn f . I <$> star)) (injections @flat) pnp 
+                branchParsers = liftA2_NP mapKSS (toNP @c demoteKeys) (cpure_NP (Proxy @FromJSON) (Star parseJSON))
+                injected = liftA2_NP (\f star -> K (unK . apFn f . I <$> star)) (injections @flat) branchParsers 
                 Star parser = asum $ collapse_NP injected
              in withObject "someobj" (\o -> fromVariant @r . fromNS <$> parser o)
     :}

@@ -58,9 +58,6 @@ -- | A map without entries. See also 'unit' and 'impossible'.
 type Empty = E
 
-{-# DEPRECATED EmptyMap "Use Empty instead." #-}
-type EmptyMap = E
-
 --
 --
 -- This code has been copied and adapted from the corresponding Data.SOP code (the All constraint).
@@ -76,12 +73,11 @@   KeysValuesAllF  c (N color left k v right) = (c k v, KeysValuesAll c left, KeysValuesAll c right)
 
 {- | Require a constraint for every key-value pair in a tree. This is a generalization of 'Data.SOP.All' from "Data.SOP".
- 
-     'cpara_Map' constructs a 'Record' by means of a constraint for producing
-     the nodes of the tree. The constraint is passed as a 'Data.Proxy.Proxy'.
-     
 -}
 class KeysValuesAllF c t => KeysValuesAll (c :: k -> v -> Constraint) (t :: Map k v) where
+
+  --  'cpara_Map' constructs a 'Record' by means of a constraint for producing
+  --  the nodes of the tree. The constraint is passed as a 'Data.Proxy.Proxy'.
   cpara_Map ::
        proxy c
     -> r E
@@ -153,7 +149,7 @@ 
   Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>.
 -}
-class (KnownSymbol k, Typeable v) => KnownKeyTypeableValue (k :: Symbol) (v :: Type)
+class (KnownSymbol k, Typeable v) => KnownKeyTypeableValue (k :: Symbol) v
 instance (KnownSymbol k, Typeable v) => KnownKeyTypeableValue k v 
 
 -- class KeyValueTop (k :: Symbol) (v :: z)
@@ -169,7 +165,7 @@ 
      See also 'insert', 'delete' and 'project'.
 -}
-data Record (f :: Type -> Type) (t :: Map Symbol Type)  where
+data Record (f :: q -> Type) (t :: Map Symbol q)  where
     Empty :: Record f E 
     Node  :: Record f left -> f v -> Record f right -> Record f (N color left k v right)
 
@@ -219,7 +215,7 @@ 
      See also 'widen', 'winnow' and 'inject'.
 -}
-data Variant (f :: Type -> Type) (t :: Map Symbol Type)  where
+data Variant (f :: q -> Type) (t :: Map Symbol q)  where
     Here       :: f v -> Variant f (N color left k v right)
     LookRight  :: Variant f t -> Variant f (N color' left' k' v' t)
     LookLeft   :: Variant f t -> Variant f (N color' t k' v' right')
@@ -258,17 +254,31 @@ 
 {- | Insert a list of type level key / value pairs into a type-level map. 
 -}
-type family InsertAll (es :: [(Symbol,Type)]) (t :: Map Symbol Type) :: Map Symbol Type where
+type family InsertAll (es :: [(Symbol,q)]) (t :: Map Symbol q) :: Map Symbol q where
     InsertAll '[] t = t
     InsertAll ( '(name,fieldType) ': es ) t = Insert name fieldType (InsertAll es t)
 
 {- | Build a type-level map out of a list of type level key / value pairs. 
 -}
-type FromList (es :: [(Symbol,Type)]) = InsertAll es Empty
+type FromList (es :: [(Symbol,q)]) = InsertAll es Empty
 
+
+{- |
+     Adds a new field to a 'Record'.
+ -}
+insert :: forall k v t f. Insertable k v t => f v -> Record f t -> Record f (Insert k v t)
+insert = _insert @_ @k @v @t @f
+
+{- |
+     Lets you use a 'Variant' in a bigger context
+     than the one in which is was defined. 
+ -}
+widen :: forall k v t f. Insertable k v t => Variant f t -> Variant f (Insert k v t)
+widen = _widen @_ @k @v @t @f
+
 {- | Alias for 'insert'. 
 -}
-addField :: forall k v t f . Insertable k v t => f v -> Record f t -> Record f (Insert k v t)
+addField :: forall k v t f. Insertable k v t => f v -> Record f t -> Record f (Insert k v t)
 addField = insert @k @v @t @f
 
 {- | Like 'insert' but specialized to pure 'Record's.
@@ -281,7 +291,7 @@ addFieldI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t)
 addFieldI = insertI @k @v @t
 
-{- | Class that determines if the pair of a 'Symbol' key and a 'Type' can
+{- | Class that determines if the pair of a 'Symbol' key and a type can
      be inserted into a type-level map.
  
      The associated type family 'Insert' produces the resulting map.
@@ -291,13 +301,13 @@      than the one in which is was defined. 'insert' tends to be more useful in
      practice.
 
-     If the map already has the key but with a /different/ 'Type', the
+     If the map already has the key but with a /different/ type, the
      insertion fails to compile.
  -}
-class Insertable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
-    type Insert k v t :: Map Symbol Type
-    insert :: f v -> Record f t -> Record f (Insert k v t)
-    widen :: Variant f t -> Variant f (Insert k v t)
+class Insertable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
+    type Insert k v t :: Map Symbol q
+    _insert :: f v -> Record f t -> Record f (Insert k v t)
+    _widen :: Variant f t -> Variant f (Insert k v t)
 
 -- insert x s =
 --  T B a z b
@@ -305,11 +315,11 @@ --  T _ a z b = ins s
 instance (InsertableHelper1 k v t, Insert1 k v t ~ inserted, CanMakeBlack inserted) => Insertable k v t where
     type Insert k v t = MakeBlack (Insert1 k v t)
-    insert fv r = makeBlackR (insert1 @k @v fv r) 
-    widen v = makeBlackV (widen1 @k @v v)
+    _insert fv r = makeBlackR @_ (insert1 @_ @k @v fv r) 
+    _widen v = makeBlackV @_ (widen1 @_ @k @v v)
 
-class CanMakeBlack (t :: Map Symbol Type) where
-    type MakeBlack t :: Map Symbol Type
+class CanMakeBlack (t :: Map Symbol k) where
+    type MakeBlack t :: Map Symbol k
     makeBlackR :: Record f t -> Record f (MakeBlack t)
     makeBlackV :: Variant f t -> Variant f (MakeBlack t)
 
@@ -327,9 +337,9 @@     makeBlackV = impossible
 
 class InsertableHelper1 (k :: Symbol) 
-                        (v :: Type) 
-                        (t :: Map Symbol Type) where
-    type Insert1 k v t :: Map Symbol Type 
+                        (v :: q) 
+                        (t :: Map Symbol q) where
+    type Insert1 k v t :: Map Symbol q 
     insert1 :: f v -> Record f t -> Record f (Insert1 k v t)
     widen1 :: Variant f t -> Variant f (Insert1 k v t)
 
@@ -345,18 +355,18 @@     -- FIXME possible duplicate work with CmpSymbol: both in constraint and in associated type family. 
     -- Is that bad? How to avoid it?
     type Insert1 k v (N color left k' v' right) = Insert2 (CmpSymbol k k') k v color left k' v' right  
-    insert1 = insert2 @ordering @k @v @color @left @k' @v' @right
-    widen1  = widen2 @ordering @k @v @color @left @k' @v' @right
+    insert1 = insert2 @_ @ordering @k @v @color @left @k' @v' @right
+    widen1  = widen2 @_ @ordering @k @v @color @left @k' @v' @right
 
 class InsertableHelper2 (ordering :: Ordering) 
                         (k :: Symbol) 
-                        (v :: Type) 
+                        (v :: q) 
                         (color :: Color) 
-                        (left :: Map Symbol Type) 
+                        (left :: Map Symbol q) 
                         (k' :: Symbol) 
-                        (v' :: Type) 
-                        (right :: Map Symbol Type) where
-    type Insert2 ordering k v color left k' v' right :: Map Symbol Type 
+                        (v' :: q) 
+                        (right :: Map Symbol q) where
+    type Insert2 ordering k v color left k' v' right :: Map Symbol q 
     insert2 :: f v -> Record f (N color left k' v' right) -> Record f (Insert2 ordering k v color left k' v' right)
     widen2 :: Variant f (N color left k' v' right) -> Variant f (Insert2 ordering k v color left k' v' right)
 
@@ -367,10 +377,10 @@          )
          => InsertableHelper2 LT k v B left k' v' right where
     type Insert2              LT k v B left k' v' right = Balance (Insert1 k v left) k' v' right
-    insert2 fv (Node left fv' right) = balanceR @_ @k' @v' @right (Node (insert1 @k @v fv left) fv' right) 
-    widen2 v = balanceV @(Insert1 k v left) @k' @v' @right $ case v of
+    insert2 fv (Node left fv' right) = balanceR @_ @_ @k' @v' @right (Node (insert1 @_ @k @v fv left) fv' right) 
+    widen2 v = balanceV @_ @(Insert1 k v left) @k' @v' @right $ case v of
         Here x -> Here x
-        LookLeft x -> LookLeft (widen1 @k @v x)
+        LookLeft x -> LookLeft (widen1 @_ @k @v x)
         LookRight x -> LookRight x
 
 --  ins s@(T B a y b)
@@ -380,10 +390,10 @@          )
          => InsertableHelper2 LT k v R left k' v' right where
     type Insert2              LT k v R left k' v' right = N R (Insert1 k v left) k' v' right
-    insert2 fv (Node left fv' right) = Node (insert1 @k @v fv left) fv' right 
+    insert2 fv (Node left fv' right) = Node (insert1 @_ @k @v fv left) fv' right 
     widen2 v = case v of
         Here x -> Here x
-        LookLeft x -> LookLeft (widen1 @k @v x)
+        LookLeft x -> LookLeft (widen1 @_ @k @v x)
         LookRight x -> LookRight x
 
 
@@ -403,11 +413,11 @@          )
          => InsertableHelper2 GT k v B left k' v' right where
     type Insert2              GT k v B left k' v' right = Balance left  k' v' (Insert1 k v right)
-    insert2 fv (Node left fv' right) = balanceR @left @k' @v' @_ (Node left  fv' (insert1 @k @v fv right)) 
-    widen2 v = balanceV @left @k' @v' @(Insert1 k v right) $ case v of
+    insert2 fv (Node left fv' right) = balanceR @_ @left @k' @v' @_ (Node left  fv' (insert1 @_ @k @v fv right)) 
+    widen2 v = balanceV @_ @left @k' @v' @(Insert1 k v right) $ case v of
         Here x -> Here x
         LookLeft x -> LookLeft x
-        LookRight x -> LookRight (widen1 @k @v x)
+        LookRight x -> LookRight (widen1 @_ @k @v x)
 
 --  ins s@(T R a y b)
 --      | ...
@@ -417,11 +427,11 @@          )
          => InsertableHelper2 GT k v R left k' v' right where
     type Insert2              GT k v R left k' v' right = N R left k' v' (Insert1 k v right)
-    insert2 fv (Node left fv' right) = Node left fv' (insert1 @k @v fv right) 
+    insert2 fv (Node left fv' right) = Node left fv' (insert1 @_ @k @v fv right) 
     widen2 v = case v of
         Here x -> Here x
         LookLeft x -> LookLeft x
-        LookRight x -> LookRight (widen1 @k @v x)
+        LookRight x -> LookRight (widen1 @_ @k @v x)
 
 data BalanceAction = BalanceSpecial
                    | BalanceLL
@@ -439,8 +449,8 @@     ShouldBalance _ (N R _ _ _ (N R _ _ _ _)) = BalanceRR
     ShouldBalance _ _                         = DoNotBalance
 
-class Balanceable (left :: Map Symbol Type) (k :: Symbol) (v :: Type) (right :: Map Symbol Type) where
-    type Balance left k v right :: Map Symbol Type
+class Balanceable (left :: Map Symbol q) (k :: Symbol) (v :: q) (right :: Map Symbol q) where
+    type Balance left k v right :: Map Symbol q
     balanceR :: Record f (N color left k v right) -> Record f (Balance left k v right)
     balanceV :: Variant f (N color left k v right) -> Variant f (Balance left k v right)
 
@@ -451,15 +461,15 @@     -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family. 
     -- Is that bad? How to avoid it?
     type Balance left k v right = Balance' (ShouldBalance left right) left k v right
-    balanceR = balanceR' @action @left @k @v @right
-    balanceV = balanceV' @action @left @k @v @right
+    balanceR = balanceR' @_ @action @left @k @v @right
+    balanceV = balanceV' @_ @action @left @k @v @right
     
 class BalanceableHelper (action :: BalanceAction) 
-                        (left :: Map Symbol Type) 
+                        (left :: Map Symbol q) 
                         (k :: Symbol) 
-                        (v :: Type) 
-                        (right :: Map Symbol Type) where
-    type Balance' action left k v right :: Map Symbol Type
+                        (v :: q) 
+                        (right :: Map Symbol q) where
+    type Balance' action left k v right :: Map Symbol q
     balanceR' :: Record f (N color left k v right) -> Record f (Balance' action left k v right)
     balanceV' :: Variant f (N color left k v right) -> Variant f (Balance' action left k v right)
 
@@ -548,6 +558,7 @@         Here v -> Here v
         LookRight r -> LookRight r
 
+
 --
 --
 -- Accessing fields
@@ -560,12 +571,12 @@ --
 {- | Auxiliary type family to avoid repetition and help improve compilation times.
  -}
-type family Field (f :: Type -> Type) (t :: Map Symbol Type) (v :: Type) where
+type family Field (f :: q -> Type) (t :: Map Symbol q) (v :: q) where
     Field f t v = Record f t -> (f v -> Record f t, f v)
 
 {- | Auxiliary type family to avoid repetition and help improve compilation times.
  -}
-type family Branch (f :: Type -> Type) (t :: Map Symbol Type) (v :: Type) where
+type family Branch (f :: q -> Type) (t :: Map Symbol q) (v :: q) where
     Branch f t v = (Variant f t -> Maybe (f v), f v -> Variant f t)
 
 --
@@ -574,39 +585,47 @@      map.
 
      The 'Value' type family gives the 'Type' corresponding to the key.
+-} 
+class Key (k :: Symbol) (t :: Map Symbol q) where
+    type Value k t :: q
+    _field  :: Field  f t (Value k t)
+    _branch :: Branch f t (Value k t)
 
-     'field' takes a field name (given through @TypeApplications@) and a
+{- |
+     Takes a field name (given through @TypeApplications@) and a
      'Record', and returns a pair of a setter for the field and the original
      value of the field.
-     
-     'branch' takes a branch name (given through @TypeApplications@) and
+-}
+field  :: forall k t f. Key k t => Field f t (Value k t)
+field = _field @_ @k @t
+
+{- |
+     Takes a branch name (given through @TypeApplications@) and
      returns a pair of a match function and a constructor.
--} 
-class Key (k :: Symbol) (t :: Map Symbol Type) where
-    type Value k t :: Type
-    field  :: Field  f t (Value k t)
-    branch :: Branch f t (Value k t)
+-}
+branch :: forall k t f. Key k t => Branch f t (Value k t)
+branch = _branch @_ @k @t
 
 -- member :: Ord a => a -> RB a -> Bool
-class KeyHelper (ordering :: Ordering) (k :: Symbol) (left :: Map Symbol Type) (v :: Type) (right :: Map Symbol Type) where 
-    type Value' ordering k left v right :: Type
+class KeyHelper (ordering :: Ordering) (k :: Symbol) (left :: Map Symbol q) (v :: q) (right :: Map Symbol q) where 
+    type Value' ordering k left v right :: q
     field'  :: Field  f (N colorx left kx v right) (Value' ordering k left v right)
     branch' :: Branch f (N colorx left kx v right) (Value' ordering k left v right)
 
 instance (CmpSymbol k' k ~ ordering, KeyHelper ordering k left v' right) => Key k (N color left k' v' right) where
     type Value k (N color left k' v' right) = Value' (CmpSymbol k' k) k left v' right
-    field = field' @ordering @k @left @v' @right
-    branch = branch' @ordering @k @left @v' @right
+    _field = field' @_ @ordering @k @left @v' @right
+    _branch = branch' @_ @ordering @k @left @v' @right
 
 --  | x<y = member x a
 instance (CmpSymbol k2 k ~ ordering, KeyHelper ordering k left2 v2 right2) 
       => KeyHelper LT k left v (N color2 left2 k2 v2 right2) where
     type Value'    LT k left v (N color2 left2 k2 v2 right2) = Value' (CmpSymbol k2 k) k left2 v2 right2
     field' (Node left fv right) = 
-        let (setter,x) = field' @ordering @k @left2 @v2 @right2 right
+        let (setter,x) = field' @_ @ordering @k @left2 @v2 @right2 right
          in (\z -> Node left fv (setter z),x)
     branch' = 
-        let (match,inj) = branch' @ordering @k @left2 @v2 @right2 
+        let (match,inj) = branch' @_ @ordering @k @left2 @v2 @right2 
          in (\case LookRight x -> match x
                    _ -> Nothing,
              \fv -> LookRight (inj fv))
@@ -616,10 +635,10 @@       => KeyHelper GT k (N color2 left2 k2 v2 right2) v' right where
     type    Value' GT k (N color2 left2 k2 v2 right2) v' right = Value' (CmpSymbol k2 k) k left2 v2 right2
     field' (Node left fv right) = 
-        let (setter,x) = field' @ordering @k @left2 @v2 @right2 left
+        let (setter,x) = field' @_ @ordering @k @left2 @v2 @right2 left
          in (\z -> Node (setter z) fv right,x)
     branch' =
-        let (match,inj) = branch' @ordering @k @left2 @v2 @right2 
+        let (match,inj) = branch' @_ @ordering @k @left2 @v2 @right2 
          in (\case LookLeft x -> match x
                    _ -> Nothing,
              \fv -> LookLeft (inj fv))
@@ -724,15 +743,15 @@ newtype SetField f a b = SetField { getSetField :: f b -> a -> a }
  
 -- this odd trick again...
-class (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol Type) (k :: Symbol) (v :: Type) 
-instance (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol Type) (k :: Symbol) (v :: Type)
+class (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q) 
+instance (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol q) (k :: Symbol) (v :: q)
 
 {- | Constraint for maps that represent subsets of fields of 'Record'-like types.
 -}
-type ProductlikeSubset (subset :: Map Symbol Type) (whole :: Map Symbol Type) (flat :: [Type]) = 
+type ProductlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (flat :: [q]) = 
                        (KeysValuesAll (PresentIn whole) subset,
-                        Productlike '[] subset flat,
-                        SListI flat)
+                       Productlike '[] subset flat,
+                       SListI flat)
 
 {- | Like 'field', but targets multiple fields at the same time 
 -}
@@ -795,7 +814,7 @@ 
 {- | Constraint for maps that represent subsets of branches of 'Variant'-like types.
 -}
-type SumlikeSubset (subset :: Map Symbol Type) (whole :: Map Symbol Type) (subflat :: [Type]) (wholeflat :: [Type]) = 
+type SumlikeSubset (subset :: Map Symbol q) (whole :: Map Symbol q) (subflat :: [q]) (wholeflat :: [q]) = 
                    (KeysValuesAll (PresentIn whole) subset,
                     Productlike '[] whole  wholeflat,
                     Sumlike '[] whole  wholeflat,
@@ -854,7 +873,7 @@      in eliminate reducedCases 
 
 --
---
+
 -- Interaction with Data.SOP
 
 {- | Class from converting 'Record's to and from the n-ary product type 'NP' from "Data.SOP".
@@ -865,26 +884,38 @@ 
      The functions 'toNP' and 'fromNP' are usually easier to use. 
 -}
-class Productlike (start :: [Type])
-                  (t :: Map Symbol Type) 
-                  (result :: [Type]) | start t -> result, result t -> start where
-    prefixNP:: Record f t -> NP f start -> NP f result
-    breakNP :: NP f result -> (Record f t, NP f start)
+class Productlike (start :: [k])
+                  (t :: Map Symbol k) 
+                  (result :: [k]) | start t -> result, result t -> start where
+    _prefixNP:: Record f t -> NP f start -> NP f result
+    _breakNP :: NP f result -> (Record f t, NP f start)
 
 instance Productlike start E start where
-    prefixNP _ start = start  
-    breakNP start = (Empty, start) 
+    _prefixNP _ start = start  
+    _breakNP start = (Empty, start) 
 
 instance (Productlike start right middle, 
           Productlike (v ': middle) left result)
           => Productlike start (N color left k v right) result where
-    prefixNP (Node left fv right) start = 
-        prefixNP @_ @left @result left (fv :* prefixNP @start @right @middle right start)
-    breakNP result =
-        let (left, fv :* middle) = breakNP @_ @left @result result
-            (right, start) = breakNP @start @right middle
+    _prefixNP (Node left fv right) start = 
+        _prefixNP @_ @_ @left @result left (fv :* prefixNP @start @right @middle right start)
+    _breakNP result =
+        let (left, fv :* middle) = _breakNP @_ @_ @left @result result
+            (right, start) = _breakNP @_ @start @right middle
          in (Node left fv right, start)
 
+{- | 
+     Flattens a 'Record' and adds it to the initial part of the product.
+-}
+prefixNP:: forall start t result f. Productlike start t result => Record f t -> NP f start -> NP f result
+prefixNP = _prefixNP @_ @start @t @result
+
+{- | 
+     Reconstructs a 'Record' from the initial part of the product and returns the unconsumed part.
+-}
+breakNP :: forall start t result f. Productlike start t result => NP f result -> (Record f t, NP f start)
+breakNP = _breakNP @_ @start @t @result
+
 {- | Convert a 'Record' into a n-ary product. 
 -}
 toNP :: forall t result f. Productlike '[] t result => Record f t -> NP f result
@@ -903,19 +934,19 @@ 
      The functions 'toNS' and 'fromNS' are usually easier to use. 
 -}
-class Sumlike (start :: [Type]) 
-              (t :: Map Symbol Type) 
-              (result :: [Type]) | start t -> result, result t -> start where
-    prefixNS :: Either (NS f start) (Variant f t) -> NS f result
-    breakNS :: NS f result -> Either (NS f start) (Variant f t)
+class Sumlike (start :: [k]) 
+              (t :: Map Symbol k) 
+              (result :: [k]) | start t -> result, result t -> start where
+    _prefixNS :: Either (NS f start) (Variant f t) -> NS f result
+    _breakNS :: NS f result -> Either (NS f start) (Variant f t)
 
 instance Sumlike start 
                   (N color E k v E)
                   (v ': start) where
-    prefixNS = \case
+    _prefixNS = \case
         Left  l -> S l
         Right x -> case x of Here fv -> Z @_ @v @start fv
-    breakNS = \case 
+    _breakNS = \case 
         Z x -> Right (Here x)
         S x -> Left x
 
@@ -924,30 +955,30 @@          => Sumlike start 
                     (N color (N colorL leftL kL vL rightL) k v (N colorR leftR kR vR rightR)) 
                     result where
-    prefixNS = \case
+    _prefixNS = \case
         Left x -> 
-            prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S (prefixNS @_ @(N colorR leftR kR vR rightR) (Left x))))
+            _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Left x))))
         Right x -> 
-            case x of LookLeft x  -> prefixNS @(v ': middle) @(N colorL leftL kL vL rightL) @result (Right x) 
-                      Here x      -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (Z x))
-                      LookRight x -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S (prefixNS (Right x))))
-    breakNS ns = case breakNS @(v ': middle) @(N colorL leftL kL vL rightL) ns of
+            case x of LookLeft x  -> _prefixNS @_ @(v ': middle) @(N colorL leftL kL vL rightL) @result (Right x) 
+                      Here x      -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (Z x))
+                      LookRight x -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S (_prefixNS @_ (Right x))))
+    _breakNS ns = case _breakNS @_ @(v ': middle) @(N colorL leftL kL vL rightL) ns of
         Left x -> case x of
             Z x -> Right (Here x)
-            S x -> case breakNS @start @(N colorR leftR kR vR rightR) x of
+            S x -> case _breakNS @_ @start @(N colorR leftR kR vR rightR) x of
                 Left ns  -> Left ns
                 Right v  -> Right (LookRight v)
         Right v -> Right (LookLeft v)
 
 instance Sumlike (v ': start) (N colorL leftL kL vL rightL) result
          => Sumlike start (N color (N colorL leftL kL vL rightL) k v E) result where
-    prefixNS = \case
+    _prefixNS = \case
         Left x  -> 
-            prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S x))
+            _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (S x))
         Right x -> 
-            case x of LookLeft x  -> prefixNS @(v ': start) @(N colorL leftL kL vL rightL) @result (Right x)
-                      Here x      -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (Z x))
-    breakNS ns = case breakNS @(v ': start) @(N colorL leftL kL vL rightL) ns of
+            case x of LookLeft x  -> _prefixNS @_ @(v ': start) @(N colorL leftL kL vL rightL) @result (Right x)
+                      Here x      -> _prefixNS @_ @_ @(N colorL leftL kL vL rightL) (Left (Z x))
+    _breakNS ns = case _breakNS @_ @(v ': start) @(N colorL leftL kL vL rightL) ns of
         Left x -> case x of
             Z x -> Right (Here x)
             S x -> Left x 
@@ -955,17 +986,30 @@ 
 instance Sumlike start (N colorR leftR kR vR rightR) middle
          => Sumlike start (N color E k v (N colorR leftR kR vR rightR)) (v ': middle) where
-    prefixNS = \case
-        Left x  -> S (prefixNS @_ @(N colorR leftR kR vR rightR) (Left x))
+    _prefixNS = \case
+        Left x  -> S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Left x))
         Right x -> 
             case x of Here x      -> Z x
-                      LookRight x -> S (prefixNS @_ @(N colorR leftR kR vR rightR) (Right x))
-    breakNS = \case 
+                      LookRight x -> S (_prefixNS @_ @_ @(N colorR leftR kR vR rightR) (Right x))
+    _breakNS = \case 
         Z x -> Right (Here x)
-        S x -> case breakNS @_ @(N colorR leftR kR vR rightR) x of
+        S x -> case _breakNS @_ @_ @(N colorR leftR kR vR rightR) x of
             Left  ns     -> Left ns
             Right v      -> Right (LookRight v)
 
+{- | 
+    
+     Flattens a 'Variant' and adds it to the initial part of the sum.
+-}
+prefixNS :: forall start t result f. Sumlike start t result => Either (NS f start) (Variant f t) -> NS f result 
+prefixNS = _prefixNS @_ @start @t @result
+
+{- | 
+     Reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part.
+-}
+breakNS :: forall start t result f. Sumlike start t result => NS f result -> Either (NS f start) (Variant f t)
+breakNS = _breakNS @_ @start @t @result
+
 {- | Convert a 'Variant' into a n-ary sum. 
 -}
 toNS :: forall t result f. Sumlike '[] t result => Variant f t -> NS f result
@@ -1148,20 +1192,20 @@     DiscriminateBalL (N R _ _ _ _) _ = False
     DiscriminateBalL _             _ = True
 
-class BalanceableL (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
-    type BalL l k v r :: Map Symbol Type
+class BalanceableL (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where
+    type BalL l k v r :: Map Symbol q
     balLR :: Record f (N color l k v r) -> Record f (BalL l k v r)
     balLV :: Variant f (N color l k v r) -> Variant f (BalL l k v r)
 
-class BalanceableHelperL (b :: Bool) (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
-    type BalL' b l k v r :: Map Symbol Type
+class BalanceableHelperL (b :: Bool) (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where
+    type BalL' b l k v r :: Map Symbol q
     balLR' :: Record f (N color l k v r) -> Record f (BalL' b l k v r)
     balLV' :: Variant f (N color l k v r) -> Variant f (BalL' b l k v r)
 
 instance (DiscriminateBalL l r ~ b, BalanceableHelperL b l k v r) => BalanceableL l k v r where
     type BalL l k v r = BalL' (DiscriminateBalL l r) l k v r
-    balLR = balLR' @b @l @k @v @r
-    balLV = balLV' @b @l @k @v @r
+    balLR = balLR' @_ @b @l @k @v @r
+    balLV = balLV' @_ @b @l @k @v @r
 
 -- balleft :: RB a -> a -> RB a -> RB a
 -- balleft (T R a x b) y c = T R (T B a x b) y c
@@ -1182,8 +1226,8 @@     type BalL'         True t1 y yv (N B t2 z zv t3)     
                  =  Balance t1 y yv (N R t2 z zv t3)
     balLR' (Node left1 v1 (Node left2 v2 right2)) = 
-        balanceR @t1 @y @yv @(N R t2 z zv t3) (Node left1 v1 (Node left2 v2 right2))
-    balLV' v = balanceV @t1 @y @yv @(N R t2 z zv t3) (case v of
+        balanceR @_ @t1 @y @yv @(N R t2 z zv t3) (Node left1 v1 (Node left2 v2 right2))
+    balLV' v = balanceV @_ @t1 @y @yv @(N R t2 z zv t3) (case v of
         LookLeft l -> LookLeft l
         Here x -> Here x
         LookRight r -> LookRight (case r of
@@ -1197,14 +1241,14 @@     type BalL'         True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) =
                              N R (N B t1 y yv t2) u uv (Balance t3 z zv (N R l k kv r))          
     balLR' (Node left1 v1 (Node (Node left2 v2 right2) vx (Node left3 v3 right3))) = 
-            Node (Node left1 v1 left2) v2 (balanceR @t3 @z @zv @(N R l k kv r) (Node right2 vx (Node left3 v3 right3)))
+            Node (Node left1 v1 left2) v2 (balanceR @_ @t3 @z @zv @(N R l k kv r) (Node right2 vx (Node left3 v3 right3)))
     balLV' v = case v of LookLeft left1                          -> LookLeft (LookLeft left1)
                          Here v1                                 -> LookLeft (Here v1)
                          LookRight (LookLeft (LookLeft left2))   -> LookLeft (LookRight left2)
                          LookRight (LookLeft (Here v2))          -> Here v2
-                         LookRight (LookLeft (LookRight right2)) -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (LookLeft right2))
-                         LookRight (Here vx)                     -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (Here vx))
-                         LookRight (LookRight rr)                -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (LookRight (case rr of
+                         LookRight (LookLeft (LookRight right2)) -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (LookLeft right2))
+                         LookRight (Here vx)                     -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (Here vx))
+                         LookRight (LookRight rr)                -> LookRight (balanceV @_ @t3 @z @zv @(N R l k kv r) (LookRight (case rr of
                                                                         LookLeft left3 -> LookLeft left3
                                                                         Here v3 -> Here v3
                                                                         LookRight right3 -> LookRight right3)))
@@ -1218,20 +1262,20 @@     DiscriminateBalR _ (N R _ _ _ _) = False
     DiscriminateBalR _ _             = True
 
-class BalanceableR (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
-    type BalR l k v r :: Map Symbol Type
+class BalanceableR (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where
+    type BalR l k v r :: Map Symbol q
     balRR :: Record f (N color l k v r) -> Record f (BalR l k v r)
     balRV :: Variant f (N color l k v r) -> Variant f (BalR l k v r)
 
-class BalanceableHelperR (b :: Bool) (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
-    type BalR' b l k v r :: Map Symbol Type
+class BalanceableHelperR (b :: Bool) (l :: Map Symbol q) (k :: Symbol) (v :: q) (r :: Map Symbol q) where
+    type BalR' b l k v r :: Map Symbol q
     balRR' :: Record f (N color l k v r) -> Record f (BalR' b l k v r)
     balRV' :: Variant f (N color l k v r) -> Variant f (BalR' b l k v r)
 
 instance (DiscriminateBalR l r ~ b, BalanceableHelperR b l k v r) => BalanceableR l k v r where
     type BalR l k v r = BalR' (DiscriminateBalR l r) l k v r
-    balRR = balRR' @b @l @k @v @r
-    balRV = balRV' @b @l @k @v @r
+    balRR = balRR' @_ @b @l @k @v @r
+    balRV = balRV' @_ @b @l @k @v @r
 
 -- balright :: RB a -> a -> RB a -> RB a
 -- balright a x (T R b y c) = T R a x (T B b y c)
@@ -1250,9 +1294,9 @@     BalanceableHelperR True (N B t2 z zv t3) y yv t1 where
     type BalR'         True (N B t2 z zv t3) y yv t1     
              =  Balance (N R t2 z zv t3) y yv t1
-    balRR' (Node (Node left1 v1 right1) v2 right2) = balanceR @(N R t2 z zv t3) @y @yv @t1 
+    balRR' (Node (Node left1 v1 right1) v2 right2) = balanceR @_ @(N R t2 z zv t3) @y @yv @t1 
            (Node (Node left1 v1 right1) v2 right2)
-    balRV' v = balanceV @(N R t2 z zv t3) @y @yv @t1 (case v of
+    balRV' v = balanceV @_ @(N R t2 z zv t3) @y @yv @t1 (case v of
         LookLeft l -> LookLeft (case l of 
             LookLeft l' -> LookLeft l'
             Here x' -> Here x'
@@ -1266,14 +1310,14 @@     type BalR'         True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 =
                              N R (Balance (N R t2 u uv t3) z zv l) k kv (N B r y yv t1) 
     balRR' (Node (Node (Node left2 v2 right2) vx (Node left3 v3 right3)) v1 left1) = 
-            Node (balanceR @(N R t2 u uv t3) @z @zv @l (Node (Node left2 v2 right2) vx left3)) v3 (Node right3 v1 left1)
+            Node (balanceR @_ @(N R t2 u uv t3) @z @zv @l (Node (Node left2 v2 right2) vx left3)) v3 (Node right3 v1 left1)
     balRV' v = case v of
-        LookLeft  (LookLeft rr)                 -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (LookLeft (case rr of
+        LookLeft  (LookLeft rr)                 -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (LookLeft (case rr of
                                                         LookLeft t2 -> LookLeft t2
                                                         Here uv -> Here uv
                                                         LookRight t3 -> LookRight t3)))
-        LookLeft  (Here zv)                     -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (Here zv))
-        LookLeft  (LookRight (LookLeft l))      -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (LookRight l))
+        LookLeft  (Here zv)                     -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (Here zv))
+        LookLeft  (LookRight (LookLeft l))      -> LookLeft (balanceV @_ @(N R t2 u uv t3) @z @zv @l (LookRight l))
         LookLeft  (LookRight (Here kv))         -> Here kv
         LookLeft  (LookRight (LookRight r))     -> LookRight (LookLeft r)
         Here      yv                            -> LookRight (Here yv) 
@@ -1294,8 +1338,8 @@ -- app (T R a x b) c = T R a x (app b c)
 
 
-class Fuseable (l :: Map Symbol Type) (r :: Map Symbol Type) where
-    type Fuse l r :: Map Symbol Type
+class Fuseable (l :: Map Symbol q) (r :: Map Symbol q) where
+    type Fuse l r :: Map Symbol q
     fuseRecord :: Record f l -> Record f r -> Record f (Fuse l r)
     fuseVariant :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)
 
@@ -1322,14 +1366,14 @@ instance Fuseable (N B left1 k1 v1 right1) left2 
     => Fuseable (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) where
     type Fuse   (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (Fuse (N B left1 k1 v1 right1) left2) k2 v2 right2
-    fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node (fuseRecord @(N B left1 k1 v1 right1) (Node left1 v1 right1) left2) v2 right2 
+    fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node (fuseRecord @_ @(N B left1 k1 v1 right1) (Node left1 v1 right1) left2) v2 right2 
     fuseVariant e = case e of 
         Left l  -> case l of
-            LookLeft left1   -> LookLeft  (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (LookLeft left1)))
-            Here v1          -> LookLeft  (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (Here v1)))
-            LookRight right1 -> LookLeft  (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (LookRight right1)))
+            LookLeft left1   -> LookLeft  (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (LookLeft left1)))
+            Here v1          -> LookLeft  (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (Here v1)))
+            LookRight right1 -> LookLeft  (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Left (LookRight right1)))
         Right r -> case r of
-            LookLeft left2   -> LookLeft  (fuseVariant @(N B left1 k1 v1 right1) @left2 (Right left2))
+            LookLeft left2   -> LookLeft  (fuseVariant @_ @(N B left1 k1 v1 right1) @left2 (Right left2))
             Here v2          -> Here      v2
             LookRight right2 -> LookRight right2
 
@@ -1338,27 +1382,27 @@ instance Fuseable right1 (N B left2 k2 v2 right2) 
     => Fuseable (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) where
     type Fuse   (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R left1 k1 v1 (Fuse right1 (N B left2 k2 v2 right2))
-    fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (fuseRecord @_ @(N B left2 k2 v2 right2) right1 (Node left2 v2 right2))
+    fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (fuseRecord @_ @_ @(N B left2 k2 v2 right2) right1 (Node left2 v2 right2))
     fuseVariant e = case e of
         Left l  -> case l of
             LookLeft left1   -> LookLeft left1
             Here v1          -> Here v1
-            LookRight right1 -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Left right1))
+            LookRight right1 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Left right1))
         Right r -> case r of
-            LookLeft left2   -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (LookLeft left2)))
-            Here v2          -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (Here v2)))
-            LookRight right2 -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (LookRight right2)))
+            LookLeft left2   -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (LookLeft left2)))
+            Here v2          -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (Here v2)))
+            LookRight right2 -> LookRight (fuseVariant @_ @right1 @(N B left2 k2 v2 right2) (Right (LookRight right2)))
 
 
 -- app (T R a x b) (T R c y d) =
 instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper1 fused (N R left1 k1 v1 right1) (N R left2 k2 v2 right2)) 
     => Fuseable (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where
     type Fuse   (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = Fuse1 (Fuse right1 left2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) 
-    fuseRecord = fuseRecord1 @(Fuse right1 left2) 
-    fuseVariant = fuseVariant1 @(Fuse right1 left2)
+    fuseRecord = fuseRecord1 @_ @(Fuse right1 left2) 
+    fuseVariant = fuseVariant1 @_ @(Fuse right1 left2)
 
-class FuseableHelper1 (fused :: Map Symbol Type) (l :: Map Symbol Type) (r :: Map Symbol Type) where
-    type Fuse1 fused l r :: Map Symbol Type
+class FuseableHelper1 (fused :: Map Symbol q) (l :: Map Symbol q) (r :: Map Symbol q) where
+    type Fuse1 fused l r :: Map Symbol q
     fuseRecord1 :: Record f l -> Record f r -> Record f (Fuse l r)
     fuseVariant1 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)
 
@@ -1377,12 +1421,12 @@             Left l  -> case l of
                             LookLeft  left1  -> LookLeft (LookLeft left1)
                             Here      v1     -> LookLeft (Here v1)
-                            LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
+                            LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of
                                                     LookLeft s1  -> LookLeft (LookRight s1)
                                                     Here zv      -> Here zv
                                                     LookRight s2 -> LookRight (LookLeft s2)
             Right r -> case r of 
-                            LookLeft  left2  -> case fuseVariant @right1 @left2 (Right left2) of
+                            LookLeft  left2  -> case fuseVariant @_ @right1 @left2 (Right left2) of
                                                     LookLeft s1  -> LookLeft (LookRight s1)
                                                     Here zv      -> Here zv
                                                     LookRight s2 -> LookRight (LookLeft s2)
@@ -1406,12 +1450,12 @@             Left l  -> case l of
                             LookLeft  left1  -> LookLeft left1
                             Here      v1     -> Here v1
-                            LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
+                            LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of
                                                     LookLeft s1  -> LookRight (LookLeft (LookLeft s1))
                                                     Here zv      -> LookRight (LookLeft (Here zv))
                                                     LookRight s2 -> LookRight (LookLeft (LookRight s2))
             Right r -> case r of 
-                            LookLeft  left2  -> case fuseVariant @right1 @left2 (Right left2) of
+                            LookLeft  left2  -> case fuseVariant @_ @right1 @left2 (Right left2) of
                                                     LookLeft s1  -> LookRight (LookLeft (LookLeft s1))
                                                     Here zv      -> LookRight (LookLeft (Here zv))
                                                     LookRight s2 -> LookRight (LookLeft (LookRight s2))
@@ -1438,12 +1482,12 @@ instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper2 fused (N B left1 k1 v1 right1) (N B left2 k2 v2 right2)) 
     => Fuseable (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where
     type Fuse   (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = Fuse2 (Fuse right1 left2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) 
-    fuseRecord = fuseRecord2 @(Fuse right1 left2) 
-    fuseVariant = fuseVariant2 @(Fuse right1 left2)
+    fuseRecord = fuseRecord2 @_ @(Fuse right1 left2) 
+    fuseVariant = fuseVariant2 @_ @(Fuse right1 left2)
 
 -- could FuseableHelper1 and FuseableHelper2 be, well... fused?
-class FuseableHelper2 (fused :: Map Symbol Type) (l :: Map Symbol Type) (r :: Map Symbol Type) where
-    type Fuse2 fused l r :: Map Symbol Type
+class FuseableHelper2 (fused :: Map Symbol q) (l :: Map Symbol q) (r :: Map Symbol q) where
+    type Fuse2 fused l r :: Map Symbol q
     fuseRecord2 :: Record f l -> Record f r -> Record f (Fuse l r)
     fuseVariant2 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)
 
@@ -1461,12 +1505,12 @@             Left l  -> case l of
                             LookLeft  left1  -> LookLeft (LookLeft left1)
                             Here      v1     -> LookLeft (Here v1)
-                            LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
+                            LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of
                                                     LookLeft s1  -> LookLeft (LookRight s1)
                                                     Here zv      -> Here zv
                                                     LookRight s2 -> LookRight (LookLeft s2)
             Right r -> case r of 
-                            LookLeft  left2  -> case fuseVariant @right1 @left2 (Right left2) of
+                            LookLeft  left2  -> case fuseVariant @_ @right1 @left2 (Right left2) of
                                                     LookLeft s1  -> LookLeft (LookRight s1)
                                                     Here zv      -> Here zv
                                                     LookRight s2 -> LookRight (LookLeft s2)
@@ -1481,18 +1525,18 @@     => FuseableHelper2 (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where
     type Fuse2         (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = BalL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2)
     fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) = 
-        case fuseRecord @right1 @left2 right1 left2 of
-            Node s1 zv s2 -> balLR @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (Node left1 v1 (Node (Node s1 zv s2) v2 right2))
-    fuseVariant2 e = balLV @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (case e of
+        case fuseRecord @_ @right1 @left2 right1 left2 of
+            Node s1 zv s2 -> balLR @_ @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (Node left1 v1 (Node (Node s1 zv s2) v2 right2))
+    fuseVariant2 e = balLV @_ @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (case e of
             Left l  -> case l of
                             LookLeft  left1  -> LookLeft left1
                             Here      v1     -> Here v1
-                            LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
+                            LookRight right1 -> case fuseVariant @_ @right1 @left2 (Left right1) of
                                                     LookLeft s1  -> LookRight (LookLeft (LookLeft s1))
                                                     Here zv      -> LookRight (LookLeft (Here zv))
                                                     LookRight s2 -> LookRight (LookLeft (LookRight s2))
             Right r -> case r of 
-                            LookLeft  left2  -> case fuseVariant @right1 @left2 (Right left2) of
+                            LookLeft  left2  -> case fuseVariant @_ @right1 @left2 (Right left2) of
                                                     LookLeft s1  -> LookRight (LookLeft (LookLeft s1))
                                                     Here zv      -> LookRight (LookLeft (Here zv))
                                                     LookRight s2 -> LookRight (LookLeft (LookRight s2))
@@ -1507,8 +1551,8 @@     => FuseableHelper2 E (N B left1 k1 v1 E) (N B E k2 v2 right2) where
     type Fuse2         E (N B left1 k1 v1 E) (N B E k2 v2 right2) = BalL left1 k1 v1 (N B E k2 v2 right2)
     fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) = 
-            balLR @left1 @k1 @v1 @(N B E k2 v2 right2) (Node left1 v1 (Node Empty v2 right2))
-    fuseVariant2 e = balLV @left1 @k1 @v1 @(N B E k2 v2 right2) (case e of
+            balLR @_ @left1 @k1 @v1 @(N B E k2 v2 right2) (Node left1 v1 (Node Empty v2 right2))
+    fuseVariant2 e = balLV @_ @left1 @k1 @v1 @(N B E k2 v2 right2) (case e of
             Left l  -> case l of
                             LookLeft  left1  -> LookLeft left1
                             Here      v1     -> Here v1
@@ -1522,16 +1566,16 @@ --      | x<y = delformLeft a y b
 --      | x>y = delformRight a y b
 --      | otherwise = app a b
-class Delable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
-    type Del k v t :: Map Symbol Type
+class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
+    type Del k v t :: Map Symbol q
     del :: Record f t -> Record f (Del k v t)
     win :: Variant f t -> Either (Variant f (Del k v t)) (f v) 
 
 --  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
 --  delformLeft a y b = T R (del a) y b
 --  In the term-level code, the k to delete is already on the environment.
-class DelableL (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
-    type DelL k v l kx vx r :: Map Symbol Type
+class DelableL (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where
+    type DelL k v l kx vx r :: Map Symbol q
     delL :: Record f (N color l kx vx r) -> Record f (DelL k v l kx vx r)
     winL :: Variant f (N color l kx vx r) -> Either (Variant f (DelL k v l kx vx r)) (f v) 
 
@@ -1539,9 +1583,9 @@ instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableL deleted kx vx right) 
     => DelableL k v (N B leftz kz vz rightz) kx vx right where
     type DelL   k v (N B leftz kz vz rightz) kx vx right = BalL (Del k v (N B leftz kz vz rightz)) kx vx right
-    delL (Node left vx right) = balLR @(Del k v (N B leftz kz vz rightz)) @kx @vx @right (Node (del @k @v left) vx right)
-    winL v = first (balLV @(Del k v (N B leftz kz vz rightz)) @kx @vx @right) (case v of
-        LookLeft l -> first LookLeft (win @k @v l)
+    delL (Node left vx right) = balLR @_ @(Del k v (N B leftz kz vz rightz)) @kx @vx @right (Node (del @_ @k @v left) vx right)
+    winL v = first (balLV @_ @(Del k v (N B leftz kz vz rightz)) @kx @vx @right) (case v of
+        LookLeft l -> first LookLeft (win @_ @k @v l)
         Here vx -> Left $ Here vx
         LookRight r -> Left $ LookRight r)
 
@@ -1549,9 +1593,9 @@ instance (Delable k v (N R leftz kz vz rightz)) 
     => DelableL k v (N R leftz kz vz rightz) kx vx right where
     type DelL   k v (N R leftz kz vz rightz) kx vx right = N R (Del k v (N R leftz kz vz rightz)) kx vx right
-    delL (Node left vx right) = Node (del @k @v left) vx right
+    delL (Node left vx right) = Node (del @_ @k @v left) vx right
     winL v = case v of
-        LookLeft l -> first LookLeft (win @k @v l)
+        LookLeft l -> first LookLeft (win @_ @k @v l)
         Here vx -> Left (Here vx)
         LookRight r -> Left (LookRight r)
 
@@ -1565,8 +1609,8 @@ 
 --  delformRight a y b@(T B _ _ _) = balright a y (del b)
 --  delformRight a y b = T R a y (del b)
-class DelableR (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
-    type DelR k v l kx vx r :: Map Symbol Type
+class DelableR (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where
+    type DelR k v l kx vx r :: Map Symbol q
     delR :: Record f (N color l kx vx r) -> Record f (DelR k v l kx vx r)
     winR :: Variant f (N color l kx vx r) -> Either (Variant f (DelR k v l kx vx r)) (f v) 
 
@@ -1574,21 +1618,21 @@ instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableR left kx vx deleted) 
     => DelableR k v left kx vx (N B leftz kz vz rightz) where
     type DelR   k v left kx vx (N B leftz kz vz rightz) = BalR left kx vx (Del k v (N B leftz kz vz rightz))
-    delR (Node left vx right) = balRR @left @kx @vx @(Del k v (N B leftz kz vz rightz)) (Node left vx (del @k @v right))
-    winR v = first (balRV @left @kx @vx @(Del k v (N B leftz kz vz rightz))) (case v of
+    delR (Node left vx right) = balRR @_ @left @kx @vx @(Del k v (N B leftz kz vz rightz)) (Node left vx (del @_ @k @v right))
+    winR v = first (balRV @_ @left @kx @vx @(Del k v (N B leftz kz vz rightz))) (case v of
         LookLeft l -> Left $ LookLeft l
         Here vx -> Left $ Here vx
-        LookRight r -> first LookRight (win @k @v r))
+        LookRight r -> first LookRight (win @_ @k @v r))
 
 --  delformRight a y b = T R a y (del b)
 instance (Delable k v (N R leftz kz vz rightz)) 
     => DelableR k v left kx vx (N R leftz kz vz rightz) where
     type   DelR k v left kx vx (N R leftz kz vz rightz) = N R left kx vx (Del k v (N R leftz kz vz rightz))
-    delR (Node left vx right) = Node left vx (del @k @v right)
+    delR (Node left vx right) = Node left vx (del @_ @k @v right)
     winR v = case v of
         LookLeft l -> Left (LookLeft l)
         Here vx -> Left (Here vx)
-        LookRight r -> first LookRight (win @k @v r)
+        LookRight r -> first LookRight (win @_ @k @v r)
 
 --  delformRight a y b = T R a y (del b)
 instance DelableR k v left kx vx E where
@@ -1611,36 +1655,36 @@ --      | otherwise = app a b
 instance (CmpSymbol kx k ~ ordering, DelableHelper ordering k v left kx vx right) => Delable k v (N color left kx vx right) where
     type Del k v (N color left kx vx right) = Del' (CmpSymbol kx k) k v left kx vx right
-    del = del' @(CmpSymbol kx k) @k @v @left @kx @vx @right
-    win = win' @(CmpSymbol kx k) @k @v @left @kx @vx @right
+    del = del' @_ @(CmpSymbol kx k) @k @v @left @kx @vx @right
+    win = win' @_ @(CmpSymbol kx k) @k @v @left @kx @vx @right
 
-class DelableHelper (ordering :: Ordering) (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
-    type Del' ordering k v l kx vx r :: Map Symbol Type
+class DelableHelper (ordering :: Ordering) (k :: Symbol) (v :: q) (l :: Map Symbol q) (kx :: Symbol) (vx :: q) (r :: Map Symbol q) where
+    type Del' ordering k v l kx vx r :: Map Symbol q
     del' :: Record f (N color l kx vx r) -> Record f (Del' ordering k v l kx vx r)
     win' :: Variant f (N color l kx vx r) -> Either (Variant f (Del' ordering k v l kx vx r)) (f v) 
 
 --      | x<y = delformLeft a y b
 instance DelableL k v left kx vx right => DelableHelper GT k v left kx vx right where
     type Del'                                           GT k v left kx vx right = DelL k v left kx vx right
-    del' = delL @k @v @left @kx @vx @right  
-    win' = winL @k @v @left @kx @vx @right  
+    del' = delL @_ @k @v @left @kx @vx @right  
+    win' = winL @_ @k @v @left @kx @vx @right  
 
 --      | otherwise = app a b
 instance Fuseable left right => DelableHelper EQ k v left k v right where
     type Del'                                 EQ k v left k v right = Fuse left right
-    del' (Node left _ right) = fuseRecord @left @right left right 
+    del' (Node left _ right) = fuseRecord @_ @left @right left right 
     win' v = case v of
-        LookLeft l  ->  Left $ fuseVariant @left @right (Left l)
+        LookLeft l  ->  Left $ fuseVariant @_ @left @right (Left l)
         Here v      -> Right v 
-        LookRight r -> Left $ fuseVariant @left @right (Right r)
+        LookRight r -> Left $ fuseVariant @_ @left @right (Right r)
 
 --      | x>y = delformRight a y b
 instance DelableR k v left kx vx right => DelableHelper LT k v left kx vx right where
     type Del'                                           LT k v left kx vx right = DelR k v left kx vx right
-    del' = delR @k @v @left @kx @vx @right  
-    win' = winR @k @v @left @kx @vx @right  
+    del' = delR @_ @k @v @left @kx @vx @right  
+    win' = winR @_ @k @v @left @kx @vx @right  
 
-{- | Class that determines if the pair of a 'Symbol' key and a 'Type' can
+{- | Class that determines if the pair of a 'Symbol' key and a type can
      be deleted from a type-level map.
  
      The associated type family 'Delete' produces the resulting map.
@@ -1651,19 +1695,31 @@      reduced 'Variant' if there isn't. 'winnow' tends to be more useful in
      practice.
 
-     If the map already has the key but with a /different/ 'Type', the deletion
+     If the map already has the key but with a /different/ type, the deletion
      fails to compile.
  -}
-class Deletable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
-    type Delete k v t :: Map Symbol Type
-    delete :: Record f t -> Record f (Delete k v t)
-    winnow :: Variant f t -> Either (Variant f (Delete k v t)) (f v) 
+class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
+    type Delete k v t :: Map Symbol q
+    _delete :: Record f t -> Record f (Delete k v t)
+    _winnow :: Variant f t -> Either (Variant f (Delete k v t)) (f v) 
 
 instance (Delable k v t, Del k v t ~ deleted, CanMakeBlack deleted) => Deletable k v t where
     type Delete k v t = MakeBlack (Del k v t)
-    delete r = makeBlackR (del @k @v r) 
-    winnow v = first makeBlackV (win @k @v v)
+    _delete r = makeBlackR (del @_ @k @v r) 
+    _winnow v = first makeBlackV (win @_ @k @v v)
 
+{- | 
+     Removes a field from a 'Record'.
+ -}
+delete :: forall k v t f . Deletable k v t => Record f t -> Record f (Delete k v t)
+delete = _delete @_ @k @v @t
+
+{- | 
+     Checks if a 'Variant' is of a given branch and returns the value in the
+     branch if there's a match, or a reduced 'Variant' if there isn't. 
+ -}
+winnow :: forall k v t f . Deletable k v t => Variant f t -> Either (Variant f (Delete k v t)) (f v)
+winnow = _winnow @_ @k @v @t 
 
 {- | Like 'winnow' but specialized to pure 'Variant's.
 -}

@@ -1,17 +1,18 @@ cabal-version:       2.0
 name:                red-black-record
-version:             2.0.4.0
+version:             2.1.0.0
 synopsis:            Extensible records and variants indexed by a type-level Red-Black tree.
 
 description:         A library that provides extensible records and variants,
                      both indexed by a type-level red-black tree that maps
-                     Symbol keys to value Types. 
+                     Symbol keys to value types of any kind. 
                      .
                      The keys correspond to fields
                      names in records, and to branch names in variants.
                      . 
-                     Each value type in a field or branch comes wrapped in a
-                     type constructor of kind @Type -> Type@. 
+                     At the term level, value types come wrapped in a type
+                     constructor of kind `q -> Type`, where `q` is the kind of
+                     value types.
                      .
                      The records and variants can be converted to and from
                      regular Haskell datatypes; also to and from the unlabelled
@@ -59,7 +60,7 @@                        bytestring           >= 0.10,
                        text                 >= 1.1,
                        profunctors          >= 5,
-                       doctest              >= 0.16
+                       doctest              >= 0.16.2
   default-language:    Haskell2010
 
 test-suite tests

@@ -18,8 +18,8 @@ import Data.SOP
 import Data.SOP.NP (cpure_NP,collapse_NP)
 import Data.Typeable
-import GHC.TypeLits
 import Data.Proxy
+import GHC.TypeLits
 import Data.Kind
 import GHC.Generics (Generic)
 
@@ -62,6 +62,10 @@                                     testCase "tandem02" testInTandem02,
                                     testCase "tandem03" testInTandem03,
                                     testCase "tandem04" testInTandem04
+                            ],
+                            testGroup "polyKindedMap" [
+                                    testCase "polyKinded01" polyKinded01,
+                                    testCase "polyKinded02" polyKinded02
                             ]
                           ]
 
@@ -505,4 +509,47 @@ perform = foldr (\(Act iod s v) t -> case iod of In -> t_insert s v t
                                                  De -> t_delete s t) 
                 emptyMap
+
+--
+--
+--
+
+type PolyKinded01 = FromList '[ '("aaa","v1"),
+                                '("bbb","v2"), 
+                                '("ccc","v3"), 
+                                '("ddd","v4"), 
+                                '("eee","v5")  ]
+
+polyKindedRecord01 :: Record Proxy PolyKinded01
+polyKindedRecord01 = 
+               insert @"aaa" (Proxy @"v1")
+             . insert @"bbb" (Proxy @"v2")
+             . insert @"ccc" (Proxy @"v3")
+             . insert @"ddd" (Proxy @"v4")
+             . insert @"eee" (Proxy @"v5")
+             $ unit
+
+polyKinded01 :: Assertion
+polyKinded01 = do
+    let r = insert @"aaa" (Proxy @"v1")
+          . insert @"bbb" (Proxy @"v2")
+          . insert @"ccc" (Proxy @"v3")
+          . insert @"ddd" (Proxy @"v4")
+          . insert @"eee" (Proxy @"v5")
+          . insert @"abb" (Proxy @"v2")
+          . insert @"acc" (Proxy @"v3")
+          . insert @"add" (Proxy @"v4")
+          . insert @"aee" (Proxy @"v5")
+          $ unit
+        proxy :: Proxy "v2"
+        proxy = getField @"abb" r
+    return ()
+
+polyKinded02 :: Assertion
+polyKinded02 = do
+    let r = demoteEntries @PolyKinded01
+        K (_,trep) = getField @"eee" r
+    assertEqual "" trep (typeRep (Proxy @"v5"))
+    return ()
+