Repository: hylo-lang/hylo (swift)

Issue:
Implement quantifier elimination for associated types
Attempting to instantiate the type of `foo` in `T.bar` will cause the compiler to crash in `TypeChecker.instantiate`:
```
trait T {
  type X: SemiRegular
  fun foo() -> X
  fun bar() {
    _ = foo()
  }
}
```
Commit: 289ed31a49747a3bfbec14547e0ace165d72e3e0

Pull request:
This PR fixes the way generic parameters are gathered for synthesized implementations of structural types involving associated types in trait extensions. 

These changes fix #1043 and #1280.

Patch:
diff --git a/Sources/Core/Types/AnyType.swift b/Sources/Core/Types/AnyType.swift
index 6402a8605..09862095d 100644
--- a/Sources/Core/Types/AnyType.swift
+++ b/Sources/Core/Types/AnyType.swift
@@ -187,6 +187,20 @@ public struct AnyType {
     (base is AssociatedTypeType) || (base is GenericTypeParameterType)
   }
 
+  /// Returns `true` iff `self` is bound to an existential quantifier.
+  public var isSkolem: Bool {
+    switch base {
+    case let u as AssociatedTypeType:
+      return u.domain.isSkolem
+    case is GenericTypeParameterType:
+      return true
+    case let u as ConformanceLensType:
+      return u.subject.isSkolem
+    default:
+      return false
+    }
+  }
+
   /// Indicates whether `self` has a record layout.
   public var hasRecordLayout: Bool {
     switch base {
diff --git a/Sources/Core/Types/AssociatedTypeType.swift b/Sources/Core/Types/AssociatedTypeType.swift
index 9e8463c9a..1bc9377fe 100644
--- a/Sources/Core/Types/AssociatedTypeType.swift
+++ b/Sources/Core/Types/AssociatedTypeType.swift
@@ -14,27 +14,44 @@ public struct AssociatedTypeType: TypeProtocol {
   /// The name of the associated type.
   public let name: Incidental<String>
 
+  /// A set of flags describing recursive properties.
+  public let flags: TypeFlags
+
   /// Creates an instance denoting the associated type declared by `decl` as a member of `domain`.
-  ///
-  /// - Requires: `domain` is an associated type, conformance lens, or generic type parameter.
   public init(_ decl: AssociatedTypeDecl.ID, domain: AnyType, ast: AST) {
-    switch domain.base {
-    case is AssociatedTypeType, is ConformanceLensType, is GenericTypeParameterType:
-      self.domain = domain
-    default:
-      preconditionFailure("invalid associated type domain")
+    self.init(decl: decl, domain: domain, name: ast[decl].baseName)
+  }
+
+  /// Creates an instance with the given properties.
+  init(decl: AssociatedTypeDecl.ID, domain: AnyType, name: String) {
+    var fs = domain.flags
+    if !domain.isSkolem && !(domain.base is TypeVariable) {
+      fs.remove(.isCanonical)
     }
 
     self.decl = decl
-    self.name = Incidental(ast[decl].baseName)
+    self.domain = domain
+    self.name = Incidental(name)
+    self.flags = fs
   }
 
-  public var flags: TypeFlags { .isCanonical }
+  public func transformParts<M>(
+    mutating m: inout M, _ transformer: (inout M, AnyType) -> TypeTransformAction
+  ) -> Self {
+    let d = domain.transform(mutating: &m, transformer)
+    return AssociatedTypeType(decl: decl, domain: d, name: name.value)
+  }
 
 }
 
 extension AssociatedTypeType: CustomStringConvertible {
 
-  public var description: String { "\(domain).\(name.value)" }
+  public var description: String {
+    if domain.base is ConformanceLensType {
+      return "(\(domain)).\(name.value)"
+    } else {
+      return "\(domain).\(name.value)"
+    }
+  }
 
 }
diff --git a/Sources/FrontEnd/TypeChecking/TypeChecker.swift b/Sources/FrontEnd/TypeChecking/TypeChecker.swift
index 796b2ea55..05d23de3a 100644
--- a/Sources/FrontEnd/TypeChecking/TypeChecker.swift
+++ b/Sources/FrontEnd/TypeChecking/TypeChecker.swift
@@ -4146,7 +4146,7 @@ struct TypeChecker {
     }
 
     // Skolems are valid associated type domains.
-    if program.isSkolem(domain) {
+    if domain.isSkolem {
       return ^MetatypeType(of: AssociatedTypeType(d, domain: domain, ast: program.ast))
     }
 
@@ -4600,7 +4600,8 @@ struct TypeChecker {
     func transform(
       mutating me: inout Self, _ t: AssociatedTypeType
     ) -> TypeTransformAction {
-      UNIMPLEMENTED("quantifier elimination for associated types (#1043)")
+      let d = t.domain.transform(mutating: &me, transform)
+      return .stepOver(^AssociatedTypeType(t.decl, domain: d, ast: me.program.ast))
     }
 
     func transform(
diff --git a/Sources/FrontEnd/TypedProgram.swift b/Sources/FrontEnd/TypedProgram.swift
index 6d80ed8f1..9422e22bb 100644
--- a/Sources/FrontEnd/TypedProgram.swift
+++ b/Sources/FrontEnd/TypedProgram.swift
@@ -195,18 +195,6 @@ public struct TypedProgram {
     }
   }
 
-  /// Returns `true` iff `t` is bound to an existential quantifier.
-  public func isSkolem(_ t: AnyType) -> Bool {
-    switch t.base {
-    case is AssociatedTypeType, is GenericTypeParameterType:
-      return true
-    case let u as ConformanceLensType:
-      return isSkolem(u.subject)
-    default:
-      return false
-    }
-  }
-
   /// Returns `true` iff deinitializing an instance of `t` in `scopeOfUse` is a no-op.
   ///
   /// A type is "trivially deinitializable" if deinitializing its instances doesn't have runtime
diff --git a/Sources/IR/Emitter.swift b/Sources/IR/Emitter.swift
index 16be8567b..108b2212e 100644
--- a/Sources/IR/Emitter.swift
+++ b/Sources/IR/Emitter.swift
@@ -2158,7 +2158,7 @@ struct Emitter {
     let functionToCall: Callee
 
     // Check if `d`'s implementation is synthetic.
-    if program.isRequirement(d) && !program.isSkolem(receiverType) {
+    if program.isRequirement(d) && !receiverType.isSkolem {
       let t = program.traitDeclaring(d)!
       let c = program.conformance(of: receiverType, to: t, exposedTo: scopeOfUse)!
       let irFunction = module.demandDeclaration(lowering: c.implementations[d]!)


Test patch:
diff --git a/Tests/EndToEndTests/TestCases/MonomorphizeSynthesizedImplementation.hylo b/Tests/EndToEndTests/TestCases/MonomorphizeSynthesizedImplementation.hylo
new file mode 100644
index 000000000..3c9920f1c
--- /dev/null
+++ b/Tests/EndToEndTests/TestCases/MonomorphizeSynthesizedImplementation.hylo
@@ -0,0 +1,20 @@
+//- compileAndRun expecting: success
+
+trait A {
+  type P: Regular
+}
+
+extension A {
+  public fun g(_ p: sink P) {
+    _ = (p.copy(), p.copy())
+  }
+}
+
+type X: A, Deinitializable {
+  public typealias P = Int
+  public memberwise init
+}
+
+public fun main() {
+  X().g(1)
+}