Why does the type of inj require the IsSymbol constraint? It seems like sym would already be constrained to :: Symbol by the Cons constraint.
inj :: forall sym a r1 r2. Cons sym a r1 r2 => IsSymbol sym => SProxy sym -> a -> Variant r2
class Cons (label :: Symbol) (a :: Type) (tail :: # Type) (row :: # Type) | label a tail -> row, label row -> a tail
class IsSymbol (sym :: Symbol) where
IsSymbol provides reflectSymbol which lets you turn a compiletime string into a runtime string. Variant uses this to tag the constructor.
I think my source of confusion is that this type class uses a concrete type, rather than a type variable. It seems a bit odd to hardcode the type.
My original assumption is that type classes should use type variables, e.g.:
class Semigroup a where
append :: a -> a -> a
Could IsSymbol have been written with a type variable, like so:
class IsSymbol a where
reflectSymbol :: SProxy a -> String
Do all Symbols (and only Symbols) belong to IsSymbol? If so, why not let reflectSymbol be a standalone function instead of a type class instance?
Are you referring to Symbol in class IsSymbol (sym :: Symbol)? If so, sym is a type variable, and Symbol is the kind of that type variable. The only valid arguments to this type class are things that are of kind Symbol, which are type level strings.
This class is “magic” in that it is automatically solved by the compiler, so yes, all symbols effectively have an instance for IsSymbol by virtue of the compiler being able to generate the dictionary on the fly. A function doesn’t work because there is nothing for the compiler to solve. You would be unable to abstract over it like what inj is doing.
Thanks. This is an important point that I didn’t grasp initially.
In 0.14, you will be able to specify kinds like so, which might be more obvious:
class IsSymbol :: Symbol -> Constraint
class IsSymbol sym where
reflectSymbol :: SProxy sym -> String
@milesfrain I think that in theory you could have an implication between these constraints (Cons => IsSymbol) which you are asking for - a working approximation could be:
class (Cons l a t r, IsSymbol l) ⇐ Kons l a t r
x ∷ ∀ l a t r. Kons l a t r ⇒ SProxy l → a → Variant r
x = inj
Cons could imply IsSymbol… but they are in some sens “unrelated” because Cons doesn’t use reflectSymbol or share any “laws” with IsSymbol so it probably won’t happen 
Another part of the reason why Cons and IsSymbol are not related is to ensure that Cons has no data (it’s purely a type-level guarantee, with unsafe foreign code supporting function implementations), while IsSymbol has to include the data for reflectSymbol in its instance, as mentioned above. Of course they are most commonly used together.
p.s. Don’t forget instance kons :: (Cons l a t r, IsSymbol l) => Kons l a t r 
I’m now looking at insert and curious why Lacks is needed in addition to Cons.
insert :: forall r1 r2 l a. IsSymbol l => Lacks l r1 => Cons l a r1 r2 => SProxy l -> a -> Record r1 -> Record r2
Does Cons l a r1 r2 mean that r1 already “Lacks” l? Or does the Cons constraint alone allow for duplicate labels in r2 if r1 already contains label l?
Duplicate labels are always allowed in rows.