diff --git a/theories/typing/type.v b/theories/typing/type.v
index 61c8cf75822784ba847840cf5d3fcd6f67ce42e0..926b38e706529d7cd18c274213c4523cdf6dfbc3 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -50,9 +50,7 @@ Instance: Params (@ty_size) 2 := {}.
 Instance: Params (@ty_own) 2 := {}.
 Instance: Params (@ty_shr) 2 := {}.
 
-Arguments ty_size {_ _} _ / : simpl nomatch.
-Arguments ty_own {_ _} _ _ _ / : simpl nomatch.
-Arguments ty_shr {_ _} _ _ _ _ / : simpl nomatch.
+Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
 
 Class TyWf `{!typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.