Check for type equivalence instead of equality

src/ast/transform/AstSemanticChecker.cpp

@@ -1440,10 +1440,16 @@ void TypeChecker::visitBinaryConstraint(const AstBinaryConstraint& constraint) {
     auto opRamTypes = getBinaryConstraintTypes(op);
     // Skip checks if either side is `Bottom` b/c it just adds noise.
     // The unable-to-deduce-type checker will point out the issue.
-    if (typeAnalysis.getTypes(left).empty() || typeAnalysis.getTypes(right).empty()) return;
+    auto leftTypes = typeAnalysis.getTypes(left);
+    auto rightTypes = typeAnalysis.getTypes(right);
+    if (leftTypes.isAll() || rightTypes.isAll() || (leftTypes.size() != 1) || (rightTypes.size() != 1))
+        return;
+
+    auto& leftType = *typeAnalysis.getTypes(left).begin();
+    auto& rightType = *typeAnalysis.getTypes(right).begin();
 
     // give them a slightly nicer error
-    if (isOrderedBinaryConstraintOp(op) && typeAnalysis.getTypes(left) != typeAnalysis.getTypes(right)) {
+    if (isOrderedBinaryConstraintOp(op) && !areEquivalentTypes(leftType, rightType)) {
         report.addError("Cannot compare different types", constraint.getSrcLoc());
     } else {
         auto checkTyAttr = [&](AstArgument const& side) {

tests/semantic.at

@@ -231,6 +231,7 @@ NEGATIVE_TEST([type_system14],[semantic])
 POSITIVE_TEST([type_system_records],[semantic])
 NEGATIVE_TEST([type_system_records2],[semantic])
 NEGATIVE_TEST([type_udef],[semantic])
+POSITIVE_TEST([types_components], [semantic])
 POSITIVE_TEST([underscore2],[semantic])
 POSITIVE_TEST([underscore3],[semantic])
 POSITIVE_TEST([underscore4],[semantic])

tests/semantic/type_system_records2/type_system_records2.err

@@ -1,39 +1,21 @@
 Error: Ambiguous record in file type_system_records2.dl at line 14
 A(1) :- [1,2] = [1].
 --------^------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 14
-A(1) :- [1,2] = [1].
---------^------------
 Error: Ambiguous record in file type_system_records2.dl at line 14
 A(1) :- [1,2] = [1].
 ----------------^----
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 14
-A(1) :- [1,2] = [1].
-----------------^----
 Error: Ambiguous record in file type_system_records2.dl at line 15
 A(2) :- [1,2] != [1].
 --------^-------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 15
-A(2) :- [1,2] != [1].
---------^-------------
 Error: Ambiguous record in file type_system_records2.dl at line 15
 A(2) :- [1,2] != [1].
 -----------------^----
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 15
-A(2) :- [1,2] != [1].
------------------^----
 Error: Ambiguous record in file type_system_records2.dl at line 16
 A(3) :- [1,2] = [1, 2, "3"].
 --------^--------------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 16
-A(3) :- [1,2] = [1, 2, "3"].
---------^--------------------
 Error: Ambiguous record in file type_system_records2.dl at line 16
 A(3) :- [1,2] = [1, 2, "3"].
 ----------------^------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 16
-A(3) :- [1,2] = [1, 2, "3"].
-----------------^------------
 Error: Unsigned constant (type mismatch) in file type_system_records2.dl at line 17
 A(4) :- [1u,2] != [2.0, 3].
 ---------^------------------
@@ -43,28 +25,16 @@ A(4) :- [1u,2] != [2.0, 3].
 Error: Ambiguous record in file type_system_records2.dl at line 18
 A(5) :- a = [1, 2], a = [b], b = [].
 ------------^------------------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 18
-A(5) :- a = [1, 2], a = [b], b = [].
-------------^------------------------
 Error: Ambiguous record in file type_system_records2.dl at line 18
 A(5) :- a = [1, 2], a = [b], b = [].
 ------------------------^------------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 18
-A(5) :- a = [1, 2], a = [b], b = [].
-------------------------^------------
 Error: Ambiguous record in file type_system_records2.dl at line 18
 A(5) :- a = [1, 2], a = [b], b = [].
 ---------------------------------^---
 Error: Ambiguous record in file type_system_records2.dl at line 19
 A(6) :- [1] != _.
 --------^---------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 19
-A(6) :- [1] != _.
---------^---------
-Error: Constraint requires an operand of type `number` or `unsigned` or `float` or `symbol` or a record in file type_system_records2.dl at line 19
-A(6) :- [1] != _.
----------------^--
 Error: Underscore in binary relation in file type_system_records2.dl at line 19
 A(6) :- [1] != _.
 ---------------^--
-23 errors generated, evaluation aborted
+13 errors generated, evaluation aborted

tests/semantic/types_components/types_components.dl

@@ -0,0 +1,39 @@
+// Souffle - A Datalog Compiler
+// Copyright (c) 2020, The Souffle Developers. All rights reserved
+// Licensed under the Universal Permissive License v 1.0 as shown at:
+// - https://opensource.org/licenses/UPL
+// - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+//
+// Types components
+// Check if types are deduced correctly, created for #1520
+//
+
+
+// aeflores' example
+.type BasicBlock <: symbol
+
+.comp Graph<N> {
+      .type TNode = N
+      .decl edge(a:TNode,b:TNode)
+}
+
+.init cfg = Graph<BasicBlock>
+
+.decl reach(a:BasicBlock, b:BasicBlock, c:BasicBlock)
+reach(origin, mid, end) :- reach(origin, z, end),
+                           cfg.edge(z, mid),
+                           mid != end.
+
+
+// azreika's example
+.type TypeOne = symbol
+.type TypeTwo = TypeOne
+
+.decl A(X:TypeOne)
+A("hello").
+
+.decl B(X:TypeTwo)
+B(X) :- A(Y), B(X), X != Y.
+
+.output B()

tests/semantic/types_components/types_components.err

@@ -0,0 +1,3 @@
+Warning: No rules/facts defined for relation cfg.edge in file types_components.dl at line 18
+      .decl edge(a:TNode,b:TNode)
+------------^---------------------