diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index ef3d107d990804de3ce656c77875793c2f48a6aa..f36ed5ae8f33d44f1a3ce8550bc097ddb33ffc2c 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -249,4 +249,5 @@ End sum.
 Notation "Σ[ ty1 ; .. ; tyn ]" :=
   (sum (cons ty1%T (..(cons tyn%T nil)..))) : lrust_type_scope.
 
+Hint Opaque sum : lrust_typing lrust_typing_merge.
 Hint Resolve sum_mono' sum_proper' : lrust_typing.