Unification Bug in Typechecker

[noahyor]

I was making a program called 'trash.sw' in VSCode containing this:

def rep : int -> cmd a -> cmd a = \n. \c.
  if (n == 0) {} {c; rep (n-1) c}
end

def trash : int -> string -> cmd () = \n. \i.
  trash <- build {};
  rep n (give trash i);
  reprogram trash {selfdestruct};
end;

and swarm-lsp gave the error message "Can't unify s0 and ()"

[byorgey]

I think the problem is the type of rep. The type you have written claims that if you give it a command that returns a value of type a it will also yield a command that returns a value of type a, but it doesn't actually do that: when n reaches 0 it results in {} (which is shorthand for {noop}). noop does nothing and returns nothing and therefore has type cmd (), not cmd a. The most general type for rep would be rep : int -> cmd a -> cmd (). You could also figure this out by simply removing the type annotation from rep, i.e. writing def rep = \n. \c... etc. and seeing what type swarm thinks it has.

I don't think this is a bug, though the error message is definitely not very helpful. Related: #99 and #109.