More general dynamic types

[AshleyYakeley]

Should be able to support existing DynamicType as well as exceptions (#299)

[AshleyYakeley]

type storable Dynamic; # contains DynamicType

dynamictype T = !"someanchor" of
    # constructors
end;

dynamictype storable T = !"someanchor" of
    # constructors with anchors
end;

[AshleyYakeley]

Existential witness approach:

type Witness {-p,+q};

point.Witness @A <anchor>: Witness A;  # requires anchor uniqueness check

new.Witness @A: Action (Witness A);

datatype Subtype -a +b of
    Mk of
        subtype a <: b;
    end;
end;

testSubtype: Witness -a -> Witness +b -> Maybe (Subtype a b);

datatype Dynamic of
    Mk of
        type A;
        tw: Witness {-A,+A};
        val: A;
    end;
end;

• point.Witness requires anchor uniqueness check (Check for duplicate anchors #7)

[AshleyYakeley]

Existing DynamicType can be replaced by predicate types (#71).

General dynamic types probably can't be storable.

[AshleyYakeley]

Will do #303 instead.