id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
1814	Typechecker incorrectly unifies distinct types through polymorphic type variables	adabe588@…	somebody	"I finally managed to get this reproduction down to a manageable size. It can probably be minimized further but this should be good enough to see the issue. If it's unclear I can try to make it even smaller.

The issue is a unification that passes but should not, it ends up with me being able to pass a Tuple<Integer,Integer> as the argument to a function expecting Integer through the use of replaceable types. I had a similar issue earlier where I managed to construct a list where one of the elements was another list.

The issue stems from a bug in my code (using a tuple instead of an int) but it is hard to find and debug these bugs when the compiler accepts them.

Actual Output:
{{{
{true,true,true}
true
""""
intEqual
1, 2284673025
false
""""
}}}

Expected output:
{{{
{true,true,true}
false
""Some Type Error here""
}}}

test.mos:
{{{
setCommandLineOptions({""+d=rml,noevalfunc,failtrace"",""+g=MetaModelica"",""+showAnnotations""});

loadFile(""test.mo"");
getErrorString();

// First element
Test.test(1, 1);
getErrorString();
}}}

test.mo:
{{{
encapsulated package Collection

replaceable type State subtypeof Any;
replaceable type Element subtypeof Any;

partial function Next
  input State state;
  output Element current;
  output State nextState;
end Next;

partial function IsEmpty
  input State state;
  output Boolean empty;
end IsEmpty;

partial function Equality<A>
  input A x;
  input A y;
  output Boolean isEqual;
end Equality;

function eq<A>
  input Next next;
  input Equality equalityFunction;
  input A element;
  input State it;
  output Boolean res;
protected
  // Side note: Element is unified with A implicitly here, but if this line is changed to
  // A currentElement;
  // an error is thrown:
  // Type mismatch in pattern currentElement\n actual type:  polymorphic<A>\n expected type:\n polymorphic<Element>
  Element currentElement;
algorithm
  // call next, which will be Test.next in the test
  (currentElement, _) := next(it);
  res := equalityFunction(element, currentElement);
end eq;

end Collection;


package Test

protected import Collection.{eq};

function intEqual
  input Integer x;
  input Integer y;
  output Boolean equal;
algorithm
  // This line prints x correctly, but y is a tuple and its address (?) is printed.
  print(""intEqual\n"" +& intString(x) +& "", "" +& intString(y) +& ""\n"");
  equal := x == y;
end intEqual;

function next
  input Integer it;
  output Tuple<Integer,Integer> currentElement;
  output Integer nextIt;
algorithm
  // Incorrectly return a tuple even though intEqual(Int,Int) => Bool and not intEqual(Int,Tuple<Int,Int>) => Bool
  currentElement := (it, it);
  nextIt := it;
end next;

function test
  input Integer element;
  input Integer i;
  output Boolean res;
algorithm
  res := Collection.eq(next, intEqual, element, i);

  // fails properly
  // res := intEqual(element, (element,element));
end test;

end Test;

}}}"	defect	new	critical	Future	Frontend	trunk