motivation: https://mail.haskell.org/pipermail/haskell-cafe/2021-February/133486.html

RBRDisjointUniverses.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UnicodeSyntax #-}
module Pipy where

import Data.Kind (Type)
import Data.Type.Equality (type (==))
import Data.Proxy
-- from "red-black-record"
import Data.RBR 
import GHC.TypeLits

-- | This is the typing judgement over all universes. It says that a given label
-- in a universe has a specific type of values it is bound to refer to.
type family Typing (universe :: sort) (label ∷ Symbol) ∷ Type
type instance Typing Cutie "catling" = Int
type instance Typing Cutie "whelp" = String

-- | This is a universe of labels.
data Cutie

-- A newtype parameterized by a universe and a symbol, 
-- where the type of the wrapped value is determined from those using the "Typing" type family. 
newtype Y (universe :: z) (s :: Symbol) = Y {unY :: Typing universe s}

-- A constrained version of 'insert' which inserts the key itself in the type-level map.
insertDisjoint :: forall k t universe. Insertable k k t 
               => Y universe k -> Record (Y universe) t -> Record (Y universe) (Insert k k t)
insertDisjoint = insert @k @k @t @(Y universe) 

-- The type Y is partially applied with the universe
disjointRec :: Record (Y Cutie) (FromList ['("catling","catling"), '("whelp", "whelp")])
disjointRec = 
      insertDisjoint @"catling" @_ @Cutie (Y 7)
    . insertDisjoint @"whelp" @_ @Cutie (Y "a string")
    $ unit

extracted :: Int
extracted = 
    let Y i = project @"catling" disjointRec
     in i

main :: IO ()
main = pure ()