diff --git a/base/src/main/java/org/aya/primitive/PrimFactory.java b/base/src/main/java/org/aya/primitive/PrimFactory.java
index 30cd9b6ba2..760e71ac6a 100644
--- a/base/src/main/java/org/aya/primitive/PrimFactory.java
+++ b/base/src/main/java/org/aya/primitive/PrimFactory.java
@@ -7,6 +7,7 @@
 import java.util.function.Function;
 
 import static org.aya.syntax.core.def.PrimDef.*;
+import static org.aya.syntax.core.term.SortTerm.Set0;
 import static org.aya.syntax.core.term.SortTerm.Type0;
 
 import kala.collection.Map;
@@ -43,6 +44,7 @@ public PrimFactory() {
       stringConcat,
       intervalType,
       pathType,
+      partialType,
       coe
     ).map(seed -> Tuple.of(seed.name, seed)));
   }
@@ -129,6 +131,15 @@ public record PrimSeed(
     return new PrimCall(prim.ref(), prim.ulift(), ImmutableSeq.of(first, second));
   }
 
+  final @NotNull PrimSeed partialType = new PrimSeed(ID.PARTIAL, (prim, _) -> {
+    throw new UnsupportedOperationException("TODO");
+  }, ref -> {
+    var paramR = new Param("r", DimTyTerm.INSTANCE, true);
+    var paramS = new Param("s", DimTyTerm.INSTANCE, true);
+    var paramA = new Param("A", Type0, true);
+    return new PrimDef(ref, ImmutableSeq.of(paramR, paramS, paramA), Set0, ID.PARTIAL);
+  }, ImmutableSeq.of(ID.I));
+
   /*
   private final @NotNull PrimSeed hcomp = new PrimSeed(ID.HCOMP, this::hcomp, ref -> {
     var varA = new LocalVar("A");
diff --git a/base/src/main/java/org/aya/resolve/ResolvingStmt.java b/base/src/main/java/org/aya/resolve/ResolvingStmt.java
index ee273a1d88..3218d85a0c 100644
--- a/base/src/main/java/org/aya/resolve/ResolvingStmt.java
+++ b/base/src/main/java/org/aya/resolve/ResolvingStmt.java
@@ -1,9 +1,10 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.resolve;
 
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.resolve.context.Context;
+import org.aya.resolve.context.ModuleContext;
 import org.aya.syntax.concrete.stmt.Generalize;
 import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.concrete.stmt.decl.Decl;
@@ -38,6 +39,6 @@ sealed interface ResolvingDecl extends ResolvingStmt { }
 
   record TopDecl(@NotNull Decl stmt, @NotNull Context context) implements ResolvingDecl { }
   record MiscDecl(@NotNull Decl stmt) implements ResolvingDecl { }
-  record GenStmt(@NotNull Generalize stmt) implements ResolvingStmt { }
+  record GenStmt(@NotNull Generalize stmt, @NotNull ModuleContext context) implements ResolvingStmt { }
   record ModStmt(@NotNull ImmutableSeq<@NotNull ResolvingStmt> resolved) implements ResolvingStmt { }
 }
diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
index c3b2121656..ee5aaddca2 100644
--- a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java
@@ -99,7 +99,7 @@ public ImmutableSeq<ResolvingStmt> resolveStmt(@NotNull ImmutableSeq<Stmt> stmts
       case Generalize variables -> {
         for (var variable : variables.variables)
           context.defineSymbol(variable, Stmt.Accessibility.Private, variable.sourcePos);
-        yield new ResolvingStmt.GenStmt(variables);
+        yield new ResolvingStmt.GenStmt(variables, context);
       }
     };
   }
diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java
index 4c58dea905..d399e903d1 100644
--- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.resolve.visitor;
 
@@ -36,8 +36,8 @@ static void resolveStmt(@NotNull ResolvingStmt stmt, @NotNull ResolveInfo info)
     switch (stmt) {
       case ResolvingStmt.ResolvingDecl decl -> resolveDecl(decl, info);
       case ResolvingStmt.ModStmt(var stmts) -> resolveStmt(stmts, info);
-      case ResolvingStmt.GenStmt(var variables) -> {
-        var resolver = new ExprResolver(info.thisModule(), false);
+      case ResolvingStmt.GenStmt(var variables, var context) -> {
+        var resolver = new ExprResolver(context, false);
         resolver.enter(Where.Head);
         variables.descentInPlace(resolver, (_, p) -> p);
         addReferences(info, new TyckOrder.Head(variables), resolver);
diff --git a/ide-lsp/src/test/resources/lsp-test-lib/src/PathPrims.aya b/ide-lsp/src/test/resources/lsp-test-lib/src/PathPrims.aya
index 8af7393dce..f92d613016 100644
--- a/ide-lsp/src/test/resources/lsp-test-lib/src/PathPrims.aya
+++ b/ide-lsp/src/test/resources/lsp-test-lib/src/PathPrims.aya
@@ -1,3 +1,4 @@
 prim I
 prim coe (r s : I) (A : I -> Type) : A r -> A s
 prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
+prim Partial (r s : I) (A : Type) : Set
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java b/syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java
index 010e0fd221..5ea9f1b22d 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/PrimDef.java
@@ -55,12 +55,11 @@ public enum ID {
     STRCONCAT("strcat"),
     I("I"),
     PATH("Path"),
+    PARTIAL("Partial"),
     COE("coe"),
     HCOMP("hcom");
 
-    public final @NotNull
-    @NonNls String id;
-
+    public final @NotNull @NonNls String id;
     @Override public String toString() { return id; }
 
     public static @Nullable ID find(@NotNull String id) {