Enforce rules on module parameters

Author: FlandiaYingman

hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala

@@ -613,8 +613,15 @@ extends Importer:
     case InfixApp(lhs: Ident, Keyword.`:`, rhs) =>
       Param(FldFlags.empty, fieldOrVarSym(ParamBind, lhs), S(term(rhs))) :: Nil
     case App(Ident(","), list) => params(list)._1
-    case TypeDef(Mod, inner, _, _) => param(inner)
-      .map(p => p.copy(flags = p.flags.copy(mod = true)))
+    case TypeDef(Mod, inner, N, N) =>
+      val ps = param(inner).map(p => p.copy(flags = p.flags.copy(mod = true)))
+      for p <- ps if p.flags.mod do p.sign match
+        case N =>
+          raise(ErrorReport(msg"Module parameters must have explicit types." -> t.toLoc :: Nil))
+        case S(ret) if ModuleChecker.isTypeParam(ret) => 
+          raise(ErrorReport(msg"Module parameters must have concrete types." -> t.toLoc :: Nil))
+        case _ => ()
+      ps
     case TermDef(ImmutVal, inner, _) => param(inner)
 
   def params(t: Tree): Ctxl[(Ls[Param], Ctx)] = t match
@@ -682,7 +689,15 @@ extends Importer:
     while trav.changed do
       trav.changed = false
       go(s)
+  
+  object ModuleChecker:
 
+    /** Checks if a term is a reference to a type parameter. */
+    def isTypeParam(t: Term): Bool = t.symbol
+      .filter(_.isInstanceOf[VarSymbol])
+      .flatMap(_.asInstanceOf[VarSymbol].decl)
+      .fold(false)(_.isInstanceOf[TyParam])
+  
   class VarianceTraverser(var changed: Bool = true) extends Traverser:
     override def traverseType(pol: Pol)(trm: Term): Unit = trm match
       case Term.TyApp(lhs, targs) =>

hkmc2/shared/src/test/mlscript/basics/ModuleMethods.mls

@@ -12,11 +12,15 @@ module M with {
 
 :e
 fun f1(module m)
-//│ FAILURE: Unexpected lack of type error
+//│ ╔══[ERROR] Module parameters must have explicit types.
+//│ ║  l.14: 	fun f1(module m)
+//│ ╙──      	              ^
 
 :e
 fun f2[T](module m: T)
-//│ FAILURE: Unexpected lack of type error
+//│ ╔══[ERROR] Module parameters must have concrete types.
+//│ ║  l.20: 	fun f2[T](module m: T)
+//│ ╙──      	                 ^^^^
 
 :e
 module N with {