diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index d3b4d503c7..952bec26d4 100644
--- a/src/Init/Notation.lean
+++ b/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