Desugar == to =!= if it is used at type Prop

[byorgey]

I think this should get us a lot of the benefits of =!= while allowing students to just use == and not worry about the difference.

[byorgey]

This is actually trickier than I thought. Even when we give an explicit Prop type annotation, the == operator still has type N * N -> Bool; it's only the overall expression that has type Prop:

Disco> :ann (3 == 4 : Prop)
(~==~ : ℕ × ℕ → Bool)((3 : ℕ, 4 : ℕ) : ℕ × ℕ) : Prop

This means e.g. we can't do something simple like just add a special case to compileBOp for == at type Prop, since the == operator actually doesn't have result type Prop.

Perhaps this would be possible if we pushed the Prop type down as far as possible, e.g. if we rewrite the type checker to always use the "propagate types inwards" trick (see swarm-game/swarm#99), though it seems like that could still be somewhat fragile.

[byorgey]

Alternatively, perhaps we can get this done simply by adding a bit more special cases to the desugarer. We already do have access to type information while desugaring. When desugaring an expression of type Prop we can propagate that information downward and desugar it specially. In other words, even when desugaring an expression of type Bool we can remember the fact that it is embedded within a larger expression of type Prop. It may be that we can also do something special for /\ and \/ in addition to ==.