diff --git a/src/lib/effects.ml b/src/lib/effects.ml
index e61bff383..4485b26fc 100644
--- a/src/lib/effects.ml
+++ b/src/lib/effects.ml
@@ -218,7 +218,9 @@ let infer_def_direct_effects asserts_termination def =
               effects := EffectSet.add IncompleteMatch !effects
         | None -> Reporting.unreachable l __POS__ "Empty funcls in infer_def_direct_effects"
       end
-    | DEF_aux (DEF_mapdef _, _) -> effects := EffectSet.add IncompleteMatch !effects
+    | DEF_aux (DEF_mapdef _, def_annot) ->
+        if Option.is_some (get_def_attribute "incomplete" def_annot) then
+          effects := EffectSet.add IncompleteMatch !effects
     | DEF_aux (DEF_scattered _, _) -> effects := EffectSet.add Scattered !effects
     | _ -> ()
   end;
diff --git a/test/pattern_completeness/mapping_let.sail b/test/pattern_completeness/mapping_let.sail
new file mode 100644
index 000000000..680035862
--- /dev/null
+++ b/test/pattern_completeness/mapping_let.sail
@@ -0,0 +1,10 @@
+struct bool2 = {
+    field: bool,
+}
+
+mapping m : bool <-> bool2 = {
+   true <-> struct { field = true },
+   false <->  struct{ field = false },
+}
+
+let a = m(true)