fix: replace dangerous instance by CoeTail

In order to guarantee termination of type class synthesis when resolving
coercions, a good rule of thumb is that the instances should not
introduce metavariables (during TC synthesis).  For common coercion type
classes this means:

 - `Coe T S`, `CoeTail T S`: the variables of `T` must be a subset of those of `S`
 - `CoeHead T S`: the variables of `S` must be a subset of those of `T`

If these rules are not followed, we can easily get nontermination.  In
this case: `CoeTC Foo Syntax` is reduced to `CoeTC Foo (TSyntax ?m_1)`
using the (dangerous) `Coe (TSyntax k) Syntax` instance, to which we can
then apply the otherwise fine `Coe (TSyntax [k]) (TSyntax (k'::ks))`
coercion infinitely often.

src/Init/Notation.lean

@@ -23,7 +23,7 @@ end Lean.Parser.Syntax
 
 namespace Lean
 
-instance : Coe (TSyntax ks) Syntax where
+instance : CoeHead (TSyntax ks) Syntax where
   coe stx := stx.raw
 
 instance : Coe SyntaxNodeKind SyntaxNodeKinds where