Skip to content

Commit

Permalink
Merge pull request #1264 from hylo-lang/synthethic-conformance-soundness
Browse files Browse the repository at this point in the history
Make sure synthesized conformances are sound
  • Loading branch information
kyouko-taiga authored Dec 29, 2023
2 parents 9bb120f + 70370a3 commit 7774d60
Show file tree
Hide file tree
Showing 8 changed files with 117 additions and 41 deletions.
43 changes: 12 additions & 31 deletions Sources/Core/AST/AST.swift
Original file line number Diff line number Diff line change
Expand Up @@ -241,41 +241,22 @@ public struct AST {
})
}

/// Returns the kind identifying synthesized declarations of `requirement`, which is defined by
/// `concept`, or `nil` if `requirement` is not synthesizable.
///
/// - Requires: `requirement` must be a requirement of `concept`.
public func synthesizedKind<T: DeclID>(
of requirement: T, definedBy concept: TraitType
) -> SynthesizedFunctionDecl.Kind? {
/// Returns the kind identifying synthesized declarations of `requirement`, or `nil` if
/// `requirement` is not synthesizable.
public func synthesizedKind<T: DeclID>(of requirement: T) -> SynthesizedFunctionDecl.Kind? {
// If the requirement is defined in `Deinitializable`, it must be the deinitialization method.
if concept == core.deinitializable.type {
assert(requirement.kind == FunctionDecl.self)
switch requirement.rawValue {
case core.deinitializable.deinitialize.rawValue:
return .deinitialize
}

// If the requirement is defined in `Movable`, it must be either the move-initialization or
// move-assignment method.
if concept == core.movable.type {
let d = MethodImpl.ID(requirement)!
switch self[d].introducer.value {
case .set:
return .moveInitialization
case .inout:
return .moveAssignment
default:
unreachable()
}
}

// If the requirement is defined in `Copyable`, it must be the copy method.
if concept == core.copyable.type {
assert(requirement.kind == FunctionDecl.self)
case core.movable.moveInitialize.rawValue:
return .moveInitialization
case core.movable.moveAssign.rawValue:
return .moveAssignment
case core.copyable.copy.rawValue:
return .copy
default:
return nil
}

// Requirement is not synthesizable.
return nil
}

/// Returns a table mapping each parameter of `d` to its default argument if `d` is a function,
Expand Down
11 changes: 11 additions & 0 deletions Sources/Core/Program.swift
Original file line number Diff line number Diff line change
Expand Up @@ -428,6 +428,17 @@ extension Program {
unreachable()
}

/// Returns the declarations of the stored part of `p`.
public func storedParts(of p: ProductTypeDecl.ID) -> [VarDecl.ID] {
var result: [VarDecl.ID] = []
for m in ast[p].members.filter(BindingDecl.self) {
for (_, n) in ast.names(in: ast[m].pattern) {
result.append(self[n].decl)
}
}
return result
}

/// Returns a textual description of `n` suitable for debugging.
public func debugDescription<T: NodeIDProtocol>(_ n: T) -> String {
switch n.kind {
Expand Down
89 changes: 84 additions & 5 deletions Sources/FrontEnd/TypeChecking/TypeChecker.swift
Original file line number Diff line number Diff line change
Expand Up @@ -356,6 +356,77 @@ struct TypeChecker {
return result
}

/// Returns `true` if `model` is declared conforming to `trait` or if its conformance can be
/// synthesized in `scopeOfUse`.
///
/// A conformance *M: T* is synthesizable iff *M* structurally conforms to *T*.
private mutating func conforms(
_ model: AnyType, to trait: TraitType, in scopeOfUse: AnyScopeID
) -> Bool {
conformedTraits(of: model, in: scopeOfUse).contains(trait)
|| structurallyConforms(model, to: trait, in: scopeOfUse)
}

/// Returns `true` if `model` structurally conforms to `trait` in `scopeOfUse`.
///
/// Given a trait describing basis operations (e.g., copy) of values, a structural conformance
/// *M: T* holds iff all the stored parts of *M* conform to *T*, structurally or otherwise. In
/// that case, the conformance can be synthesized because its implementation is obvious.
///
/// Note that this method is intended to test whether a conformance is synthesizable. It does not
/// look for explicit conformances of `model` to `trait`.
private mutating func structurallyConforms(
_ model: AnyType, to trait: TraitType, in scopeOfUse: AnyScopeID
) -> Bool {
switch model.base {
case let m as BoundGenericType:
return structurallyConforms(m, to: trait, in: scopeOfUse)
case let m as BufferType:
// FIXME: To remove once conditional conformance is implemented
return conforms(m.element, to: trait, in: scopeOfUse)
case let m as LambdaType:
return m.captures.allSatisfy({ conforms($0.type, to: trait, in: scopeOfUse) })
case is MetatypeType:
return true
case let m as ProductType:
return structurallyConforms(m, to: trait, in: scopeOfUse)
case let m as RemoteType:
return conforms(m.bareType, to: trait, in: scopeOfUse)
case let m as TupleType:
return m.elements.allSatisfy({ conforms($0.type, to: trait, in: scopeOfUse) })
case let m as TypeAliasType:
return structurallyConforms(m.aliasee.value, to: trait, in: scopeOfUse)
case let m as UnionType:
return m.elements.allSatisfy({ conforms($0, to: trait, in: scopeOfUse) })
default:
return false
}
}

/// Returns `true` if `model` structurally conforms to `trait` in `scopeOfUse`.
private mutating func structurallyConforms(
_ model: BoundGenericType, to trait: TraitType, in scopeOfUse: AnyScopeID
) -> Bool {
guard let base = ProductType(canonical(model.base, in: scopeOfUse)) else {
return false
}

let s = AnyScopeID(base.decl)
return program.storedParts(of: base.decl).allSatisfy { (p) in
let t = specialize(uncheckedType(of: p), for: model.arguments, in: s)
return conforms(t, to: trait, in: s)
}
}

/// Returns `true` if `model` structurally conforms to `trait` in `scopeOfUse`.
private mutating func structurallyConforms(
_ model: ProductType, to trait: TraitType, in scopeOfUse: AnyScopeID
) -> Bool {
program.storedParts(of: model.decl).allSatisfy { (p) in
conforms(uncheckedType(of: p), to: trait, in: scopeOfUse)
}
}

/// Returns the checked conformance of `model` to `trait` that is exposed to `scopeOfUse`, or
/// `nil` if such a conformance doesn't exist.
private mutating func demandConformance(
Expand Down Expand Up @@ -1435,12 +1506,19 @@ struct TypeChecker {
func resolveFunctionalImplementation(of requirement: AnyDeclID) {
let expectedAPI = canonicaAPI(of: requirement)

// Look for a user-defined implementation.
if let d = concreteImplementation(of: requirement, withAPI: expectedAPI) {
implementations[requirement] = .concrete(d)
} else if let d = syntheticImplementation(of: requirement, withAPI: expectedAPI) {
}

// Build a synthethic implementation if possible.
else if let d = syntheticImplementation(of: requirement, withAPI: expectedAPI) {
implementations[requirement] = .synthetic(d)
registerSynthesizedDecl(d, in: program.module(containing: program[origin.source].scope))
} else {
}

// No implementation matches the requirement.
else {
let t = expectedType(of: requirement)
let n = Diagnostic.note(
trait: trait, requires: requirement.kind,
Expand All @@ -1455,9 +1533,10 @@ struct TypeChecker {
func syntheticImplementation(
of requirement: AnyDeclID, withAPI expectedAPI: API
) -> SynthesizedFunctionDecl? {
guard let k = program.ast.synthesizedKind(of: requirement, definedBy: trait) else {
return nil
}
guard
let k = program.ast.synthesizedKind(of: requirement),
structurallyConforms(model, to: trait, in: scopeOfDefinition)
else { return nil }

// Note: compiler-known requirement is assumed to be well-typed.
return .init(k, typed: LambdaType(expectedAPI.type)!, in: AnyScopeID(origin.source)!)
Expand Down
2 changes: 1 addition & 1 deletion Sources/FrontEnd/TypedProgram.swift
Original file line number Diff line number Diff line change
Expand Up @@ -453,7 +453,7 @@ public struct TypedProgram {

var implementations = Conformance.ImplementationMap()
for requirement in ast.requirements(of: concept.decl) {
guard let k = ast.synthesizedKind(of: requirement, definedBy: concept) else { return nil }
guard let k = ast.synthesizedKind(of: requirement) else { return nil }

let a: GenericArguments = [ast[concept.decl].receiver: .type(model)]
let t = LambdaType(specialize(declType[requirement]!, for: a, in: scopeOfUse))!
Expand Down
2 changes: 0 additions & 2 deletions StandardLibrary/Sources/Core/Void.hylo
Original file line number Diff line number Diff line change
@@ -1,4 +1,2 @@
/// The type whose instance denote the absence of any specific value.
public typealias Void = {}

public conformance Void: Deinitializable {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
//- typeCheck expecting: failure

//! @+1 diagnostic type 'A<T>' does not conform to trait 'Deinitializable'
type A<T>: Deinitializable {
var x: T
public memberwise init
}
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ type A<X>: Movable, Deinitializable {
public memberwise init
}

type B<X>: Movable, Deinitializable {
type B<X: Deinitializable & Movable>: Movable, Deinitializable {
var foo: X
public memberwise init

Expand Down
2 changes: 1 addition & 1 deletion Tests/HyloTests/TestCases/TypeChecking/NestedGenerics.hylo
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
//- typeCheck expecting: success

type M<T> {
type M<T: Deinitializable> {
public var x: T
public memberwise init

Expand Down

0 comments on commit 7774d60

Please sign in to comment.