SubListProof & ElemProof can be marked injective

[Icelandjack]

Moved from thesis

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]

These are interesting sorts of injectivity annotations, in that both are fully implied simply by the kind of the result. Note that the injective arguments are all mentioned in the kind of the result. Naturally, a type's identity implies its kind's identity. Does the injectivity annotation change inference? I would doubt it, but I can't say for sure.