ssr breaks type-annotated patters in binders

[llelf]

Description of the problem

Variant foo := Foo (a b : nat).

Module VANILLA.
     Definition F₁ '(Foo a b)       := a+b.
     Definition F₂ '(Foo a b : foo) := a+b.
End VANILLA.

From Coq Require Import ssreflect.

Module SSREFLECT.
     Definition F₁ '(Foo a b)       := a+b.
Fail Definition F₂ '(Foo a b : foo) := a+b.
(* invalid notation for pattern *)
End SSREFLECT.

Coq Version

8.9.1, 8.10.0, master

[gares]

Maybe @ggonthier has an idea of where it could come from. SSR extends the syntax for binders, but I don't know that code very well.

[ggonthier]

The conflict is not with the plugin code and the binder extension syntax. It's with the overloading of the cast t : T syntax in ssreflect.v. The latter is used to force the interpretation t in type_scope when T is Type or Prop. There's been some discussion around this #6078, #6133, including a PR to support this more generally #6134, but this wasn't merged in the end.
At any rate, the problem here is that the parsing rules for type-annotated patterns are too fragile and should either parse the pattern (at level 99) and cast explicitly, or else recognise a generic operator : as a cast.