Declare a constraint that holds for Vinyl records having a specific field

Question

I use vinyl to declare a number of different record types, some of which have a field called Content with a specific type LanguageContent. For the functions that depend on the field being present in the record, I want to have a type like:

getContent :: HasContent a => a -> LanguageContent
getContent a = a ^. rlens SContent . unAttr

(Function given for illustration only; there are many functions taking something that HasContent and doing different things with it.)

Now I just need to declare HasContent as a constraint. The closest I can get using Data.Vinyl.Notation is:

getContent :: (Content ∈ fs) => Rec Attr fs -> LanguageContent

A type family can be declared but the function does not typecheck:

type family HasContent c :: Constraint
type instance HasContent (Rec Attr rs) = Content ∈ rs

getContent :: HasContent a => a -> LanguageContent
getContent a = a ^. rlens SContent . unAttr

Could not deduce (a ~ Rec Attr rs0)
from the context (HasContent a)

I can make a constraint with two parameters which works but isn't ideal (rs is a parameter that I have to repeat everywhere):

type HasContent c rs = (c ~ Rec Attr rs, Content ∈ rs)

Without the extra parameter (see answer by @ChristianConkle), I just get:

type HasContent c = (c ~ Rec Attr rs, Content ∈ rs)

Not in scope: type variable ‘rs’

How do I declare a constraint which only holds for such Rec Attr fs that Content ∈ fs?

Answer 1

Edit: @Koterpillar's test file seems to demonstrate that this type synonym doesn't work the way I expected; it appears the constraint is not available inside the definition. It'd be worth investigation or a follow-up question to determine why. It had been my understanding that (C x => T x) -> Y was equivalent to C x => T x -> Y, but the fact that the example doesn't work seems to belie that. /Edit

I think you want to write this instead:

type RecWithContent rs = Content ∈ rs => Rec Attrs rs

getContent' :: RecWithContent rs -> LanguageContent

This is really just wrapping up the constraint in a type synonym. You need RankNTypes and probably a bunch of other extensions.

Your existing attempts to solve the problem and leave just a on the right hand side of the => boil down to this type synonym:

type HasContent c = (Content ∈ fs, c ~ Rec Attr fs)

In other words, you want HasContent to witness two separate things: that Content is in fs, and that the type parameter c is equal to Rec Attr fs.

I don't think you can do this in a way that's convenient for you. With the type synonym, the surface-level problem is that rs is not in scope on the right hand side. The deeper issue is that you're asking the compiler to make up fs; you want to write something like exists fs. (Content ∈ fs, c ~ Rec Attr fs), which is not expressible directly in current Haskell.

Your type family solution won't help, but for a different reason. In the definition of getContent, the compiler needs proof that a really is Rec Attr rs0 in order to use rlens (or probably unAttr), but it can't deduce that from the type family. (You know that there's only one type instance, but the compiler doesn't use that logic.)