Prohibit user-defined parametric sorts (#3878)

This PR adds a check to error on any non-`MInt` parametric sorts. 

We already assume `MInt` is the only parametric sort internally, so this
check just makes that explicit to the user:

https://github.com/runtimeverification/k/blob/0b4353c62f018a46736dc6b512414b77ab81523d/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java#L419

The check has to be done in `Module.checkSorts` so that we error early
enough, e.g., before computing the subsort `POSet`.

k-distribution/tests/regression-new/checks/checkParametricSort.k

@@ -0,0 +1,8 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module CHECKPARAMETRICSORT
+imports MINT
+imports INT
+
+syntax MInt{6}
+syntax {S} Foo{S}
+endmodule

k-distribution/tests/regression-new/checks/checkParametricSort.k.out

@@ -0,0 +1,5 @@
+[Error] Compiler: User-defined parametric sorts are currently unsupported: Foo{S}
+	Source(checkParametricSort.k)
+	Location(7,1,7,18)
+	7 |	syntax {S} Foo{S}
+	  .	^~~~~~~~~~~~~~~~~

kore/src/main/scala/org/kframework/definition/outer.scala

@@ -427,9 +427,21 @@ case class Module(
           set.head
       }
 
-  // check that non-terminals have a defined sort
+  private def throwIfUserParametricSort(sort: Sort, loc: HasLocation): Unit =
+    if (sort.head.params != 0 && sort.name != Sorts.MInt.name)
+      throw KEMException.compilerError(
+        "User-defined parametric sorts are currently " +
+          "unsupported: " + sort,
+        loc
+      )
+
+  // Check that user-defined sorts are non-parametric and that
+  // each non-terminal has a defined sort
   def checkSorts(): Unit = localSentences.foreach {
-    case p @ Production(_, params, _, items, _) =>
+    case s @ SyntaxSort(_, sort, _)     => throwIfUserParametricSort(sort, s)
+    case s @ SortSynonym(newSort, _, _) => throwIfUserParametricSort(newSort, s)
+    case p @ Production(_, params, sort, items, _) =>
+      throwIfUserParametricSort(sort, p)
       val res = items.collect {
         case nt: NonTerminal
             if !p.isSortVariable(nt.sort) && !definedSorts.contains(nt.sort.head) && !sortSynonymMap