mirror of
https://github.com/carbon-language/carbon-lang.git
synced 2026-10-05 16:11:06 +01:00
Richard Smith
374bf9f853
Per recent discussion, in `... where .A = B`, require that `B` is implicitly convertible to the type of `A` immediately, rather than treating that as part of the criteria that a type must satisfy to satisfy the resulting constraint. Extend the implementation of implicit conversion so that conversion of a type to a constraint checks that the type satisfies the constraint. As part of implementing this, stop duplicating rewrite constraints as equality constraints. Instead, when checking that a constraint is satisfied, check both its equality constraints and its rewrite constraints. This fixes an infinite recursion that would otherwise be caused by this change, and is also a necessary prerequisite for applying rewrite constraints to equality constraints, where we would otherwise collapse the implied equality constraints to a tautological `V == V` constraint. In passing, make ErrorBuilder support building the error message more incrementally and use that to improve diagnostics for mismatched values with equality constraints.
39 lines
1.1 KiB
Plaintext
39 lines
1.1 KiB
Plaintext
// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
|
|
// Exceptions. See /LICENSE for license information.
|
|
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
|
//
|
|
// AUTOUPDATE
|
|
// RUN: %{not} %{explorer-run}
|
|
// RUN: %{not} %{explorer-run-trace}
|
|
|
|
package ExplorerTest api;
|
|
|
|
interface Iface {
|
|
let T:! Type;
|
|
}
|
|
|
|
fn F[T:! Iface where .T == i32](x: T) {}
|
|
|
|
class Class {
|
|
impl as Iface where .T = i32 {}
|
|
}
|
|
|
|
// OK, constraint on `F` rewritten to `T:! Iface where U == i32`, which we can
|
|
// prove from the constraint on `U`.
|
|
fn G[U:! Type where .Self == i32, T:! Iface where .T = U](x: T, y: U) {
|
|
F(x);
|
|
}
|
|
|
|
// Not OK: would require looking through two levels of `==`.
|
|
fn H[V:! Type where .Self == i32, W:! Iface where .T == V](x: W, y: V) {
|
|
// CHECK:STDERR: COMPILATION ERROR: {{.*}}/explorer/testdata/assoc_const/fail_equal_indirectly.carbon:[[@LINE+1]]: constraint requires that (T).(Iface.T) (with value (W).(Iface.T)) == i32, which is not known to be true
|
|
F(x);
|
|
}
|
|
|
|
fn Main() -> i32 {
|
|
var x: Class = {};
|
|
G(x, 0);
|
|
H(x, 0);
|
|
return 0;
|
|
}
|