Fix type mismatch diagnostic for types in a double negative position (#…

…1344)

* Don't swap expected/actual types while unifying

* Refactor type inference diagnostics

* Clean up diagnostic messages

* Ordering should be private

* Rename TypeMismatch record to TypeContext

* Update variable names

* Refactor Diagnostic.withParents

* Fix Diagnostic.withParents for InfiniteType

* Add doc comment to TypeContext

* Update error messages

* Add comments to Diagnsotic.withParents

* Re-add "type" to message

src/QsCompiler/DataStructures/Diagnostics.fs

@@ -465,23 +465,24 @@ type DiagnosticItem =
         with
         | _ -> str // let's fail silently for now
 
-    static member Message(code: ErrorCode, args: IEnumerable<string>) =
-        let unlines = String.concat Environment.NewLine
+    static member Message(code, args) =
+        let typeMismatch summary expected actual =
+            String.concat Environment.NewLine [ summary; "Expected: " + expected; "  Actual: " + actual ]
 
         let message =
             match code with
             | ErrorCode.TypeMismatch ->
-                unlines [ "The type {0} does not match the type {1}."
-                          "Expected type: {2}"
-                          "Actual type:   {3}" ]
+                match Seq.take 4 args |> Seq.toList with
+                | [ expected; expectedParent; actual; actualParent ] when
+                    expected = expectedParent && actual = actualParent
+                    ->
+                    // Use a simplified message if the parent and child types are the same.
+                    "Expected type {0}, but actual type was {2}."
+                | _ -> typeMismatch "Couldn't match type {2} with type {0}." "{1}" "{3}"
             | ErrorCode.TypeIntersectionMismatch ->
-                unlines [ "The type {1} does not {0} the type {2}."
-                          "Left-hand type:  {3}"
-                          "Right-hand type: {4}" ]
+                typeMismatch "The type {3} doesn't {0} type {2}." "{2} (or a related type)" "{4}"
             | ErrorCode.InfiniteType ->
-                unlines [ "The type {0} cannot be unified with {1} because it would create an infinite type."
-                          "Left-hand type:  {2}"
-                          "Right-hand type: {3}" ]
+                typeMismatch "Couldn't create the infinite type while matching {2} and {0}." "{1}" "{3}"
             | ErrorCode.MutableClosure ->
                 "A lambda expression cannot close over a mutable variable. "
                 + "Declare '{0}' as immutable or remove the reference to '{0}'."

src/QsCompiler/SyntaxProcessor/ExpressionVerification.fs

@@ -9,6 +9,7 @@ open Microsoft.Quantum.QsCompiler.Diagnostics
 open Microsoft.Quantum.QsCompiler.SyntaxExtensions
 open Microsoft.Quantum.QsCompiler.SyntaxGenerator
 open Microsoft.Quantum.QsCompiler.SyntaxProcessing.TypeInference
+open Microsoft.Quantum.QsCompiler.SyntaxProcessing.TypeInference.RelationOps
 open Microsoft.Quantum.QsCompiler.SyntaxProcessing.VerificationTools
 open Microsoft.Quantum.QsCompiler.SyntaxTokens
 open Microsoft.Quantum.QsCompiler.SyntaxTree
@@ -125,15 +126,15 @@ let private verifyUdtWith processUdt (resolvedType: ResolvedType) range =
 /// Verifies that <paramref name="lhs"/> and <paramref name="rhs"/> have type Bool.
 /// </summary>
 let private verifyAreBooleans (inference: InferenceContext) lhs rhs =
-    inference.Unify(ResolvedType.New Bool, lhs.ResolvedType)
-    @ inference.Unify(ResolvedType.New Bool, rhs.ResolvedType)
+    inference.Match(ResolvedType.New Bool .> lhs.ResolvedType)
+    @ inference.Match(ResolvedType.New Bool .> rhs.ResolvedType)
 
 /// <summary>
 /// Verifies that <paramref name="lhs"/> and <paramref name="rhs"/> have type Int.
 /// </summary>
 let private verifyAreIntegers (inference: InferenceContext) lhs rhs =
-    inference.Unify(ResolvedType.New Int, lhs.ResolvedType)
-    @ inference.Unify(ResolvedType.New Int, rhs.ResolvedType)
+    inference.Match(ResolvedType.New Int .> lhs.ResolvedType)
+    @ inference.Match(ResolvedType.New Int .> rhs.ResolvedType)
 
 /// <summary>
 /// Verifies that <paramref name="expr"/> has type Int or BigInt.
@@ -331,7 +332,7 @@ let private verifyIdentifier (inference: InferenceContext) (symbols: SymbolTrack
 /// IMPORTANT: ignores any external type parameter occuring in expectedType without raising an error!
 let internal verifyAssignment (inference: InferenceContext) expectedType mismatchErr rhs =
     [
-        if inference.Unify(expectedType, rhs.ResolvedType) |> List.isEmpty |> not then
+        if inference.Match(expectedType .> rhs.ResolvedType) |> List.isEmpty |> not then
             QsCompilerDiagnostic.Error
                 (mismatchErr, [ showType rhs.ResolvedType; showType expectedType ])
                 (rangeOrDefault rhs)
@@ -370,7 +371,7 @@ let rec internal verifyBinding (inference: InferenceContext) tryBuildDeclaration
             if List.isEmpty types then UnitType else ImmutableArray.CreateRange types |> TupleType
             |> ResolvedType.create (TypeRange.inferred symbol.Range)
 
-        let unifyDiagnostics = inference.Unify(tupleType, rhsType)
+        let unifyDiagnostics = inference.Match(tupleType .> rhsType)
 
         let verify symbol symbolType =
             verifyBinding inference tryBuildDeclaration (symbol, symbolType) warnOnDiscard
@@ -495,7 +496,7 @@ type QsExpression with
             let resolveSlicingRange start step end' =
                 let integerExpr ex =
                     let ex = resolve context ex
-                    inference.Unify(ResolvedType.New Int, ex.ResolvedType) |> List.iter diagnose
+                    inference.Match(ResolvedType.New Int .> ex.ResolvedType) |> List.iter diagnose
                     ex
 
                 let resolvedStep = step |> Option.map integerExpr
@@ -558,7 +559,7 @@ type QsExpression with
         /// and returns the corrsponding NewArray expression as typed expression
         let buildNewArray (bType, ex) =
             let ex = resolve context ex
-            inference.Unify(ResolvedType.New Int, ex.ResolvedType) |> List.iter diagnose
+            inference.Match(ResolvedType.New Int .> ex.ResolvedType) |> List.iter diagnose
 
             let resolvedBase = symbols.ResolveType diagnose bType
             let arrType = resolvedBase |> ArrayType |> ResolvedType.create (TypeRange.inferred this.Range)
@@ -579,7 +580,7 @@ type QsExpression with
             let value = resolve context value
             let arrayType = ArrayType value.ResolvedType |> ResolvedType.create (TypeRange.inferred this.Range)
             let size = resolve context size
-            inference.Unify(ResolvedType.New Int, size.ResolvedType) |> List.iter diagnose
+            inference.Match(ResolvedType.New Int .> size.ResolvedType) |> List.iter diagnose
 
             let quantumDependency =
                 value.InferredInformation.HasLocalQuantumDependency
@@ -686,7 +687,7 @@ type QsExpression with
         /// *under the assumption* that the range operator is left associative.
         let buildRange (lhs: QsExpression, rhs) =
             let rhs = resolve context rhs
-            inference.Unify(ResolvedType.New Int, rhs.ResolvedType) |> List.iter diagnose
+            inference.Match(ResolvedType.New Int .> rhs.ResolvedType) |> List.iter diagnose
 
             let lhs =
                 match lhs.Expression with
@@ -704,7 +705,7 @@ type QsExpression with
                 | _ ->
                     resolve context lhs
                     |> (fun resStart ->
-                        inference.Unify(ResolvedType.New Int, resStart.ResolvedType) |> List.iter diagnose
+                        inference.Match(ResolvedType.New Int .> resStart.ResolvedType) |> List.iter diagnose
                         resStart)
 
             let localQdependency =
@@ -763,7 +764,7 @@ type QsExpression with
 
             let resolvedType =
                 if inference.Resolve(lhs.ResolvedType).Resolution = BigInt then
-                    inference.Unify(ResolvedType.New Int, rhs.ResolvedType) |> List.iter diagnose
+                    inference.Match(ResolvedType.New Int .> rhs.ResolvedType) |> List.iter diagnose
                     lhs.ResolvedType
                 else
                     verifyArithmeticOp inference this.Range lhs rhs |> takeDiagnostics
@@ -794,7 +795,7 @@ type QsExpression with
             let lhs = resolve context lhs
             let rhs = resolve context rhs
             let resolvedType = verifyIsIntegral inference lhs |> takeDiagnostics
-            inference.Unify(ResolvedType.New Int, rhs.ResolvedType) |> List.iter diagnose
+            inference.Match(ResolvedType.New Int .> rhs.ResolvedType) |> List.iter diagnose
 
             let localQdependency =
                 lhs.InferredInformation.HasLocalQuantumDependency
@@ -825,7 +826,7 @@ type QsExpression with
             let cond = resolve context cond
             let ifTrue = resolve context ifTrue
             let ifFalse = resolve context ifFalse
-            inference.Unify(ResolvedType.New Bool, cond.ResolvedType) |> List.iter diagnose
+            inference.Match(ResolvedType.New Bool .> cond.ResolvedType) |> List.iter diagnose
             verifyConditionalExecution ifTrue |> List.iter diagnose
             verifyConditionalExecution ifFalse |> List.iter diagnose
 
@@ -871,7 +872,7 @@ type QsExpression with
                 inference.Constrain(callable.ResolvedType, Callable(argType, output)) |> List.iter diagnose
             else
                 let diagnostics =
-                    inference.Unify(QsTypeKind.Function(argType, output) |> ResolvedType.New, callable.ResolvedType)
+                    inference.Match(callable.ResolvedType <. ResolvedType.New(QsTypeKind.Function(argType, output)))
 
                 if inference.Resolve callable.ResolvedType |> isOperation then
                     QsCompilerDiagnostic.Error(ErrorCode.OperationCallOutsideOfOperation, []) this.RangeOrDefault
@@ -1039,6 +1040,6 @@ type QsExpression with
                 NOT
                 (fun ex' ->
                     Bool |> ResolvedType.create (TypeRange.inferred this.Range),
-                    inference.Unify(ResolvedType.New Bool, ex'.ResolvedType))
+                    inference.Match(ResolvedType.New Bool .> ex'.ResolvedType))
                 ex
         | Lambda lambda -> buildLambda lambda

src/QsCompiler/SyntaxProcessor/StatementVerification.fs

@@ -12,6 +12,7 @@ open Microsoft.Quantum.QsCompiler.Diagnostics
 open Microsoft.Quantum.QsCompiler.SyntaxExtensions
 open Microsoft.Quantum.QsCompiler.SyntaxProcessing
 open Microsoft.Quantum.QsCompiler.SyntaxProcessing.Expressions
+open Microsoft.Quantum.QsCompiler.SyntaxProcessing.TypeInference.RelationOps
 open Microsoft.Quantum.QsCompiler.SyntaxTokens
 open Microsoft.Quantum.QsCompiler.SyntaxTree
 open Microsoft.Quantum.QsCompiler.Transformations.QsCodeOutput
@@ -56,7 +57,7 @@ let private asStatement comments location vars kind =
 let NewExpressionStatement comments location context expr =
     let expr, diagnostics = resolveExpr context expr
 
-    if context.Inference.Unify(ResolvedType.New UnitType, expr.ResolvedType) |> List.isEmpty |> not then
+    if context.Inference.Match(ResolvedType.New UnitType .> expr.ResolvedType) |> List.isEmpty |> not then
         let type_ = context.Inference.Resolve expr.ResolvedType |> SyntaxTreeToQsharp.Default.ToCode
         let range = QsNullable.defaultValue Range.Zero expr.Range
         QsCompilerDiagnostic.Error(ErrorCode.ValueImplicitlyIgnored, [ type_ ]) range |> diagnostics.Add
@@ -69,7 +70,7 @@ let NewExpressionStatement comments location context expr =
 /// Returns the built statement as well as an array of diagnostics generated during resolution and verification.
 let NewFailStatement comments location context expr =
     let expr, diagnostics = resolveExpr context expr
-    context.Inference.Unify(ResolvedType.New String, expr.ResolvedType) |> diagnostics.AddRange
+    context.Inference.Match(ResolvedType.New String .> expr.ResolvedType) |> diagnostics.AddRange
     onAutoInvertCheckQuantumDependency context.Symbols expr |> diagnostics.AddRange
     QsFailStatement expr |> asStatement comments location LocalDeclarations.Empty, diagnostics.ToArray()
 
@@ -216,7 +217,7 @@ let NewForStatement comments (location: QsLocation) context (symbol, expr) =
 /// as well as a delegate that given a Q# scope returns the built while-statement with the given scope as the body.
 let NewWhileStatement comments (location: QsLocation) context condition =
     let condition, diagnostics = resolveExpr context condition
-    context.Inference.Unify(ResolvedType.New Bool, condition.ResolvedType) |> diagnostics.AddRange
+    context.Inference.Match(ResolvedType.New Bool .> condition.ResolvedType) |> diagnostics.AddRange
 
     let whileLoop body =
         QsWhileStatement.New(condition, body) |> QsWhileStatement
@@ -229,7 +230,7 @@ let NewWhileStatement comments (location: QsLocation) context condition =
 /// as well as a delegate that given a positioned block of Q# statements returns the corresponding conditional block.
 let NewConditionalBlock comments location context condition =
     let condition, diagnostics = resolveExpr context condition
-    context.Inference.Unify(ResolvedType.New Bool, condition.ResolvedType) |> diagnostics.AddRange
+    context.Inference.Match(ResolvedType.New Bool .> condition.ResolvedType) |> diagnostics.AddRange
     onAutoInvertCheckQuantumDependency context.Symbols condition |> diagnostics.AddRange
     BlockStatement(fun body -> condition, QsPositionedBlock.New comments (Value location) body), diagnostics.ToArray()
 
@@ -321,7 +322,7 @@ let private NewBindingScope kind comments (location: QsLocation) context (symbol
             SingleQubitAllocation |> ResolvedInitializer.create (TypeRange.inferred init.Range), Seq.empty
         | QubitRegisterAllocation size ->
             let size, diagnostics = resolveExpr context size
-            context.Inference.Unify(ResolvedType.New Int, size.ResolvedType) |> diagnostics.AddRange
+            context.Inference.Match(ResolvedType.New Int .> size.ResolvedType) |> diagnostics.AddRange
             onAutoInvertCheckQuantumDependency context.Symbols size |> diagnostics.AddRange
 
             QubitRegisterAllocation size |> ResolvedInitializer.create (TypeRange.inferred init.Range),

src/QsCompiler/SyntaxProcessor/SymbolTracker.fs

@@ -289,12 +289,10 @@ type SymbolTracker(globals: NamespaceManager, sourceFile, parent: QsQualifiedNam
                 |> SymbolResolution.GenerateDeprecationWarning(fullName, qsSym.RangeOrDefault)
                 |> Array.iter addDiagnostic
 
-            let argType, returnType =
-                decl.ArgumentType |> StripPositionInfo.Apply, decl.ReturnType |> StripPositionInfo.Apply
-
             let idType =
-                kind ((argType, returnType), decl.Information)
+                kind ((decl.ArgumentType, decl.ReturnType), decl.Information)
                 |> ResolvedType.create (TypeRange.inferred qsSym.Range)
+                |> ResolvedType.withAllRanges (TypeRange.inferred qsSym.Range)
 
             LocalVariableDeclaration.New false (defaultLoc, GlobalCallable fullName, idType, false), decl.TypeParameters