[move-prover] add a test case for warnings on uninstanted invariants

Closes: #9545

language/move-prover/tests/sources/functional/uninst_global_invariant.exp

@@ -0,0 +1,8 @@
+warning: Failed to instantiate all type parameters in this global invariant
+   ┌─ tests/sources/functional/uninst_global_invariant.move:11:9
+   │
+ 7 │         move_to(&account, S1 {});
+   │         ------- When instrumenting the global invariant here
+   ·
+11 │         invariant<T> exists<S1>(@0x42) ==> exists<S2<T>>(@0x42);
+   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

language/move-prover/tests/sources/functional/uninst_global_invariant.move

@@ -0,0 +1,17 @@
+module 0x42::Test {
+    struct S1 has key, store {}
+
+    struct S2<T: store> has key, store { t: T }
+
+    fun foo(account: signer) {
+        move_to(&account, S1 {});
+    }
+
+    spec module {
+        invariant<T> exists<S1>(@0x42) ==> exists<S2<T>>(@0x42);
+
+        // When applying invariant I to function foo, we cannot
+        // find a valid instantiation for the type parameter `T`.
+        // therefore, this global invariant cannot be checked.
+    }
+}