More specific types for morphism product & sum combinators

[AshleyYakeley]

Currently we have:

!** :: (a ~> {-bp,+bq}) -> (a ~> {-cp,+cq}) -> a ~> {-(bp, cp),+(bq, cq)}
!++ :: ({-ap,+aq} ~> c) -> ({-bp,+bq} ~> c) -> {-(Either ap bp),+(Either aq bq)} ~> c

Would prefer:

!** :: ({-ap,+aq} ~> {-bp,+bq}) -> ({-ap,+aq} ~> {-cp,+cq}) -> {-ap,+aq} ~> {-(bp, cp),+(bq, cq)}
!++ :: ({-ap,+aq} ~> {-cp,+cq}) -> ({-bp,+bq} ~> {-cp,+cq}) -> {-(Either ap bp),+(Either aq bq)} ~> {-cp,+cq}

[AshleyYakeley]

Related to #26.

[AshleyYakeley]

Consider:

bodyweight :: Animal ~> Mass;
name :: Human ~> Text;
Human <= Animal;
myDog :: Animal;
myHuman :: Human;

then

bn :: {-Human,+Animal} ~> (Mass,Text)
bn = bodyweight !** name
bn !$% pureRef myHuman :: Ref (Mass,Text)
bn !$% pureRef myDog -- type error

[AshleyYakeley]

It's now

!** :: ({-ap,+Entity,+aq} ~> {-bp,+bq}) -> ({-ap,+Entity,+aq} ~> {-cp,+cq}) -> {-ap,+aq} ~> {-(bp, cp),+(bq, cq)}
!++ :: ({-ap,+aq} ~> c) -> ({-bp,+bq} ~> c) -> {-(Either ap bp),+(Either aq bq)} ~> c

[AshleyYakeley]

OK, now they're both correct:

!** :: ({-ap,+Entity,+aq} ~> {-bp,+bq}) -> ({-ap,+Entity,+aq} ~> {-cp,+cq}) -> {-ap,+aq} ~> {-(bp, cp),+(bq, cq)}
!++ :: ({-ap,+aq} ~> {-cp,+cq}) -> ({-bp,+bq} ~> {-cp,+cq}) -> {-(Either ap bp),+(Either aq bq)} ~> {-cp,+cq}