Repository: hylo-lang/hylo (swift)

Issue:
Checker doesn't recognize conformance of 'Int' to 'Equatable'
```
trait P: Regular {
  property n: Int { let }
}

// error: type 'Int' does not conform to trait 'Equatable'
conformance Int: P {
  property n: Int {
    let { yield self }
  }
}
```
However, conformance to `Copyable` is properly recognized.

Pull request:
This patch fixes #1055

Patch:
diff --git a/Sources/Core/AST/Decl/SynthesizedFunctionDecl.swift b/Sources/Core/AST/Decl/SynthesizedFunctionDecl.swift
index 6a5507df4..b15e6a930 100644
--- a/Sources/Core/AST/Decl/SynthesizedFunctionDecl.swift
+++ b/Sources/Core/AST/Decl/SynthesizedFunctionDecl.swift
@@ -63,7 +63,7 @@ public struct SynthesizedFunctionDecl: Hashable {
 extension SynthesizedFunctionDecl: CustomStringConvertible {
 
   public var description: String {
-    "(\(receiver)).\(kind)"
+    "\(scope).(\(receiver)).\(kind)"
   }
 
 }
diff --git a/Sources/Core/Program.swift b/Sources/Core/Program.swift
index 3cc42ccdc..384dbafd0 100644
--- a/Sources/Core/Program.swift
+++ b/Sources/Core/Program.swift
@@ -61,7 +61,9 @@ extension Program {
   }
 
   /// Returns `true` iff `l` is lexically enclosed in more scopes than `r`.
-  public func hasMoreAncestors(_ l: AnyDeclID, than r: AnyDeclID) -> Bool {
+  public func hasMoreAncestors<T: NodeIDProtocol, U: NodeIDProtocol>(
+    _ l: T, than r: U
+  ) -> Bool {
     guard let s = nodeToScope[l] else { return false }
     guard let t = nodeToScope[r] else { return true }
 
@@ -73,6 +75,35 @@ extension Program {
     return false
   }
 
+  /// Compares `lhs` and `rhs` in `scopeOfUse` and returns whether one lexically shadows the other.
+  ///
+  /// `lhs` is lexically deeper than `rhs` w.r.t. `scopeOfUse` if any of these statements hold:
+  /// - `lhs` is declared in the module containing `scopeOfUse` and `rhs` isn't.
+  /// - `lhs` and `rhs` are declared in module containing `scopeOfUse` and `lhs` has more ancestors
+  ///   than `rhs`.
+  public func compareLexicalDepth<T: NodeIDProtocol, U: NodeIDProtocol>(
+    _ lhs: T, _ rhs: U, in scopeOfUse: AnyScopeID
+  ) -> StrictPartialOrdering {
+    let m = module(containing: scopeOfUse)
+    if isContained(lhs, in: m) {
+      // If `lhs` is in the same module as `scopeOfUse` but `rhs` isn't, then `lhs` shadows `rhs`.
+      guard isContained(rhs, in: m) else { return .ascending }
+
+      // If `lhs` and `rhs` are in the same module as `scopeOfUse`, then `lhs` shadows `rhs` iff
+      // it has more ancestors than `rhs`.
+      if hasMoreAncestors(lhs, than: rhs) { return .ascending }
+      if hasMoreAncestors(rhs, than: lhs) { return .descending }
+      return nil
+    }
+
+    if isContained(rhs, in: m) {
+      // If `rhs` is in the same module as `scopeOfUse` but `lhs` isn't, then `rhs` shadows `lhs`.
+      return .descending
+    }
+
+    return nil
+  }
+
   /// Returns the scope of `d`'s body, if any.
   public func scopeContainingBody(of d: FunctionDecl.ID) -> AnyScopeID? {
     switch ast[d].body {
diff --git a/Sources/Driver/Driver.swift b/Sources/Driver/Driver.swift
index 84020754e..509f085e9 100644
--- a/Sources/Driver/Driver.swift
+++ b/Sources/Driver/Driver.swift
@@ -129,13 +129,11 @@ public struct Driver: ParsableCommand {
   public func run() throws {
     do {
       let (exitCode, diagnostics) = try execute()
-
       diagnostics.render(
         into: &standardError, style: ProcessInfo.ansiTerminalIsConnected ? .styled : .unstyled)
-
       Driver.exit(withError: exitCode)
     } catch let e {
-      print("Unexpected error\n\(e)")
+      print("Unexpected error\n")
       Driver.exit(withError: e)
     }
   }
diff --git a/Sources/Driver/Process+Extensions.swift b/Sources/Driver/Process+Extensions.swift
index 571b4a4a4..852de1daf 100644
--- a/Sources/Driver/Process+Extensions.swift
+++ b/Sources/Driver/Process+Extensions.swift
@@ -27,8 +27,12 @@ extension Process {
     /// The contents of the standard error stream.
     public let standardError: Lazy<String>
 
-    /// The command-line that triggered the process run.
-    public let commandLine: [String]
+    /// The name of the executable ran by the process.
+    public let executable: String
+
+    /// The arguments passed to executable ran by the process.
+    public let arguments: [String]
+
   }
 
   /// Runs `executable` with the given command line `arguments` and returns its exit status along
@@ -51,8 +55,10 @@ extension Process {
     if p.terminationStatus != 0 {
       throw NonzeroExit(
         terminationStatus: p.terminationStatus,
-        standardOutput: r.standardOutput, standardError: r.standardError,
-        commandLine: [executable.fileSystemPath] + arguments)
+        standardOutput: r.standardOutput,
+        standardError: r.standardError,
+        executable: executable.fileSystemPath,
+        arguments: arguments)
     }
 
     return r
@@ -63,13 +69,14 @@ extension Process {
 extension Process.NonzeroExit: CustomStringConvertible {
 
   public var description: String {
-    return """
-      NonzeroExit(
-        terminationStatus: \(terminationStatus),
-        standardOutput: \(String(reflecting: standardOutput[])),
-        standardError: \(String(reflecting: standardError[])),
-        commandLine: \(commandLine))
-      """
+    """
+    '\(executable)' failed with status \(terminationStatus)
+    arguments: \(list: arguments)
+    standard output:
+    \(standardOutput[])
+    standard error:
+    \(standardError[])
+    """
   }
 
 }
diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker.swift b/Sources/FrontEnd/TypeChecking/TypeChecker.swift
index 6705e97dd..aad9da84a 100644
--- a/Sources/FrontEnd/TypeChecking/TypeChecker.swift
+++ b/Sources/FrontEnd/TypeChecking/TypeChecker.swift
@@ -297,13 +297,10 @@ struct TypeChecker {
   private mutating func demandConformance(
     of model: AnyType, to trait: TraitType, exposedTo scopeOfUse: AnyScopeID
   ) -> Conformance? {
+    // As results already in cache may be shadowed by a conformance that hasn't been checked yet,
+    // we have to check all conformance sources in scope before we can be sure we'll grab the right
+    // one when we call `cachedConformance`.
     let m = canonical(model, in: scopeOfUse)
-    if let c = cachedConformance(of: m, to: trait, exposedTo: scopeOfUse) {
-      return c
-    }
-
-    // If the conformance isn't already in cache, check sources defining a conformance of `model`
-    // to `trait` in scope, thus filling the cache before we look again.
     let r = refinements(of: trait)
     let s = originsOfConformance(of: m, to: trait, exposedTo: scopeOfUse)
     for o in s {
@@ -317,6 +314,10 @@ struct TypeChecker {
   /// Returns the checked conformance of `model` to `trait` that is exposed to `scopeOfUse`, or
   /// `nil` if such a conformance doesn't exist or hasn't been checked yet.
   ///
+  /// The result is the innermost available conformance of `model` to `trait` in `scopeOfUse` iff
+  /// all possible sources have already been checked. Otherwise, the returned conformance may be
+  /// shadowed by one that hasn't been checked yet.
+  ///
   /// - Requires: `model` is canonical.
   func cachedConformance(
     of model: AnyType, to trait: TraitType, exposedTo scopeOfUse: AnyScopeID
@@ -338,6 +339,10 @@ struct TypeChecker {
   /// Returns the checked conformance of `model` to `trait` that is exposed to `scopeOfUse`, or
   /// `nil` if such a conformance doesn't exist or hasn't been checked yet.
   ///
+  /// The result is the innermost available conformance of `model` to `trait` in `scopeOfUse` iff
+  /// all possible sources have already been checked. Otherwise, the returned conformance may be
+  /// shadowed by one that hasn't been checked yet.
+  ///
   /// - Requires: `model` is canonical.
   private func cachedConformance(
     of model: BoundGenericType, to trait: TraitType, exposedTo scopeOfUse: AnyScopeID
@@ -367,10 +372,7 @@ struct TypeChecker {
         }
       }
       .minimalElements { (a, b) in
-        if a.scope == b.scope { return .equal }
-        if program.isContained(a.scope, in: b.scope) { return .ascending }
-        if program.isContained(b.scope, in: a.scope) { return .descending }
-        return nil
+        program.compareLexicalDepth(a.scope, b.scope, in: scopeOfUse)
       }
       .uniqueElement
   }
@@ -1244,9 +1246,15 @@ struct TypeChecker {
 
     // TODO: Use arguments to bound generic types as constraints
 
+    // There's nothing to do if the conformance introduced by `origin` has already been checked.
+    // Otherwise, if there's already another conformance exposed to `scopeOfDefinition` in cache,
+    // it can't be introduced the same scope.
     if let c = cachedConformance(of: model, to: trait, exposedTo: scopeOfDefinition) {
-      assert(c.origin == origin, "inconsistent conformance origin")
-      return
+      if c.origin == origin {
+        return
+      } else {
+        precondition(c.scope != scopeOfDefinition, "inconsistent conformance origin")
+      }
     }
 
     /// A map from requirement to its implementation.
@@ -5060,12 +5068,10 @@ struct TypeChecker {
 
   /// Compares `lhs` and `rhs` in `scopeOfUse` and returns whether one shadows the other.
   ///
-  /// `lhs` is deeper than `rhs` w.r.t. `scopeOfUse` if either of these statements hold:
-  /// - `lhs` and `rhs` are members of traits `t1` and `t2`, respectively, and `t1` refines `t2`
+  /// `lhs` is deeper than `rhs` w.r.t. `scopeOfUse` if any of these statements hold:
+  /// - `lhs` and `rhs` are members of traits `t1` and `t2`, respectively, and `t1` refines `t2`.
   /// - `lhs` isn't member of a trait and `rhs` is.
-  /// - `lhs` is declared in the module containing `scopeOfUse` and `rhs` isn't.
-  /// - `lhs` and `rhs` are declared in module containing `scopeOfUse` and `lhs` has more ancestors
-  ///   than `rhs`.
+  /// - `lhs` is lexically deeper than `rhs` (see `Program.compareLexicalDepth`).
   private mutating func compareDepth(
     _ lhs: AnyDeclID, _ rhs: AnyDeclID, in scopeOfUse: AnyScopeID
   ) -> StrictPartialOrdering {
@@ -5085,24 +5091,7 @@ struct TypeChecker {
       return .ascending
     }
 
-    let m = program.module(containing: scopeOfUse)
-    if program.isContained(lhs, in: m) {
-      // If `lhs` is in the same module as `scopeOfUse` but `rhs` isn't, then `lhs` shadows `rhs`.
-      guard program.isContained(rhs, in: m) else { return .ascending }
-
-      // If `lhs` and `rhs` are in the same module as `scopeOfUse`, then `lhs` shadows `rhs` iff
-      // it has more ancestors than `rhs`.
-      if program.hasMoreAncestors(lhs, than: rhs) { return .ascending }
-      if program.hasMoreAncestors(rhs, than: lhs) { return .descending }
-      return nil
-    }
-
-    if program.isContained(rhs, in: m) {
-      // If `rhs` is in the same module as `scopeOfUse` but `lhs` isn't, then `rhs` shadows `lhs`.
-      return .descending
-    }
-
-    return nil
+    return program.compareLexicalDepth(lhs, rhs, in: scopeOfUse)
   }
 
   /// Compares `lhs` and `rhs` in `scopeOfUse` and returns whether one is more specific than the
diff --git a/Sources/IR/Mangling/Mangler.swift b/Sources/IR/Mangling/Mangler.swift
index c0f2f9906..6c79522e2 100644
--- a/Sources/IR/Mangling/Mangler.swift
+++ b/Sources/IR/Mangling/Mangler.swift
@@ -106,10 +106,10 @@ struct Mangler {
     mangle(decl: v, to: &output)
   }
 
-  /// Writes the mangled qualification of `d` to `output`.
-  private mutating func writeQualification<T: DeclID>(of d: T, to output: inout Output) {
+  /// Writes the mangled qualification of `n` to `output`.
+  private mutating func writeQualification<T: NodeIDProtocol>(of n: T, to output: inout Output) {
     var qualification: [AnyScopeID] = []
-    for s in program.scopes(from: program[d].scope) {
+    for s in program.scopes(from: program[n].scope) {
       if writeLookup(.node(AnyNodeID(s)), to: &output) {
         break
       } else {
@@ -354,6 +354,10 @@ struct Mangler {
   ) {
     write(operator: .synthesizedFunctionDecl, to: &output)
     write(synthesizedKind: symbol.kind, to: &output)
+
+    if symbol.scope.kind != ModuleDecl.self {
+      writeQualification(of: symbol.scope, to: &output)
+    }
     write(scope: symbol.scope, to: &output)
     mangle(type: ^symbol.type, to: &output)
   }


Test patch:
diff --git a/Tests/HyloTests/TestCases/TypeChecking/ConformanceWithRefinement.hylo b/Tests/HyloTests/TestCases/TypeChecking/ConformanceWithRefinement.hylo
new file mode 100644
index 000000000..95d55e412
--- /dev/null
+++ b/Tests/HyloTests/TestCases/TypeChecking/ConformanceWithRefinement.hylo
@@ -0,0 +1,13 @@
+//- typeCheck expecting: success
+
+trait P: Regular {
+  property n: Int { let }
+}
+
+conformance Int: P {
+  public property n: Int {
+    let { yield self }
+  }
+}
+
+public let x = Int.zero().n