Skip to content

Commit

Permalink
Merge pull request #1567 from hylo-lang/conditional-synthetic-conform…
Browse files Browse the repository at this point in the history
…ance

Fix the checking of synthesizable conformances under a where clause
  • Loading branch information
kyouko-taiga authored Aug 23, 2024
2 parents e47c274 + fb2f60c commit d61d644
Show file tree
Hide file tree
Showing 4 changed files with 46 additions and 24 deletions.
53 changes: 29 additions & 24 deletions Sources/FrontEnd/TypeChecking/TypeChecker.swift
Original file line number Diff line number Diff line change
Expand Up @@ -421,49 +421,51 @@ struct TypeChecker {
}
}

/// Returns `true` if a conformance of `model` to `trait` is synthesizable in `scopeOfUse`.
/// Returns `true` if implementations of `trait`'s requirements can be synthesized for `model` in
/// `scopeOfImplementation`.
///
/// A conformance *M: T* is synthesizable iff *M* structurally conforms to *T*.
private mutating func canSynthesizeConformance(
_ model: AnyType, to trait: TraitType, in scopeOfUse: AnyScopeID
_ model: AnyType, to trait: TraitType, in scopeOfImplementation: AnyScopeID
) -> Bool {
switch model.base {
case let m as BoundGenericType:
return canSynthesizeConformance(m, to: trait, in: scopeOfUse)
return canSynthesizeConformance(m, to: trait, in: scopeOfImplementation)
case let m as ProductType:
return canSynthesizeConformance(m, to: trait, in: scopeOfUse)
return canSynthesizeConformance(m, to: trait, in: scopeOfImplementation)
default:
return structurallyConforms(model, to: trait, in: scopeOfUse)
return structurallyConforms(model, to: trait, in: scopeOfImplementation)
}
}

/// Returns `true` if `model` structurally conforms to `trait` in `scopeOfUse`.
/// Returns `true` if implementations of `trait`'s requirements can be synthesized for `model` in
/// `scopeOfImplementation`.
private mutating func canSynthesizeConformance(
_ model: BoundGenericType, to trait: TraitType, in scopeOfUse: AnyScopeID
_ model: BoundGenericType, to trait: TraitType, in scopeOfImplementation: AnyScopeID
) -> Bool {
let base = canonical(model.base, in: scopeOfUse)
let base = canonical(model.base, in: scopeOfImplementation)
let z = GenericArguments(model)

// If the base is a product type, we specialize each stored part individually to check whether
// the conformance holds for a specialized whole. Othwrwise, we specialize the base directly.
if let b = ProductType(base) {
let s = AnyScopeID(b.decl)
return program.storedParts(of: b.decl).allSatisfy { (p) in
let t = specialize(uncheckedType(of: p), for: z, in: s)
return conforms(t, to: trait, in: s)
let t = specialize(uncheckedType(of: p), for: z, in: scopeOfImplementation)
return conforms(t, to: trait, in: scopeOfImplementation)
}
} else {
let t = specialize(base, for: z, in: scopeOfUse)
return canSynthesizeConformance(t, to: trait, in: scopeOfUse)
let t = specialize(base, for: z, in: scopeOfImplementation)
return canSynthesizeConformance(t, to: trait, in: scopeOfImplementation)
}
}

/// Returns `true` if `model` structurally conforms to `trait` in `scopeOfUse`.
/// Returns `true` if implementations of `trait`'s requirements can be synthesized for `model` in
/// `scopeOfImplementation`.
private mutating func canSynthesizeConformance(
_ model: ProductType, to trait: TraitType, in scopeOfUse: AnyScopeID
_ model: ProductType, to trait: TraitType, in scopeOfImplementation: AnyScopeID
) -> Bool {
program.storedParts(of: model.decl).allSatisfy { (p) in
conforms(uncheckedType(of: p), to: trait, in: scopeOfUse)
conforms(uncheckedType(of: p), to: trait, in: scopeOfImplementation)
}
}

Expand Down Expand Up @@ -1644,16 +1646,19 @@ struct TypeChecker {
func syntheticImplementation(
of requirement: AnyDeclID, withAPI expectedAPI: API
) -> SynthesizedFunctionDecl? {
guard
let scopeOfImplementation = AnyScopeID(origin.source)!
if
let k = program.ast.synthesizedKind(of: requirement),
canSynthesizeConformance(model, to: trait, in: scopeOfDefinition)
else { return nil }

let t = ArrowType(expectedAPI.type)!
let h = Array(t.environment.skolems)
canSynthesizeConformance(model, to: trait, in: scopeOfImplementation)
{
let t = ArrowType(expectedAPI.type)!
let h = Array(t.environment.skolems)

// Note: compiler-known requirement is assumed to be well-typed.
return .init(k, typed: t, parameterizedBy: h, in: AnyScopeID(origin.source)!)
// Note: compiler-known requirement is assumed to be well-typed.
return .init(k, typed: t, parameterizedBy: h, in: scopeOfImplementation)
} else {
return nil
}
}

/// Returns a concrete implementation of `requirement` for `model` with given `expectedAPI`,
Expand Down
7 changes: 7 additions & 0 deletions StandardLibrary/Sources/Core/Optional.hylo
Original file line number Diff line number Diff line change
Expand Up @@ -19,3 +19,10 @@ public extension Optional {
}

}

// Note: We can't declare confitional conformance of `Optional` to "umbrella traits" yet without
// causing ambiguities. See #1566

public conformance Optional: Deinitializable where T: Deinitializable {}

public conformance Optional: Equatable where T: Equatable {}
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
//- typeCheck expecting: .success

type Box<T> {
public let contents: T
public memberwise init
}

conformance Box: Equatable where T: Equatable {}
2 changes: 2 additions & 0 deletions Tests/LibraryTests/TestCases/OptionalTests.hylo
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ public fun main() {
precondition(None<Int>() == None<Int>())

var x = 42 as Optional<Int>
precondition(x == x)

let y = if let i: Int = x { i.copy() } else { 0 }
precondition(y == 42)

Expand Down

0 comments on commit d61d644

Please sign in to comment.