packages feed

generic-labels (empty) → 0.1.0.1

raw patch · 22 files changed

+1713/−0 lines, 22 filesdep +Cabaldep +basedep +generic-labels

Dependencies added: Cabal, base, generic-labels, generic-lens-core, inspection-testing

Files

+ changelog.md view
@@ -0,0 +1,5 @@+# Changelog for package `generic-labels`
+
+## 0.1.0.1 ( February 09, 2020 )
+
+* Initial release
+ generic-labels.cabal view
@@ -0,0 +1,141 @@+cabal-version: 3.0
+name:          generic-labels
+version:       0.1.0.1
+author:        Sam Derbyshire
+maintainer:    Sam Derbyshire
+build-type:    Simple
+license:       BSD-3-Clause
+homepage:      https://github.com/sheaf/generic-labels
+bug-reports:   https://github.com/sheaf/generic-labels/issues
+category:      Data, Generics, Records
+extra-source-files:
+  changelog.md
+
+synopsis: Generically extract and replace collections of record fields
+
+description:
+
+  Handle various conversion operations between record types,
+  such as projecting out a collection of fields from a record,
+  or plugging in values for a subset of the fields of a larger record.
+
+  Works both with built-in Haskell records, as well as explicitly labelled types
+  @ ( #label := value ) :: ( "label" := Type ) @.
+
+  Project out a smaller record using @project@:
+  
+  @
+    data IBXD x = IBXD { i :: Int, b :: Bool, x :: x, d :: Double }
+      deriving stock Generic
+    data XI x = XI { x :: c, i :: Int }
+      deriving stock Generic
+  @
+  
+  Plug in a subset of fields using @inject@:
+
+  @
+    xi_into_ibxd :: XI x -> IBXD x -> IBXD x
+    xi_into_ibxd = inject
+  @
+  
+  Create a record out of two collections of arguments using @adapt@:
+  
+  @
+    xi_plus_bd_makes_ibxd :: XI x -> ( "b" := Bool, "d" := Double ) -> IBXD x
+    xi_plus_bd_makes_ibxd = adapt
+  @
+
+  See also the library's [readme](https://github.com/sheaf/generic-labels/blob/master/readme.md).
+
+source-repository head
+  type:     git
+  location: git://github.com/sheaf/generic-labels
+
+common common
+
+  build-depends:
+    base
+      >= 4.14 && < 4.17
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall
+    -Wcompat
+    -Wno-unticked-promoted-constructors
+
+  default-extensions:
+    DataKinds
+    DerivingStrategies
+    FlexibleContexts
+    FlexibleInstances
+    FunctionalDependencies
+    NoStarIsType
+    PatternSynonyms
+    PolyKinds
+    ScopedTypeVariables
+    --StandaloneKindSignatures -- currently unsupported by hackage
+    TypeApplications
+    TypeFamilyDependencies
+    TypeOperators
+
+common generic-lens-core
+
+  build-depends:
+    generic-lens-core
+      >= 2.0 && < 2.2
+
+library
+
+  import:
+    common, generic-lens-core
+
+  hs-source-dirs:
+    src
+
+  exposed-modules:
+    Data.Generic.Labels
+    Data.Generic.Labels.Internal
+    Data.Generic.Labels.Internal.Errors
+    Data.Label
+
+  other-modules:
+    Data.Type.Error
+    Data.Type.List
+    Data.Type.Maybe
+    Data.Type.Multiplicity
+
+test-suite generic-labels-test
+
+  import:
+    common
+
+  type:
+    detailed-0.9
+
+  build-depends:
+    , generic-labels
+    , Cabal
+        >= 3.0 && < 3.5
+    , inspection-testing
+        >= 0.4 && < 0.5
+
+  hs-source-dirs:
+    test
+
+  test-module:
+    Inspection
+
+  other-modules:
+    ShouldCompile.Adapt.RRR
+    ShouldCompile.Adapt.TTR
+    ShouldCompile.Adapt.TTT
+    ShouldCompile.Adapt.SingletonArg
+    ShouldCompile.Adapt.SingletonArgOpt
+    ShouldCompile.Adapt.SingletonOpt
+    ShouldCompile.Inject.Basic
+    ShouldCompile.Project.Basic
+    ShouldCompile.Project.PolymorphicR
+    ShouldCompile.Project.PolymorphicT
+
+ src/Data/Generic/Labels.hs view
@@ -0,0 +1,280 @@+{-# LANGUAGE UndecidableInstances #-}
+
+{-|
+Module: Data.Generic.Labels
+Description: Convert between collections of fields using generics.
+
+This module provides functionality for converting between different collections of fields.
+
+== Projections
+
+To project out certain fields of a record, use 'project'.
+
+For instance:
+
+@
+data IBXD x = IBXD { i :: Int, b :: Bool, x :: x, d :: Double }
+  deriving stock Generic
+data XI x = XI { x :: c, i :: Int }
+  deriving stock Generic
+@
+
+We can project out the two fields of interest from the first record type:
+
+@
+ibxd_to_xi :: IBXD x -> XI x
+ibxd_to_xi = project
+@
+
+== Injections
+
+Going the other way, we can use 'inject' to override fields of the larger record
+with those from the smaller record:
+
+@
+xi_into_ibxd :: XI x -> IBXD x -> IBXD x
+xi_into_ibxd = inject
+@
+
+== Adapters
+
+'project' and 'inject' are two instances of the more general 'adapt' function,
+which allows us to only specify the missing arguments in the above example.
+
+@
+xi_plus_bd_makes_ibxd :: XI x -> ( "b" := Bool, "d" := Double ) -> IBXD x
+xi_plus_bd_makes_ibxd = adapt
+@
+
+In this situation, we are building up a record of type @IBXD x@ out of two parts.
+
+More generally, `adapt` allows for fields in the first argument to override
+fields in the second argument, which provides a convenient mechanism for
+named optional arguments.
+
+@
+adapt :: _ => givenArgs -> optionalArgs -> allArgs
+@
+
+For instance, if we have a function @f@ which takes in several named arguments
+
+@
+type AllArgsTuple = ( "arg1" := Ty1, "arg2" := Ty2, "arg3" := Ty3, "arg4" := Ty4 ) 
+
+f :: AllArgsTuple -> r
+@
+
+and we have default values for some of those arguments, e.g.
+
+@
+type DefaultArgsTuple = ( "arg2" := Ty2, "arg3" := Ty3 )
+
+f_defaults :: DefaultArgsTuple
+f_defaults = ( #arg2 := val2, #arg3 := val3 )
+@
+
+then we can create a corresponding function @f_defaulting@,
+which allows user to only pass the remaining (required) arguments:
+
+@
+f_defaulting
+  :: CheckedAdapt args DefaultArgsTuple AllArgsTuple => args -> r
+f_defaulting args = adapt args f_defaults
+@
+
+-}
+
+module Data.Generic.Labels
+  (
+  -- * Converting between collections of fields
+    Adapt(..), Inject(..), Project(..)
+
+  -- * Re-export of labelling functionality from "Data.Label"
+  , (:=)(..)
+
+  -- * Unchecked functions (can behave unpredictably).
+  , UncheckedAdapt(..), UncheckedInject(..), UncheckedProject(..)
+  )
+  where
+
+-- base
+import GHC.Generics
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels.Internal
+  ( GAdapt
+    ( gAdapt )
+  )
+import Data.Generic.Labels.Internal.Errors
+  ( CheckAdapt, CheckInject, CheckProject )
+
+--------------------------------------------------------------------------------
+
+class UncheckedAdapt args opt all where
+  -- | Create an adapter, without extra type-level validation.
+  --
+  -- Unchecked uses (e.g. presence of duplicate fields)
+  -- can throw abstruse compile-time error messages
+  -- or produce unexpected results at runtime.
+  --
+  -- Prefer using 'adapt' whenever possible.
+  uncheckedAdapt :: args -> opt -> all
+
+instance {-# OVERLAPPING #-} UncheckedAdapt a a a where
+  uncheckedAdapt = const
+instance {-# OVERLAPPING #-} UncheckedAdapt a opt a where
+  uncheckedAdapt = const
+instance {-# OVERLAPPING #-} ( a ~ b )
+       => UncheckedAdapt ( lbl := a ) opt ( lbl := b ) where
+  uncheckedAdapt = const
+instance {-# OVERLAPPING #-} ( a ~ b, o ~ b )
+       => UncheckedAdapt ( lbl := a ) ( lbl := o ) ( lbl := b ) where
+  uncheckedAdapt = const
+
+instance {-# OVERLAPPING #-}
+    ( Generic all
+    , argFld ~ S1 ( MetaSel ( Just lbl1 ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 a )
+    , optFld ~ S1 ( MetaSel ( Just lbl2 ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 o )
+    , GAdapt argFld optFld ( Rep all )
+    )
+  => UncheckedAdapt ( lbl1 := a ) ( lbl2 := o ) all where
+  uncheckedAdapt ( _ := arg ) ( _ := opt ) =
+    to $ gAdapt ( M1 ( K1 arg ) :: argFld x ) ( M1 ( K1 opt ) :: optFld x )
+
+instance
+    ( Generic opt, Generic all
+    , argFld ~ S1 ( MetaSel ( Just lbl ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 a )
+    , GAdapt argFld ( Rep opt ) ( Rep all )
+    )
+  => UncheckedAdapt ( lbl := a ) opt all where
+  uncheckedAdapt ( _ := arg ) opt =
+    to $ gAdapt ( M1 ( K1 arg ) :: argFld x ) ( from opt )
+
+instance {-# OVERLAPPING #-}
+    ( Generic args, Generic all
+    , optFld ~ S1 ( MetaSel ( Just lbl ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 o )
+    , GAdapt ( Rep args ) optFld ( Rep all )
+    )
+  => UncheckedAdapt args ( lbl := o ) all where
+  uncheckedAdapt args ( _ := opt ) =
+    to $ gAdapt ( from args ) ( M1 ( K1 opt ) :: optFld x )
+
+instance {-# OVERLAPPABLE #-}
+    ( Generic args, Generic opt, Generic all
+    , GAdapt ( Rep args ) ( Rep opt ) ( Rep all )
+    )
+  => UncheckedAdapt args opt all where
+  uncheckedAdapt args opt =
+    to $ gAdapt ( from args ) ( from opt )
+
+class    ( UncheckedAdapt args opt all ) => Adapt args opt all where
+  -- | Create an adapter, to inject a smaller type into a larger one,
+  -- providing defaults for optional values.
+  --
+  -- @
+  --   myAdapt :: ( "i" := Int, "f" := Float ) -> ( "f" := Float, "b" := Bool, "i" := Int )
+  --   myAdapt args = adapt args ( #b := False )
+  -- @
+  --
+  -- @
+  --   > myAdapt ( #i := 3, #f := 17.1 )
+  --   > ( #f = 17.1, #b = False, #i := 3 )
+  -- @
+  --
+  -- Here @ myAdapt @ re-arranges the arguments into the result,
+  -- passing in additional (default) values that are overriden
+  -- when they occur in the arguments.
+  --
+  -- Includes custom validation, e.g. to disallow duplicate arguments.
+  -- Use 'uncheckedAdapt' to disable this validation
+  -- (you might get strange errors!).
+  adapt
+    :: args -- ^ Provided arguments
+    -> opt  -- ^ Default values of optional arguments
+    -> all  -- ^ Combination of provided arguments and non-overridden defaults
+
+instance ( UncheckedAdapt args opt all, CheckAdapt args opt all )
+      => Adapt args opt all where
+  adapt = uncheckedAdapt
+
+class    UncheckedAdapt small big big => UncheckedInject small big where
+  -- | Inject a smaller type into a larger one, without extra type-level validation.
+  --
+  -- Unchecked uses (e.g. presence of duplicate fields)
+  -- can throw abstruse compile-time error messages
+  -- or produce unexpected results at runtime.
+  --
+  -- Prefer using 'inject' whenever possible.
+  uncheckedInject :: small -> big -> big
+
+instance UncheckedAdapt small big big => UncheckedInject small big where
+  uncheckedInject = uncheckedAdapt
+
+class    ( UncheckedInject small big ) => Inject small big where
+  -- | Inject a smaller type into a larger one,
+  -- overriding the fields in the larger type with those from the smaller type.
+  --
+  -- @
+  --   myInject
+  --     :: ( "i" := Int, "f" := Float )
+  --     -> ( "f" := Float, "b" := Bool, "i" := Int )
+  --     -> ( "f" := Float, "b" := Bool, "i" := Int )
+  --   myInject = inject
+  -- @
+  --
+  -- Here @ myInject @ overrides the fields of the second argument
+  -- with those provided in the first argument.
+  --
+  -- @
+  --   > myInject ( #i := 3, #f := 17.1 ) ( #f := 9.0, #b := False, #i := 22 )
+  --   > ( #f := 17.1, #b := False, #i := 3 )
+  -- @
+  --
+  -- Includes custom validation, e.g. to disallow duplicate arguments.
+  -- Use 'uncheckedInject' to disable this validation
+  -- (you might get strange errors!).
+  inject :: small -> big -> big
+
+instance ( UncheckedInject small big, CheckInject small big )
+      => Inject small big where
+  inject = uncheckedInject
+
+class    UncheckedAdapt big big small => UncheckedProject big small where
+  -- | Project a smaller type out from a larger one, without extra type-level validation.
+  --
+  -- Unchecked uses (e.g. presence of duplicate fields)
+  -- can throw abstruse compile-time error messages
+  -- or produce unexpected results at runtime.
+  --
+  -- Prefer using 'project' whenever possible.
+  uncheckedProject :: big -> small
+
+instance UncheckedAdapt big big small => UncheckedProject big small where
+  uncheckedProject big = uncheckedAdapt big big
+
+class    ( UncheckedProject big small ) => Project big small where
+  -- | Project a smaller type out from a larger one, discarding the rest.
+  --
+  -- @
+  --   myProject :: ( "f" := Float, "b" := Bool, "i" := Int ) -> ( "i" := Int, "f" := Float )
+  --   myProject = project
+  -- @
+  --
+  -- Here @ myProject @ projects out a sub-component of the whole type,
+  -- in this case discarding the boolean while re-arranging the other fields.
+  --
+  -- @
+  --   > myProject ( #f := 17.1, #b := False, #i := 3 )
+  --   > ( #i := 3, #f := 17.1 )
+  -- @
+  --
+  -- Includes custom validation, e.g. to disallow duplicate arguments.
+  -- Use 'uncheckedProject' to disable this validation
+  -- (you might get strange errors!).
+  project :: big -> small
+
+instance ( UncheckedProject big small, CheckProject big small )
+      => Project big small where
+  project = uncheckedProject
+ src/Data/Generic/Labels.hs-boot view
@@ -0,0 +1,25 @@+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Data.Generic.Labels where
+
+--------------------------------------------------------------------------------
+
+class UncheckedAdapt args opt all where
+   uncheckedAdapt :: args -> opt -> all
+class UncheckedAdapt small big big
+   => UncheckedInject  small big where
+   uncheckedInject :: small -> big -> big
+class UncheckedAdapt big big small
+  => UncheckedProject big small where
+   uncheckedProject :: big -> small
+
+class ( UncheckedAdapt args opt all )
+   => Adapt args opt all where
+   adapt :: args -> opt -> all
+class ( UncheckedInject small big )
+   => Inject small big where
+   inject :: small -> big -> big
+class ( UncheckedProject big small )
+   => Project big small where
+   project :: big -> small
+ src/Data/Generic/Labels/Internal.hs view
@@ -0,0 +1,144 @@+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+{-|
+Module: Data.Generic.Labels.Internal
+
+Internal module containing the generics machinery to provide the instances
+exported by this library, using 'Data.Generics.Product.Internal.GLens.GLens'.
+
+__Warnings__:
+
+  * contains an incoherent instance for 'GAdapt' which is used to
+    prioritise built-in record field names over explicitly labelled types;
+  * contains an orphan overlapping instance for @generic-lens@'s 'Data.Generics.Product.Internal.GLens.GLens'
+    typeclass, which is used to additionally unwrap through labelled types.
+
+-}
+
+module Data.Generic.Labels.Internal
+  ( GAdapt(..) )
+  where
+
+-- base
+import Data.Kind
+  ( Constraint, Type )
+import GHC.Generics
+import GHC.TypeLits
+  ( Symbol )
+
+-- generic-lens-core
+import Data.Generics.Product.Internal.GLens
+  ( Eval, GLens(..), GLens', TyFun )
+import Data.Generics.Internal.Profunctor.Lens
+  ( view )
+import Data.Generics.Internal.Profunctor.Iso 
+  ( Iso, iso, kIso )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..), Label(..) )
+import Data.Generic.Labels.Internal.Errors
+  ( AdaptLabelMessage )
+
+--------------------------------------------------------------------------------
+-- Generics machinery for 'Adapt'.
+
+-- | Generic version of 'Data.Generic.Labels.Adapt'.
+type GAdapt :: ( Type -> Type ) -> ( Type -> Type ) -> ( Type -> Type ) -> Constraint
+class GAdapt args opt all where
+  gAdapt :: args p -> opt p -> all p
+
+instance ( GAdapt args opt all1, GAdapt args opt all2 ) => GAdapt args opt ( all1 :*: all2 ) where
+  gAdapt args opt = gAdapt args opt :*: gAdapt args opt
+
+instance GAdapt args opt all => GAdapt args opt ( C1 c all ) where
+  gAdapt args opt = M1 $ gAdapt args opt
+
+instance GAdapt args opt all => GAdapt args opt ( D1 c all ) where
+  gAdapt args opt = M1 $ gAdapt args opt
+
+-- | This instance is INCOHERENT because we assume that no type variable (say @all0@)
+-- will later be instantiated to a labelled type @lbl := all@.
+--
+-- The end result is that, when we have both a built-in Haskell record field name
+-- as well as an explicit label, we prioritise the built-in record field name over the label.
+instance {-# INCOHERENT #-}
+         ( GLens' ( HasTotalLabelPSym lbl ) ( args :*: opts ) all )
+      => GAdapt args opts ( M1 m meta ( Rec0 ( lbl := all ) ) )
+      where
+  gAdapt args opt = M1 . K1 . ( Label @lbl := ) $ view ( glens @( HasTotalLabelPSym lbl ) ) ( args :*: opt )
+
+instance ( GLens' ( HasTotalLabelPSym lbl ) ( args :*: opts ) all )
+      => GAdapt args opts ( S1 ( MetaSel ( Just lbl ) p f b ) ( Rec0 all ) )
+      where
+  gAdapt args opt = M1 . K1 $ view ( glens @( HasTotalLabelPSym lbl ) ) ( args :*: opt )
+
+--------------------------------------------------------------------------------
+-- Generic lens machinery.
+
+type And :: Maybe a -> Maybe a -> Maybe a
+type family m1 `And` m2 where
+  Just a `And` Just a = Just a
+  _      `And` _      = Nothing
+
+type Or :: Maybe a -> Maybe a -> Maybe a
+type family m1 `Or` m2 where
+  Just a `Or` _ = Just a
+  _      `Or` b = b
+
+type HasTotalLabelP :: Symbol -> ( Type -> Type ) -> Maybe Type
+type family HasTotalLabelP lbl f where
+  HasTotalLabelP lbl ( S1 ( MetaSel ( Just lbl ) _ _ _ ) ( Rec0 ty ) ) = 
+    Just ty
+  HasTotalLabelP lbl ( S1 ( MetaSel ( Just lbl' ) _ _ _ ) _ ) = 
+    Nothing
+  HasTotalLabelP lbl ( S1 _ ( K1 _ ( lbl := ty ) ) ) =
+    Just ty
+  HasTotalLabelP lbl ( S1 _ ( K1 _ ( lbl' := _ ) ) ) =
+    Nothing
+  HasTotalLabelP lbl ( l :*: r ) =
+    HasTotalLabelP lbl l `Or` HasTotalLabelP lbl r
+  HasTotalLabelP lbl ( l :+: r ) =
+    HasTotalLabelP lbl l `And` HasTotalLabelP lbl r
+  HasTotalLabelP lbl ( S1 _ _ ) =
+    Nothing
+  HasTotalLabelP lbl ( C1 _ f ) =
+    HasTotalLabelP lbl f
+  HasTotalLabelP lbl ( D1 _ f ) =
+    HasTotalLabelP lbl f
+  HasTotalLabelP lbl ( K1 _ _ ) =
+    Nothing
+  HasTotalLabelP lbl U1 =
+    Nothing
+  HasTotalLabelP lbl V1 =
+    Nothing
+
+type HasTotalLabelPSym :: Symbol -> TyFun ( Type -> Type ) ( Maybe Type )
+data HasTotalLabelPSym lbl f mbTy
+type instance Eval ( HasTotalLabelPSym lbl ) f = HasTotalLabelP lbl f
+
+class LabelIso mbLbl1 mbLbl2 s t a b | mbLbl1 s -> a, mbLbl2 t -> b where
+  lblIso :: Iso s t a b
+instance
+  ( AdaptLabelMessage lbl ( Just a1 ) Nothing b1
+  , a1 ~ a, b1 ~ b
+  ) => LabelIso ( Just lbl ) ( Just lbl ) ( lbl := a1 ) ( lbl := b1 ) a b where
+  lblIso = iso ( \ ( _ := a ) -> a ) ( Label @lbl := )
+  {-# INLINE lblIso #-}
+instance LabelIso Nothing Nothing a b a b where
+  lblIso = id
+  {-# INLINE lblIso #-}
+
+type GetLabel :: Type -> Maybe Symbol
+type family GetLabel ty where
+ GetLabel ( lbl := _ ) = Just lbl
+ GetLabel _            = Nothing
+
+instance {-# OVERLAPPABLE #-} LabelIso ( GetLabel a' ) ( GetLabel b' ) a' b' a b
+      => GLens pred ( K1 r a' ) ( K1 r b' ) a b where
+  glens = kIso . lblIso @( GetLabel a' ) @( GetLabel b' )
+  {-# INLINE glens #-}
+ src/Data/Generic/Labels/Internal/Errors.hs view
@@ -0,0 +1,500 @@+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}
+
+{-|
+Module: Data.Generic.Labels.Internal.Errors
+
+Internal module providing custom type errors for invalid uses of
+'Data.Generic.Labels.Adapt', 'Data.Generic.Labels.inject', 'Data.Generic.Labels.project'.
+
+Consider for instance trying to project a source record onto a smaller target record,
+but the source record is missing one of the fields:
+
+@
+missingField :: ( "a" := Bool, "c" := Double ) -> ( "c" := Double, "b" := Int )
+missingField = project
+@
+
+Note that the source record is missing the @ "b" := Int @ field which is present in the target.
+
+This results in the following error message:
+
+@
+  * No instance for
+        Project
+          ("b" := Float, "a" := Bool, "c" := Double)
+          ("c" := Double, "b" := Int)
+    The type being projected down is missing the following fields:
+      - #b := Int
+@
+-}
+
+module Data.Generic.Labels.Internal.Errors
+  ( AdaptLabelMessage
+  , CheckAdapt, CheckInject, CheckProject
+  )
+  where
+
+-- base
+import Data.Kind
+  ( Constraint, Type )
+import GHC.Generics
+import GHC.TypeLits
+  ( Symbol
+  , TypeError, ErrorMessage(..)
+  )
+
+-- generic-lens-core
+import Data.Generics.Product.Internal.GLens
+  ( Eval, TyFun )
+
+-- generic-labels
+import Data.Label
+  ( (:=) )
+import Data.Type.Error
+  ( ErrorIfAmbiguous, MessageIfNonEmpty, ThrowMessagesWithHeader )
+import Data.Type.List
+  ( (:++:), Intersect, Remove )
+import Data.Type.Maybe
+  ( CatMaybes )
+import Data.Type.Multiplicity
+  ( Mult ( None, One, Many ) )
+import {-# SOURCE #-} Data.Generic.Labels
+  ( Adapt(..), Inject(..), Project(..)
+  , UncheckedAdapt(..), UncheckedInject(..), UncheckedProject(..)
+  )
+
+--------------------------------------------------------------------------------
+-- Helper type families for improved error messages.
+
+-- | Throw an error message when encountering two distinct types with the same label.
+type AdaptLabelMessage :: Symbol -> Maybe Type -> Maybe Type -> Type -> Constraint
+type family AdaptLabelMessage lbl mb_argTy mb_optTy allTy where
+  AdaptLabelMessage _   Nothing     Nothing     ty = ( () :: Constraint )
+  AdaptLabelMessage _   ( Just ty ) Nothing     ty = ( () :: Constraint )
+  AdaptLabelMessage _   Nothing     ( Just ty ) ty = ( () :: Constraint )
+  AdaptLabelMessage _   ( Just ty ) ( Just ty ) ty = ( () :: Constraint )
+  AdaptLabelMessage lbl ( Just a )  Nothing     b  =
+    TypeError
+      (    Text "Mismatched types at label #" :<>: Text lbl :<>: Text "."
+      :$$: Text "   Expected type: " :<>: ShowType b
+      :$$: Text "   Provided type: " :<>: ShowType a
+      )
+  AdaptLabelMessage lbl Nothing    ( Just o )   b =
+    TypeError
+      (    Text "Mismatched types at label #" :<>: Text lbl :<>: Text "."
+      :$$: Text "   Expected type: " :<>: ShowType b
+      :$$: Text "   Optional type: " :<>: ShowType o
+      )
+  AdaptLabelMessage lbl ( Just a ) ( Just o ) b  =
+    TypeError
+      (    Text "Mismatched types at label #" :<>: Text lbl :<>: Text "."
+      :$$: Text "   Expected type: " :<>: ShowType b
+      :$$: Text "   Provided type: " :<>: ShowType a
+      :$$: Text "   Optional type: " :<>: ShowType o
+      )
+
+-- | Throw an error message when an invalid use of 'Data.Generic.Labels.Adapt' is encountered:
+--   - a field of the destination is missing in the source,
+--   - a field that appears in both the source and destination appears more than once in either,
+--   - a 'Generic' instance is missing.
+type CheckAdapt :: Type -> Type -> Type -> Constraint
+type family CheckAdapt args opt all where
+  CheckAdapt a a a = ( () :: Constraint )
+  CheckAdapt a opt a = ( () :: Constraint )
+  CheckAdapt ( lbl := a ) ( lbl := o ) ( lbl := b ) =
+    ( AdaptLabelMessage lbl ( Just a ) ( Just o ) b, a ~ b, o ~ b )
+  CheckAdapt ( lbl := a ) opt ( lbl := b ) =
+    ( AdaptLabelMessage lbl ( Just a ) Nothing b, a ~ b )
+
+  CheckAdapt ( lbl1 := arg ) ( lbl2 := opt ) all =
+    ( ProperAdapt arg opt all
+        ( CollectLeaves ( S1 ( MetaSel ( Just lbl1 ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 arg ) ) )
+        ( CollectLeaves ( S1 ( MetaSel ( Just lbl2 ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 opt ) ) )
+        ( CollectLeaves ( Rep all ) )
+    , ErrorIfAmbiguous ( Rep all )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic all )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Adapt ( lbl1 := arg ) ( lbl2 := opt ) all )
+          )
+        )
+        ( () :: Constraint )
+    )
+
+  CheckAdapt ( lbl := arg ) opt all =
+    ( ProperAdapt arg opt all
+        ( CollectLeaves ( S1 ( MetaSel ( Just lbl ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 arg ) ) )
+        ( CollectLeaves ( Rep opt ) )
+        ( CollectLeaves ( Rep all ) )
+    , ErrorIfAmbiguous ( Rep opt )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic opt )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Adapt ( lbl := arg ) opt all )
+          )
+        )
+        ( () :: Constraint )
+    , ErrorIfAmbiguous ( Rep all )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic all )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Adapt ( lbl := arg ) opt all )
+          )
+        )
+        ( () :: Constraint )
+    )
+
+  CheckAdapt args ( lbl := opt ) all =
+    ( ProperAdapt args opt all
+        ( CollectLeaves ( Rep args ) )
+        ( CollectLeaves ( S1 ( MetaSel ( Just lbl ) NoSourceUnpackedness NoSourceStrictness DecidedLazy ) ( Rec0 opt ) ) )
+        ( CollectLeaves ( Rep all ) )
+    , ErrorIfAmbiguous ( Rep args )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic args )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Adapt args ( lbl := opt ) all )
+          )
+        )
+        ( () :: Constraint )
+    , ErrorIfAmbiguous ( Rep all )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic all )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Adapt args ( lbl := opt ) all )
+          )
+        )
+        ( () :: Constraint )
+    )
+
+  CheckAdapt args opt all =
+    ( ProperAdapt args opt all
+        ( CollectLeaves ( Rep args ) ) ( CollectLeaves ( Rep opt ) ) ( CollectLeaves ( Rep all ) )
+    , ErrorIfAmbiguous ( Rep args )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic args )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Adapt args opt all )
+          )
+        )
+        ( () :: Constraint )
+    , ErrorIfAmbiguous ( Rep opt )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic opt )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Adapt args opt all )
+          )
+        )
+        ( () :: Constraint )
+    , ErrorIfAmbiguous ( Rep all )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic all )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Adapt args opt all )
+          )
+        )
+        ( () :: Constraint )
+    )
+
+-- | Throw an error message when an invalid use of 'Data.Generic.Labels.inject' is encountered:
+--   - a field of the destination is missing in the source,
+--   - a field that appears in both the source and destination appears more than once in either,
+--   - a 'Generic' instance is missing.
+type CheckInject :: Type -> Type -> Constraint
+type family CheckInject small big where
+  CheckInject a a = ( () :: Constraint )
+  CheckInject small big =
+    ( ProperInjection small big ( CollectLeaves ( Rep small ) ) ( CollectLeaves ( Rep big ) )
+    , ErrorIfAmbiguous ( Rep small )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic small )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Inject small big )
+          )
+        )
+        ( () :: Constraint )
+    , ErrorIfAmbiguous ( Rep big )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic big )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Inject small big )
+          )
+        )
+        ( () :: Constraint )
+    )
+
+-- | Throw an error message when an invalid use of 'Data.Generic.Labels.project' is encountered:
+--   - a field of the destination is missing in the source,
+--   - a field that appears in both the source and destination appears more than once in either,
+--   - a 'Generic' instance is missing.
+type CheckProject :: Type -> Type -> Constraint
+type family CheckProject big small where
+  CheckProject a a = ( () :: Constraint )
+  CheckProject big small =
+    ( ProperProjection big small ( CollectLeaves ( Rep big ) ) ( CollectLeaves ( Rep small ) )
+    , ErrorIfAmbiguous ( Rep big )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic big )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Project big small )
+          )
+        )
+        ( () :: Constraint )
+    , ErrorIfAmbiguous ( Rep small )
+        ( TypeError
+          (    Text "No instance for " :<>: ShowType ( Generic small )
+          :$$: Text "arising from the constraint " :<>: ShowType ( Project big small )
+          )
+        )
+        ( () :: Constraint )
+    )
+
+--------------------------------------------------------------------------------
+-- Checking validity using type families.
+
+data Leaves =
+  Leaves
+    { labelledLeaves   :: [ ( Symbol, Type ) ]
+    , unlabelledLeaves :: [ Type ]
+    }
+
+type CollectLeaves :: ( Type -> Type ) -> Leaves
+type family CollectLeaves f where
+  CollectLeaves ( S1 ( MetaSel ( Just lbl ) _ _ _ ) ( Rec0 ty ) ) =
+    'Leaves '[ '( lbl, ty ) ] '[]
+  CollectLeaves ( M1 _ _ ( Rec0 ( lbl := ty ) ) ) =
+    'Leaves '[ '( lbl, ty ) ] '[]
+  CollectLeaves ( M1 _ _ ( Rec0 ty ) ) =
+    'Leaves '[] '[ ty ]
+  CollectLeaves ( M1 _ _ a ) =
+    CollectLeaves a
+  CollectLeaves ( l :*: r ) =
+    MergeLeaves ( CollectLeaves l ) ( CollectLeaves r )
+  CollectLeaves ( l :+: r ) =
+    IntersectLeaves ( CollectLeaves l ) ( CollectLeaves r )
+  CollectLeaves U1 =
+    'Leaves '[] '[]
+  CollectLeaves V1 =
+    'Leaves '[] '[]
+
+type ProperAdapt :: Type -> Type -> Type -> Leaves -> Leaves -> Leaves -> Constraint
+type family ProperAdapt args opts all argLeaves optLeaves allLeaves where
+  ProperAdapt args opts all ( 'Leaves ls_args us_args ) ( 'Leaves ls_opts us_opts ) ( 'Leaves ls_all us_all ) =
+    ThrowMessagesWithHeader
+      (    Text "No instance for "
+      :$$: Text "    " :<>: ShowType ( Adapt args opts all )
+      :$$: Text ""
+      )
+      ( CatMaybes
+         '[ MessageIfNonEmpty ShowTypeWithLabelSym us_args ( Text "Unexpected unlabelled arguments:" )
+          , MessageIfNonEmpty ShowTypeWithLabelSym us_opts ( Text "Unexpected unlabelled defaults:" )
+          , MessageIfNonEmpty ShowTypeWithLabelSym us_all  ( Text "Unexpected unlabelled types in destination:" )
+          ]
+      :++:
+        ValidAdaptMessages args opts all ( RelativePosition ls_opts ls_all ) ( RelativePosition ls_args ls_all )
+      )
+
+data InjectOrProject
+  = InjectCase
+  | ProjectCase
+
+type ProperInjection :: Type -> Type -> Leaves -> Leaves -> Constraint
+type family ProperInjection small big smallLeaves bigLeaves where
+  ProperInjection small big ( 'Leaves ls_small us_small ) ( 'Leaves ls_big us_big ) =
+    ThrowMessagesWithHeader
+      (    Text "No instance for "
+      :$$: Text "    " :<>: ShowType ( Inject small big )
+      :$$: Text ""
+      )
+      ( CatMaybes
+         '[ MessageIfNonEmpty ShowTypeWithLabelSym us_small ( Text "Unexpected unlabelled types in source:" )
+          , MessageIfNonEmpty ShowTypeWithLabelSym us_big   ( Text "Unexpected unlabelled types in destination:" )
+          ]
+      :++:
+        ValidRelativePositionMessages InjectCase ( RelativePosition ls_small ls_big )
+      )
+
+type ProperProjection :: Type -> Type -> Leaves -> Leaves -> Constraint
+type family ProperProjection big small bigLeaves smallLeaves where
+  ProperProjection big small ( 'Leaves ls_big us_big ) ( 'Leaves ls_small us_small ) =
+    ThrowMessagesWithHeader
+      (    Text "No instance for "
+      :$$: Text "    " :<>: ShowType ( Project big small )
+      :$$: Text ""
+      )
+      ( CatMaybes
+         '[ MessageIfNonEmpty ShowTypeWithLabelSym us_big   ( Text "Unexpected unlabelled types in source:" )
+          , MessageIfNonEmpty ShowTypeWithLabelSym us_small ( Text "Unexpected unlabelled types in destination:" )
+          ]
+      :++:
+        ValidRelativePositionMessages ProjectCase ( RelativePosition ls_small ls_big )
+      )
+
+type ValidAdaptMessages :: Type -> Type -> Type -> RelPos ty -> RelPos ty -> [ ErrorMessage ]
+type family ValidAdaptMessages args opts all opt_all_relPos args_all_relPos where
+  ValidAdaptMessages args opts all ( 'RelPos optsNotInAll optsInAllDups allNotInOpt ) ( 'RelPos argsNotInAll argsInAllDups allNotInArgs ) =
+    CatMaybes
+     '[ MessageIfNonEmpty ShowTypeWithLabelSym argsNotInAll 
+           ( Text "The following provided types do not appear in the destination:" )
+      , MessageIfNonEmpty ShowTypeWithLabelSym optsNotInAll 
+           ( Text "The following optional types do not appear in the destination:" )
+      , MessageIfNonEmpty ShowWhichTypeWithLabelSym optsInAllDups
+           ( Text "The following duplicate optional types cause a problem:" )
+      , MessageIfNonEmpty ShowWhichTypeWithLabelSym argsInAllDups
+           ( Text "The following duplicate provided types cause a problem:" )
+      , MessageIfNonEmpty ShowTypeWithLabelSym ( allNotInOpt `Intersect` allNotInArgs )
+           ( Text "The following types are non-optional but have not been provided:" )
+      ]
+
+type ValidRelativePositionMessages :: InjectOrProject -> RelPos ty -> [ ErrorMessage ]
+type family ValidRelativePositionMessages injProj relPos where
+  ValidRelativePositionMessages InjectCase ( 'RelPos smallNotInBig smallInBigDups _ ) =
+    CatMaybes
+     '[ MessageIfNonEmpty ShowWhichTypeWithLabelSym smallInBigDups
+          ( Text "The following duplicate types cause a problem:" )
+      , MessageIfNonEmpty ShowTypeWithLabelSym smallNotInBig
+          ( Text "The following types can't be injected, as they are missing from the target:" )
+      ]
+  ValidRelativePositionMessages ProjectCase ( 'RelPos smallNotInBig smallInBigDups _ ) =
+    CatMaybes
+     '[ MessageIfNonEmpty ShowWhichTypeWithLabelSym smallInBigDups
+          ( Text "The following duplicate types cause a problem:" )
+      , MessageIfNonEmpty ShowTypeWithLabelSym smallNotInBig
+          ( Text "The following types can't be projected out, as they are missing from the source:" )
+      ]
+
+--------------------------------------------------------------------------------
+-- Computing the relative positition of two sets.
+
+data Which
+  = InSmall
+  | InBig
+  | InBoth
+
+data RelPos k =
+  RelPos
+    { smallNotInBig  :: [ k ]
+    , smallInBigDups :: [ ( k, Which ) ]
+    , bigNotInSmall  :: [ k ]
+    }
+
+type RelativePosition :: [k] -> [k] -> RelPos k
+type family RelativePosition small big where
+  RelativePosition '[] bs = 'RelPos '[] '[] bs
+  RelativePosition ( a ': as ) bs =
+    RelativePositionWithRemoves a ( Remove a as ) ( Remove a bs )
+
+type RelativePositionWithRemoves :: k -> ( [k], Mult ) -> ( [k], Mult ) -> RelPos k
+type family RelativePositionWithRemoves a rem_a_as rem_a_bs where
+  RelativePositionWithRemoves a '( rem_a_as, mult_a_as ) '( rem_a_bs, mult_a_bs ) =
+    RelativePositionHelper a mult_a_as mult_a_bs ( RelativePosition rem_a_as rem_a_bs )
+
+type RelativePositionHelper :: k -> Mult -> Mult -> RelPos k -> RelPos k
+type family RelativePositionHelper a a_in_as a_in_bs rest where
+  RelativePositionHelper a _ None ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
+    'RelPos ( a ': smallNotInBig ) smallInBigDups bigNotInSmall
+  RelativePositionHelper a None One ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
+    'RelPos smallNotInBig smallInBigDups bigNotInSmall
+  RelativePositionHelper a _ One ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
+    'RelPos smallNotInBig ( '( a, InSmall ) ': smallInBigDups ) bigNotInSmall 
+  RelativePositionHelper a None Many ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall ) =
+    'RelPos smallNotInBig ( '( a, InBig ) ': smallInBigDups ) bigNotInSmall 
+  RelativePositionHelper a _ Many ( 'RelPos smallNotInBig smallInBigDups bigNotInSmall  ) =
+    'RelPos smallNotInBig ( '( a, InBoth ) ': smallInBigDups ) bigNotInSmall 
+
+--------------------------------------------------------------------------------
+-- Helpers for constructing error messages.
+
+type ShowTypeWithLabel :: ty -> ErrorMessage
+type family ShowTypeWithLabel ty where
+  ShowTypeWithLabel @( Symbol, Type ) '( lbl, ty ) = Text "#" :<>: Text lbl :<>: Text " := " :<>: ShowType ty 
+  ShowTypeWithLabel @k ty = ShowType ty
+
+type ShowTypeWithLabelSym :: TyFun ty ErrorMessage
+data ShowTypeWithLabelSym fun mess
+type instance Eval ShowTypeWithLabelSym ty = ShowTypeWithLabel ty
+
+type ShowWhichTypeWithLabel :: ( ty, Which ) -> ErrorMessage
+type family ShowWhichTypeWithLabel tyWhich where
+  ShowWhichTypeWithLabel '( ty, _ ) =  ShowTypeWithLabel ty
+  --ShowWhichTypeWithLabel '( ty, which ) = ShowWhich which :<>: Text " " :<>: ShowTypeWithLabel ty
+
+type ShowWhichTypeWithLabelSym :: TyFun ( ty, Which ) ErrorMessage
+data ShowWhichTypeWithLabelSym fun mess
+type instance Eval ShowWhichTypeWithLabelSym tyWhich = ShowWhichTypeWithLabel tyWhich
+
+type ShowWhich :: Which -> ErrorMessage
+type family ShowWhich which where
+  ShowWhich InSmall = Text "(general)"
+  ShowWhich InBig   = Text "(special)"
+  ShowWhich InBoth  = Text "         "
+
+type MergeLeaves :: Leaves -> Leaves ->Leaves
+type family MergeLeaves as bs where
+  MergeLeaves ( 'Leaves l1 u1 ) ( 'Leaves l2 u2 ) = 'Leaves ( l1 :++: l2 ) ( u1 :++: u2 )
+
+type IntersectLeaves :: Leaves -> Leaves ->Leaves
+type family IntersectLeaves as bs where
+  IntersectLeaves ( 'Leaves l1 u1 ) ( 'Leaves l2 u2 ) = 'Leaves ( l1 `Intersect` l2 ) ( u1 `Intersect` u2 )
+
+--------------------------------------------------------------------------------
+-- Dummy class instances to de-clutter type signatures
+-- by avoiding systematic expansion of class constraints.
+
+-- | Dummy type used in dummy instances.
+type Dummy :: Type
+data Dummy
+  deriving stock Generic
+
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedAdapt a a Dummy where
+  uncheckedAdapt = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedAdapt a Dummy Dummy where
+  uncheckedAdapt = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedAdapt a Dummy a where
+  uncheckedAdapt = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedAdapt Dummy a a where
+  uncheckedAdapt = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedAdapt Dummy Dummy a where
+  uncheckedAdapt = undefined
+
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedInject a Dummy where
+  uncheckedInject = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedInject Dummy a where
+  uncheckedInject = undefined
+
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedProject a Dummy where
+  uncheckedProject = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} UncheckedProject Dummy a where
+  uncheckedProject = undefined
+
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Adapt a a Dummy where
+  adapt = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Adapt a Dummy Dummy where
+  adapt = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Adapt a Dummy a where
+  adapt = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Adapt Dummy a a where
+  adapt = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Adapt Dummy Dummy a where
+  adapt = undefined
+
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Inject a Dummy where
+  inject = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Inject Dummy a where
+  inject = undefined
+
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Project a Dummy where
+  project = undefined
+-- | Dummy instance to improve error messages.
+instance {-# OVERLAPPING #-} Project Dummy a where
+  project = undefined
+ src/Data/Label.hs view
@@ -0,0 +1,86 @@+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ViewPatterns #-}
+
+{-|
+Module: Data.Label
+Description: Field label type, for use with @OverloadedLabels@.
+
+This module provides syntax for labelling values with symbolic field names.
+
+Given @ val :: a @, we can specify a label by using the syntax
+@ #field := val @, which has type @ "field" := a @.
+
+For instance, we can pass a record of three arguments with the syntax:
+
+@
+myRecord :: ( "field1" := Int, "field2" := Bool, "field3" := Float )
+myRecord = ( #field1 := 3, #field2 := True, #field3 := 7.7 )
+@
+
+This is a simple triple of labelled types, so the order matters.    
+
+However, this library provides functionality which will automatically
+handle re-ordering fields when needed, see "Data.Generic.Labels".
+-}
+
+module Data.Label
+  ( (:=)
+      ( .., (:=) )
+  , Label
+      ( Label )
+  ) where
+
+-- base
+import Data.Kind
+  ( Type )
+import GHC.Exts
+  ( proxy# )
+import GHC.OverloadedLabels
+  ( IsLabel
+    ( fromLabel )
+  )
+import GHC.TypeLits
+  ( Symbol, KnownSymbol, symbolVal' )
+
+--------------------------------------------------------------------------------
+-- Field labels.
+
+-- | 'Data.Proxy.Proxy'-like label type,
+-- used to pass the label name at the type-level.
+--
+-- With @OverloadedLabels@:
+--
+-- @ #foo :: Label "foo" @
+data Label ( lbl :: Symbol ) = Label
+type role Label nominal
+instance ( lbl' ~ lbl ) => IsLabel lbl ( Label lbl' ) where
+  fromLabel = Label
+instance KnownSymbol lbl => Show ( Label lbl ) where
+  show _ = "#" <> symbolVal' @lbl proxy#
+
+-- | A type with a 'Label'.
+--
+-- With @OverloadedLabels@:
+--
+-- @ ( #bar := Just 'c' ) :: ( "bar" := Maybe Char ) @
+newtype ( lbl :: Symbol ) := ( a :: Type ) = Labelled { unLabel :: a }
+
+instance ( KnownSymbol lbl, Show a ) => Show ( lbl := a ) where
+  showsPrec p ( Labelled a ) =
+    showParen ( p > 1 )
+      ( showString ( show ( Label @lbl ) <> " := " ) . showsPrec 2 a )
+
+infix 1 :=
+-- | Add a 'Label' to a type.
+--
+-- With @OverloadedLabels@:
+--
+-- @ ( #bar := Just 'c' ) :: ( "bar" := Maybe Char ) @
+pattern (:=) :: Label lbl -> a -> lbl := a
+pattern lbl := a <- ( ( \ ( Labelled a ) -> LabelPair Label a ) -> LabelPair lbl a )
+  where
+    _ := a = Labelled a
+{-# COMPLETE (:=) #-}
+
+data LabelPair lbl a = LabelPair !( Label lbl ) !a
+ src/Data/Type/Error.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Type.Error
+  ( ErrorIfAmbiguous
+  , ListBulletsWith
+  , MessageIfNonEmpty
+  , ThrowMessagesWithHeader
+  , UnlinesMessages
+  )
+  where
+
+-- base
+import Data.Kind
+  ( Constraint )
+import GHC.TypeLits
+  ( TypeError, ErrorMessage(..) )
+
+-- generic-lens-core
+import Data.Generics.Product.Internal.GLens
+  ( Eval, TyFun )
+
+--------------------------------------------------------------------------------
+
+type ErrorIfAmbiguous :: k -> Constraint -> l -> l
+type family ErrorIfAmbiguous break err a where
+  ErrorIfAmbiguous Dummy _ _ = Dummy
+  ErrorIfAmbiguous _     _ a = a
+
+type Dummy :: k
+data family Dummy
+
+type MessageIfNonEmpty :: TyFun ty ErrorMessage -> [ ty ] -> ErrorMessage -> Maybe ErrorMessage
+type family MessageIfNonEmpty showTySym tys message where
+  MessageIfNonEmpty _         '[] _       = Nothing
+  MessageIfNonEmpty showTySym tys message = Just ( message :$$: ListBulletsWith showTySym tys )
+
+type ListBulletsWith :: TyFun ty ErrorMessage -> [ ty ] -> ErrorMessage
+type family ListBulletsWith showTySym tys where
+  ListBulletsWith _         '[]           = Text ""
+  ListBulletsWith showTySym ( ty ': tys ) = Text "  - " :<>: Eval showTySym ty
+                                       :$$: ListBulletsWith showTySym tys
+
+type ThrowMessagesWithHeader :: ErrorMessage -> [ ErrorMessage ] -> Constraint
+type family ThrowMessagesWithHeader header messages where
+  ThrowMessagesWithHeader _ '[] = ( () :: Constraint )
+  ThrowMessagesWithHeader header messages = TypeError ( header :$$: UnlinesMessages messages )
+
+type UnlinesMessages :: [ ErrorMessage ] -> ErrorMessage
+type family UnlinesMessages messages where
+  UnlinesMessages '[] = Text ""
+  UnlinesMessages ( m ': ms ) = m :$$: UnlinesMessages ms
+ src/Data/Type/List.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Type.List
+  ( (:++:), Elem, Intersect, Remove )
+  where
+
+-- generic-labels
+import Data.Type.Multiplicity
+  ( AddMult
+  , Mult
+    ( None, One )
+  )
+
+--------------------------------------------------------------------------------
+
+infixr 5 :++:
+type (:++:) :: [k] -> [k] -> [k]
+type family xs :++: ys where
+  '[]         :++: ys = ys
+  ( x ': xs ) :++: ys = x ': xs :++: ys
+
+type Elem :: k -> [k] -> Bool
+type family Elem x xs where
+  Elem _ '[]         = False
+  Elem x ( x ': _ )  = True
+  Elem x ( _ ': ys ) = Elem x ys
+
+type Remove :: k -> [k] -> ( [k], Mult )
+type family Remove x ys where
+  Remove _ '[] = '( '[], None )
+  Remove x ( x ': ys ) = RemoveHelper Nothing    ( Remove x ys )
+  Remove x ( y ': ys ) = RemoveHelper ( Just y ) ( Remove x ys )
+
+type RemoveHelper :: Maybe k -> ( [k], Mult ) -> ( [k], Mult )
+type family RemoveHelper new rest where
+  RemoveHelper Nothing    '( rest, m ) = '(      rest, m `AddMult` One )
+  RemoveHelper ( Just y ) '( rest, m ) = '( y ': rest, m )
+
+-- | Intersect two lists, removing duplicates.
+type Intersect :: [k] -> [k] -> [k]
+type family Intersect as bs where
+  Intersect '[] _ = '[]
+  Intersect _ '[] = '[]
+  Intersect ( a ': as ) bs = IntersectHelper a as ( Remove a bs )
+
+type IntersectHelper :: k -> [k] -> ( [k], Mult ) -> [k]
+type family IntersectHelper a as rem_a_bs where
+  IntersectHelper _ as '( bs, None ) =      Intersect as bs
+  IntersectHelper a as '( bs, _    ) = a ': Intersect as bs
+ src/Data/Type/Maybe.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module Data.Type.Maybe
+  ( CatMaybes )
+  where
+
+--------------------------------------------------------------------------------
+
+type CatMaybes :: [ Maybe a ] -> [ a ]
+type family CatMaybes mbs where
+  CatMaybes '[] = '[]
+  CatMaybes ( Nothing ': mbs ) = CatMaybes mbs
+  CatMaybes ( Just a ': mbs )  = a ': CatMaybes mbs
+ src/Data/Type/Multiplicity.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module Data.Type.Multiplicity
+  ( AddMult, Mult(..) )
+  where
+
+--------------------------------------------------------------------------------
+
+data Mult
+  = None
+  | One
+  | Many
+
+type AddMult :: Mult -> Mult -> Mult
+type family AddMult m1 m2 where
+  AddMult None m = m
+  AddMult m None = m
+  AddMult _ _    = Many
+ test/Inspection.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE TemplateHaskell #-}
+
+module Inspection
+  ( tests )
+  where
+
+-- cabal
+import qualified Distribution.TestSuite as Cabal
+
+-- inspection-testing
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels-test
+import qualified ShouldCompile.Adapt.RRR as Adapt.RRR
+import qualified ShouldCompile.Adapt.TTR as Adapt.TTR
+import qualified ShouldCompile.Adapt.TTT as Adapt.TTT
+import qualified ShouldCompile.Adapt.SingletonArg    as Adapt.SingletonArg
+import qualified ShouldCompile.Adapt.SingletonArgOpt as Adapt.SingletonArgOpt
+import qualified ShouldCompile.Adapt.SingletonOpt    as Adapt.SingletonOpt
+import qualified ShouldCompile.Inject.Basic as Inject.Basic
+import qualified ShouldCompile.Inject.PolymorphicR  as Inject.PolymorphicR 
+import qualified ShouldCompile.Project.Basic as Project.Basic
+import qualified ShouldCompile.Project.PolymorphicR as Project.PolymorphicR
+import qualified ShouldCompile.Project.PolymorphicT as Project.PolymorphicT
+
+--------------------------------------------------------------------------------
+-- Inspection tests.
+
+tests :: IO [ Cabal.Test ]
+tests = pure $ map mkCabalTest inspectionResults
+
+inspectionResults :: [ ( String, Inspection.Result ) ]
+inspectionResults =
+  [ ( "Adapt.RRR", Adapt.RRR.result )
+  , ( "Adapt.TTR", Adapt.TTR.result )
+  , ( "Adapt.TTT", Adapt.TTT.result )
+  , ( "Adapt.SingletonArg"   , Adapt.SingletonArg.result    )
+  , ( "Adapt.SingletonArgOpt", Adapt.SingletonArgOpt.result )
+  , ( "Adapt.SingletonOpt"   , Adapt.SingletonOpt.result    )
+  , ( "Inject.Basic", Inject.Basic.result )
+  , ( "Inject.PolymorphicR", Inject.PolymorphicR.result )
+  , ( "Project.Basic", Project.Basic.result )
+  , ( "Project.PolymorphicR", Project.PolymorphicR.result )
+  , ( "Project.PolymorphicT", Project.PolymorphicT.result )
+  ]
+
+--------------------------------------------------------------------------------
+-- Converting to 'Cabal' test types.
+
+mkCabalTest :: ( String, Inspection.Result ) -> Cabal.Test
+mkCabalTest ( testName, inspectionResult ) =
+  Cabal.Test $
+    Cabal.TestInstance
+      { Cabal.run  = pure . Cabal.Finished . cabalResult $ inspectionResult
+      , Cabal.name = testName
+      , Cabal.tags = []
+      , Cabal.options   = []
+      , Cabal.setOption = \ _ _ -> Left "Test does not have any options."
+      }
+
+cabalResult :: Inspection.Result -> Cabal.Result
+cabalResult ( Inspection.Failure err ) = Cabal.Error err
+cabalResult _                          = Cabal.Pass
+ test/ShouldCompile/Adapt/RRR.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Adapt.RRR where
+
+-- base
+import GHC.Generics
+  ( Generic )
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Generic.Labels
+  ( Adapt(..) )
+
+--------------------------------------------------------------------------------
+
+data IFC = IFC { int :: Int, float :: Float, char :: Char }
+  deriving stock Generic
+
+data CFBI = CFBI
+  { char  :: Char
+  , float :: Float
+  , bool  :: Bool
+  , int   :: Int
+  }
+  deriving stock Generic
+
+data BC = BC { bool :: Bool, char :: Char }
+  deriving stock Generic
+
+test, manual :: IFC -> CFBI
+
+test args = adapt args ( BC { bool = False, char = '?' } )
+
+manual ( IFC { int, float, char } ) = CFBI { char, float, int, bool = False }
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Adapt/SingletonArg.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Adapt.SingletonArg where
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels
+  ( Adapt(..) )
+
+--------------------------------------------------------------------------------
+
+test, manual :: ( "a" := Int, "b" := Bool, "c" := Char )
+
+test = adapt ( #a := 3 ) ( #b := True, #c := 'c' )
+
+manual = ( #a := 3, #b := True, #c := 'c' )
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Adapt/SingletonArgOpt.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Adapt.SingletonArgOpt where
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels
+  ( Adapt(..) )
+
+--------------------------------------------------------------------------------
+
+test, manual :: ( "a" := Int, "b" := Bool )
+
+test = adapt ( #a := 3 ) ( #b := True )
+
+manual = ( #a := 3, #b := True )
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Adapt/SingletonOpt.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Adapt.SingletonOpt where
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels
+  ( Adapt(..) )
+
+--------------------------------------------------------------------------------
+
+test, manual :: ( "a" := Int, "b" := Bool, "c" := Char )
+
+test = adapt ( #a := 3, #b := True ) ( #c := 'c' )
+
+manual = ( #a := 3, #b := True, #c := 'c' )
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Adapt/TTR.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Adapt.TTR where
+
+-- base
+import GHC.Generics
+  ( Generic )
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels
+  ( Adapt(..) )
+
+--------------------------------------------------------------------------------
+
+data FBI = FBI
+  { float :: Float
+  , bool  :: Bool
+  , int   :: Int
+  }
+  deriving stock Generic
+
+test, manual :: ( "int" := Int, "float" := Float ) -> FBI
+
+test args = adapt args ( #bool := False )
+
+manual ( _ := int, _ := float ) = FBI { float, bool = False, int }
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Adapt/TTT.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Adapt.TTT where
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels
+  ( Adapt(..) )
+
+--------------------------------------------------------------------------------
+
+test, manual :: ( "int" := Int, "float" := Float ) -> ( "float" := Float, "bool" := Bool, "int" := Int )
+
+test args = adapt args ( #bool := False )
+
+manual ( int, float ) = ( float, #bool := False, int )
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Inject/Basic.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Inject.Basic where
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels
+  ( Inject(..) )
+
+--------------------------------------------------------------------------------
+
+test, manual
+  :: ( "a" := Double, "b" := Float )
+  -> ( "b" := Float, "c" := Int, "a" := Double )
+  -> ( "b" := Float, "c" := Int, "a" := Double )
+
+test = inject
+
+manual ( double, float ) ( _, int, _ ) = ( float, int, double )
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Project/Basic.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Project.Basic where
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels
+  ( Project(..) )
+
+--------------------------------------------------------------------------------
+
+test, manual :: ( "b" := Float, "c" := Int, "a" := Double ) -> ( "a" := Double, "b" := Float )
+
+test = project
+
+manual ( float, _, double ) = ( double, float )
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Project/PolymorphicR.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Project.PolymorphicR where
+
+-- base
+import GHC.Generics
+  ( Generic )
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Generic.Labels
+  ( project )
+
+-------------------------------------------------------------------
+
+default ()
+
+data AB b = AB { a :: Float, b :: b } deriving stock Generic
+
+newtype B b = B { b :: b } deriving stock Generic
+
+test, manual :: Num b => B b
+test = project ( AB { a = 0.5, b = 7 } )
+
+manual = B { b = 7 }
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )
+ test/ShouldCompile/Project/PolymorphicT.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+{-# OPTIONS_GHC -O1 #-}
+
+module ShouldCompile.Project.PolymorphicT where
+
+-- inspection-testing
+import Test.Inspection
+  ( inspectTest, (===) )
+import qualified Test.Inspection as Inspection
+  ( Result(..) )
+
+-- generic-labels
+import Data.Label
+  ( (:=)(..) )
+import Data.Generic.Labels
+  ( Project(..) )
+
+--------------------------------------------------------------------------------
+
+default ()
+
+test, manual :: ( "b" := Int, "c" := Char, "a" := Float )
+
+test = project ( #c := 'c', #a := 17.7, #b := 9 )
+
+manual = ( #b := 9, #c := 'c', #a := 17.7 )
+
+result :: Inspection.Result
+result = $( inspectTest $ 'manual === 'test )