From 5d9f3f6fba324bc4e1908bda5b42803a124a042d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Nov 2019 18:36:42 -0800 Subject: [PATCH] chore: add ambiguity comment --- tests/elabissues/typeclass_nested_validate.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/elabissues/typeclass_nested_validate.lean b/tests/elabissues/typeclass_nested_validate.lean index ce8a073e88..d6539abda1 100644 --- a/tests/elabissues/typeclass_nested_validate.lean +++ b/tests/elabissues/typeclass_nested_validate.lean @@ -63,3 +63,7 @@ instance bad (K E : Type) [Field K] [VectorSpace K E] [CompleteSpace K] : Comple -- Warning: argument #3 is a class that occurs in downstream arguments and not the return type. -- You may want to replace [Field K] with {Field K} so typeclass resolution infers this instance after solving downstream instances. -/ + +/- +The syntax `[Field K]` is ambiguous. It can be interpreted also as {Field K : _}. Note that we use this version all the time (e.g., {α β}). +-/