2

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?

RichardW
  • 899
  • 10
  • 15
  • The definition of the pattern synonym seems fine; it's type is wrong. The types of pattern synonyms are not really types at all (in particular, pattern synonym type annotations must specify which constraints are proved by matching on the pattern - your type definition says *no* constraints are proved, but the inlined pattern match is a GADT; by pattern matching on it you prove `rs1 ~ '[ x :-> xs ]` for some `x, xs`). A description of pattern synonym type annotations is given [here](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms). – user2407038 Nov 30 '17 at 02:14
  • Thank you; that link is very enlightening. I'm still having a hard time figuring out what proved constraint I need to add in this case, however. rs1 doesn't appear anywhere in the pattern declaration so adding `rs1 ~ '[ x :-> xs ]` doesn't constrain anything. – RichardW Nov 30 '17 at 02:54
  • I was referring to the `rs1` in the type of `f` - indeed, the appropriate change would add a new variable to the pattern signature. I believe something like `() => (rs ~ '[s :-> t]) => Sing s -> Sing t -> SList rs` should work (but I can't compile the example myself to make sure). – user2407038 Nov 30 '17 at 03:15
  • That did it! I'm still not really clear on why my original type signature doesn't imply the new constraint. Anyway, if you want to lift your comment into an answer, I will accept it. Thanks! – RichardW Nov 30 '17 at 03:59

1 Answers1

2

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.

user2407038
  • 14,400
  • 3
  • 29
  • 42
  • Isn't the `PatternSynonym` in the O.P. a red herring here? `f` doesn't use the arguments to `OnlyRecord` on its rhs. I'm guessing that's why it doesn't 'activate' the `data instance` for `SRecArrow`. You could just omit the first argument from `f` and put the `~` constraint on `f`'s type(?) – AntC Jun 14 '21 at 02:58
  • @AntC You are correct, `f` could be modified as you describe. However I made no attempt to discern the OPs intent, I assumed that the signature they wrote is precisely the one they want. With the current signature for `f`, it's a partial function, and I would expect that a complete program would have other patterns for `f` (e.g. `f _ _ = 0`). Regardless of the intent of `f`, it seemed to me that this question was about pattern synonyms in particular, and why inlining that pattern synonym gets it to work, so my answer focused on that aspect. – user2407038 Jun 14 '21 at 15:11