Function gets constrained by callers

[danabr]

Consider this example:

module list_tests

is_empty l =
  match l with
    [] -> true
  | _ :: _ -> false

a () = is_empty []

b () = is_empty [:ok]

c () = is_empty [1]

This fails unexpectedly with {error,{cannot_unify,list_tests,12,t_atom,t_int}}.

The fact that we applied an atom to is_empty, should not specialize the function to only act on atoms.

[j14159]

Interesting. Must be missing a deep type copy somewhere, thanks for finding this.

[j14159]

Per conversation on PR #30: tuples, pids, and receivers still need to be accounted for in mlfe_typer:copy_cell/2 so that their contained reference cells are deep-copied as well.

[j14159]

Started looking at this and found a new bug:

module poly_process

  behaviour start =
    receive with
        x -> behaviour x

a () = let p = spawn behaviour 1 in send 2 p

b () = let p = spawn behaviour 1.0 in send 2 p

While a/1 should be fine, b/1 should fail to type check since the received x differs from behaviour/1's type but it does not.

a and b as

a () = spawn behaviour 1
b () = spawn behaviour 1.0

type (respectively) to

{t_arrow,[t_unit],{t_pid,{unbound,t3,0}}}
{t_arrow,[t_unit],{t_pid,{unbound,t5,0}}}

But should type to

{t_arrow,[t_unit],{t_pid, t_int}}

and

{t_arrow,[t_unit],{t_pid, t_float}}

[j14159]

I was initially thinking this was failing due to a lack of evidence for the inferencer to make a decision as to the type of x but b/1 in the following also types when it shouldn't and the supplied function to behaviour/2 should be enough for the inferencer to type x:

module poly_process

behaviour state state_f =
  receive with
    x -> behaviour (state_f state x) state_f

a () =
  let f x y = x + y in
  spawn behaviour 1 f

b () =
  let f x y = x +. y in
  let p = spawn behaviour 1.0 f in
  send :a p\n",

[danabr]

Good find. This might explain why I failed to produce a failing test case for receives and spawns earlier.

[j14159]

Still investigating but my current hypothesis is that this might be a problem due to incomplete use of generalization. Some reference cells might contain the same name instead of linking to each other or using the same reference cell. Going to take some digging to check/confirm though.

[j14159]

Got it mostly narrowed down, just cleaning up some code and dialyzer errors on > 18.3 (building 19.1 as I type this up).

Basics of it was that copying a receiver wasn't ensuring that the receive type and the receiver's expression were guaranteed to use the same reference cells for the same type variables. This meant that unification during the typing of an application wouldn't affect the receive type and would thus lead to incorrect typing. I think my solution's a little rough around the edges and may yet have some holes but there's progress. Once records (row polymorphism) is working it's probably worth a full rewrite of the typer incorporating some cleanup as discussed elsewhere around using exceptions.