The function f does not type check in the following code, which uses singletons with Frames and Vinyl:
f :: forall rs1 rs2. SList rs1 -> Frame (Record rs1) -> Int
f (OnlyRecord s1 t1) df1 = broadcast (*) (rhead <$> df1)
pattern OnlyRecord :: Sing s -> Sing t -> SList '[s :-> t]
pattern OnlyRecord sym typsing = SCons (SRecArrow sym typsing) SNil
rhead :: Record ((s :-> t) ': sstt) -> t
rhead (x :& xs) = getCol $ getIdentity x
data instance Sing (a :: Type) where
SRecArrow :: Sing (s :: Symbol) -> Sing (t :: Type) -> Sing (s :-> t)
The error is Couldn't match type ‘rs1’ with ‘'[s2 :-> t1] in the call to rhead -- basically it seems as if the pattern match is not binding the structure of rs1 as I would expect. But if I inline the pattern, it type checks:
f' :: forall rs1 rs2. SList rs1 -> Frame (Record rs1) -> Int
f' (SCons (SRecArrow s1 t1) SNil) df1 = broadcast (*) (rhead <$> df1)
Given the pattern synonym is supposed to be, well, a synonym, shouldn't it work identically to the inline pattern?
The definition of the pattern synonym is correct; it is the type which is wrong. The correct type is
pattern OnlyRecord :: () => (rs ~ '[s :-> t]) => Sing s -> Sing t -> SList rs
pattern OnlyRecord ...
With your original pattern type signature (which is equivalent to () => () => Sing s -> Sing t -> SList '[s :-> t]), you are claiming that given an expression x :: SList '[s :-> t] you can match on this expression using your pattern synonym. However, in f, you don't have such an expression - you only have x :: SList rs1 for some rs1, which is strictly more general. With the correct signature, you can use the pattern synonym to match on such an expression, because the pattern synonym is declared to be applicable to any SList rs; and then the provided constraints (namely rs ~ '[s :-> t]) are available within the scope of the pattern match.
For additional details regarding pattern signatures, see the GHC user guide.