SubListProof & ElemProof can be marked injective

[Icelandjack]

Type families SubListProof and ElemProof can be made injective, does that help anywhere?

type family
  SubListProof = (res :: SubList (xs :: [a]) (ys :: [a])) | res -> xs a where
  SubListProof = SubNil
  SubListProof = Keep SubListProof
  SubListProof = Drop SubListProof

type family
  ElemProof = (res :: EffElem eff a xs) | res -> eff a xs where
  ElemProof = Here
  ElemProof = There ElemProof

[goldfirere]

Perhaps, but I'm not keen on maintaining this repo as a "living document" -- so I'm going to close. If this code has been broken out into another package of mine, perhaps report there. Sorry!

[Icelandjack]

No problem, I'm not trying to change the code but trying to understand these new programming patterns and how they interact

[Icelandjack]

Err it exists here so I'll just.. reopen the ticket or something? ticket #1