Can we: replace Member p ps with a type-family?

[ShapeOfMatter]

No description provided.

[ShapeOfMatter]

Quoting @gshen42 from Zulip:

Let me be a bit more clear, there might be a way to do that , but I suspect it will be long-winded and painful. The short reason for this in Haskell is that the type-constraints system doesn't do backtracking. For example, let's say we want to prove Member l ls, it can be proved either directly by rules of Member or transitively through Subset and Member. Without backtracking, GHC will blindly pick one and if it fails then the whole resolution fails — it doesn't remember the other option and try that.

There're good reasons why GHC impose these restrictions: they want resolution to be coherent and decidable, and it's never ment to be a full-blown logic programming language.

One way around this is using a GHC plugin and write our own constraint solver. This is what I mean "long-winded and painful".