mlkit
mlkit copied to clipboard
Problematic unification of RT_BOT-typed region variables
In some cases, when garbage collection is enabled, region variables with type RT_BOT are forced into arrow effects, which serves to guarantee that no dangling pointers occur during evaluation. Here is a function for which this happens:
fun app (f: 'a -> int, x: 'a) : unit -> int =
fn () => f x
Unfortunately, sometimes different region variables of type RT_BOT are unified even when they are associated with different ML type variables. When this happens, instantiation can lead to region type clashes. See issue #97.
Here is a program that triggers the ICE:
local
datatype 'a option = NONE | SOME of 'a
datatype stream = Stream of unit -> (char * stream) option
infix @ ::
infix 3 <*> <* *>
infixr 4 <$> <$$> <$
fun nil @ xs = xs
| (x::xs) @ ys = x :: (xs @ ys)
datatype 'a parser = P of
{names: string list,
run: stream -> ('a * stream) option}
fun pure a =
P {names=[],
run=fn s => SOME (a, s)}
fun (P {names=names1, run=run1})
<*>
(P {names=names2, run=run2}) =
P {
names=names1 @ names2,
run=fn s =>
case run1 s of
SOME (f, s') =>
(case run2 s' of
SOME (b, s'') => SOME (f b, s'')
| NONE => NONE)
| NONE => NONE}
fun fst a _ = a
fun snd _ b = b
fun curry f a b = f (a, b)
fun f <$> p = (pure f) <*> p
fun f <$$> (p1, p2) = curry <$> (pure f) <*> p1 <*> p2
fun a <* b = fst <$> a <*> b
fun a *> b = snd <$> a <*> b
val next =
P {names=["char"],
run=fn s => NONE}
fun sat (P {names, run}, p) =
P {names=names,
run=fn s =>
case run s of
x as SOME (a, _) =>
if p a
then x
else NONE
| x => x}
fun nextSat p = sat (next, p)
fun many (P {names, run}) =
let fun f (s, k) =
case run s of
SOME (a, s') => f (s', a :: k)
| NONE => NONE
in P {names=names,
run=fn s => f (s, [])}
end
fun sepBy (t, sep) = (op ::) <$$> (t, many (sep *> t))
fun char c =
P {names=[],
run=fn s => NONE}
val space = nextSat (fn #" " => true | _ => false)
local
fun between (l, p: 'a parser, r): 'a parser =
many space *> char l *> p <* char r
in
fun paren p = between (#"(", p, #")")
fun cbrack p = between (#"{", p, #"}")
end
in
fun list (p: 'a parser): 'a list parser =
(fn x => x) <$> paren (sepBy (p, char #","))
datatype chunk =
Coalesce of string
| Simple of {mainFns: bool}
fun fromString s =
let val p = cbrack (pure (Simple {mainFns = true}))
in NONE
end
end