mlkit icon indicating copy to clipboard operation
mlkit copied to clipboard

Problematic unification of RT_BOT-typed region variables

Open melsman opened this issue 4 years ago • 1 comments

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.

melsman avatar Jan 18 '22 14:01 melsman

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

melsman avatar Jan 27 '22 13:01 melsman