Typechecker incorrectly unifies distinct types through polymorphic type variables

[adabe588@…]

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;

[adabe588@…]

I worked on another bug report, which looks like it's the same issue:

encapsulated package Test

replaceable type X subtypeof Any;
replaceable type Y subtypeof Any;

partial function Get
  output Y current;
end Get;

partial function Func
  input X value;
end Func;

function test
algorithm
  call(const1, printFstInt);
end test;

function call
  input Get next;
  input Func func;
algorithm
  // func = printFstInt, next = const1
  func(next());
end call;

function printFstInt
  input Tuple<Integer,Integer> x;
algorithm
  // x = 1
  printInt(fst(x));
end printFstInt;

function const1
  output Integer i;
algorithm
  i := 1;
end const1;

protected function fst
  input Tuple<Integer, Integer> t;
  output Integer a;
algorithm
  a := match (t)
    local Integer b;
    case (b, _) then b;
  end match;
end fst;

function printInt
  input Integer x;
algorithm
  print(intString(x));
end printInt;

end Test;

[Martin Sjölund]

Moved to new milestone 1.9.4

[Martin Sjölund]

Milestone pushed to 1.9.5

[Martin Sjölund]

Milestone renamed

[Martin Sjölund]

Ticket retargeted after milestone closed

[Martin Sjölund]

Milestone moved to 1.12.0 due to 1.11.0 already being released.

[Francesco Casella]

The milestone of this ticket has been reassigned to "Future".

If you think the issue is still valid and relevant for you, please select milestone 1.13.0 for back-end, code generation and run-time issues, or 2.0.0 for front-end issues.

If you are aware that the problem is no longer present, please select the milestone corresponding to the version of OMC you used to check that, and set the status to "worksforme".

In both cases, a short informative comment would be welcome.