Open AshleyYakeley opened 1 year ago
Type escape issue:
let
datatype R of
MkR of
type T
v: T -> Action T
end;
end;
f = fn MkR => v;
r1: R
= MkR of
type T = Integer;
v = fn _ => return 0;
end;
r2: R
= MkR of
type T = Text;
v = fn t => writeLn stdout (t <> "!") >> return t
end;
in f r1 undefined >>= f r2
f
cannot be given a type. Solution: when matching a record pattern over an expression, examine the type of the expression to ensure it does not contain existential types defined in the record.
Idea: distinguish upper case and lower case:
type T
type T +a -b {-c,+d}
type t
(#312)*
onlyrf: t of type t; f: a -> (t *: Maybe a) end
Type of rf
is effectively forall t. (forall a. a -> (t *: Maybe a)) -> t
datatype R +t of Mk of type t; f: a -> (t *: Maybe a) end end
Extend record constructors (#150) to have existential types and subtype relations.
type T - +
type storable T + +
subtype P <: Q
Examples:
Note types can have any kind: