Create way of mapping uninvertible positive type

[AshleyYakeley]

Let T be an uninvertible positive type (e.g. Maybe None). Given this:

data W of
    Mk of
        t: T;
    end;
end;
newT: Action T;

It ought to be possible to create newW: Action W, but it currently isn't.

• map (fn t => Mk.W) newT requires inversion of T.
• newT >>= fn t => pure Mk.W requires inversion of T.
• do t <- newT; pure Mk.W; end reduces to previous.

[AshleyYakeley]

Note that, given someT: T, it is possible to create someW: W: someW = let t = someT in Mk.W.

This is because let p = e in b does not simply reduce to (fn p => b) e.

[AshleyYakeley]

This might be a bad idea actually. Consider:

data AnyRef of
    Mk of
        ref: Ref {-a,+a};
    end;
end;

newRef: Action (Ref {-a,+a});

newAnyRef: Action AnyRef; # unsound

Note that, given some someRef: Ref {-a,+a} it is possible to create someAnyRef: AnyRef. This is not unsound.