Make Shape an injective type family

[juliapath]

This allows the constraint solver to infer a ~ a' from Shape a ~ Shape a' make some type annotations redundant. The case, that one data type is the Shape of two different data types doesn't really seem useful, as one could just define two newtypes of that type, as we do with GShape. Ideally we would make this would be a data family which would allow a ~ a' and Shape ~ s to be inferred, from Shape a ~ s a, but sadly it is not possible to define default data families.

This is actually a breaking change, but I think it is not that likely it is actually going to break anything, as most people are probably just using GShape and even if they don't there is still a good chance, that their Shape instances are injective.

[juliapath]

The changes are already in the safe-entanglement branch