diff --git a/api/src/main/java/org/aya/api/error/Problem.java b/api/src/main/java/org/aya/api/error/Problem.java
index 08ec724287..a43a1430e8 100644
--- a/api/src/main/java/org/aya/api/error/Problem.java
+++ b/api/src/main/java/org/aya/api/error/Problem.java
@@ -6,6 +6,7 @@
 import kala.collection.SeqLike;
 import kala.collection.immutable.ImmutableSeq;
 import kala.tuple.Tuple;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.util.WithPos;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.error.PrettyError;
@@ -34,7 +35,7 @@ enum Stage {
   }
 
   @NotNull SourcePos sourcePos();
-  @NotNull Doc describe();
+  @NotNull Doc describe(DistillerOptions options);
   @NotNull Severity level();
   default @NotNull Stage stage() {
     return Stage.OTHER;
@@ -74,7 +75,7 @@ default boolean isError() {
       case INFO -> Doc.plain("Info:");
       case ERROR -> Doc.plain("Error:");
     };
-    var doc = Doc.sep(tag, Doc.align(describe()));
+    var doc = Doc.sep(tag, Doc.align(describe(DistillerOptions.DEFAULT)));
     var hint = hint();
     return hint instanceof Doc.Empty ? doc : Doc.vcat(
       doc,
@@ -83,7 +84,7 @@ default boolean isError() {
   }
 
   default @NotNull String computeFullErrorMessage() {
-    if (sourcePos() == SourcePos.NONE) return describe().commonRender();
+    if (sourcePos() == SourcePos.NONE) return describe(DistillerOptions.DEFAULT).commonRender();
     return toPrettyError().toDoc().commonRender();
   }
 
diff --git a/api/src/main/java/org/aya/api/error/Reporter.java b/api/src/main/java/org/aya/api/error/Reporter.java
index de6b9b22d7..2920a271bc 100644
--- a/api/src/main/java/org/aya/api/error/Reporter.java
+++ b/api/src/main/java/org/aya/api/error/Reporter.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.api.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.pretty.doc.Doc;
 import org.jetbrains.annotations.ApiStatus;
 import org.jetbrains.annotations.NotNull;
@@ -28,7 +29,7 @@ default void reportString(@NotNull String s) {
         return Severity.INFO;
       }
 
-      @Override public @NotNull Doc describe() {
+      @Override public @NotNull Doc describe(DistillerOptions options) {
         return Doc.plain(s);
       }
     });
diff --git a/base/src/main/java/org/aya/concrete/desugar/error/LevelProblem.java b/base/src/main/java/org/aya/concrete/desugar/error/LevelProblem.java
index eed60f43c3..3ef55e3cf7 100644
--- a/base/src/main/java/org/aya/concrete/desugar/error/LevelProblem.java
+++ b/base/src/main/java/org/aya/concrete/desugar/error/LevelProblem.java
@@ -18,14 +18,14 @@ public sealed interface LevelProblem extends ExprProblem {
 
   record BadTypeExpr(@Override @NotNull Expr.AppExpr expr, int expected)
     implements LevelProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.english("Expected " + expected + " level(s)");
     }
   }
 
   record BadLevelExpr(@Override @NotNull Expr expr) implements LevelProblem {
-    @Override public @NotNull Doc describe() {
-      return Doc.sep(Doc.english("Expected level expression, got:"), expr.toDoc(DistillerOptions.DEFAULT));
+    @Override public @NotNull Doc describe(DistillerOptions options) {
+      return Doc.sep(Doc.english("Expected level expression, got:"), expr.toDoc(options));
     }
   }
 }
diff --git a/base/src/main/java/org/aya/concrete/desugar/error/OperatorProblem.java b/base/src/main/java/org/aya/concrete/desugar/error/OperatorProblem.java
index 75aa497c64..62b9f95e4e 100644
--- a/base/src/main/java/org/aya/concrete/desugar/error/OperatorProblem.java
+++ b/base/src/main/java/org/aya/concrete/desugar/error/OperatorProblem.java
@@ -3,6 +3,7 @@
 package org.aya.concrete.desugar.error;
 
 import kala.collection.mutable.Buffer;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.concrete.desugar.BinOpSet;
@@ -23,7 +24,7 @@ public record AmbiguousPredError(
       return Severity.ERROR;
     }
 
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.sep(
         Doc.english("Ambiguous operator precedence detected between"),
         Doc.styled(Style.code(), Doc.plain(op1)),
@@ -44,7 +45,7 @@ public record BindSelfError(@Override @NotNull SourcePos sourcePos) implements P
       return Severity.ERROR;
     }
 
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.english("Self bind is not allowed");
     }
   }
@@ -57,11 +58,10 @@ public record CircleError(
         .max(Comparator.comparingInt(SourcePos::endLine));
     }
 
-    @Override public @NotNull Doc describe() {
-      return Doc.cat(
+    @Override public @NotNull Doc describe(DistillerOptions options) {
+      return Doc.sep(
         Doc.english("Precedence circle found between"),
-        Doc.ONE_WS,
-        Doc.plain(items.view().map(BinOpSet.Elem::name).sorted().joinToString(", "))
+        Doc.commaList(items.view().map(BinOpSet.Elem::name).map(Doc::plain).sorted())
       );
     }
 
diff --git a/base/src/main/java/org/aya/concrete/parse/ParseError.java b/base/src/main/java/org/aya/concrete/parse/ParseError.java
index 5f288dadc4..385824708f 100644
--- a/base/src/main/java/org/aya/concrete/parse/ParseError.java
+++ b/base/src/main/java/org/aya/concrete/parse/ParseError.java
@@ -2,13 +2,14 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.parse;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
 import org.jetbrains.annotations.NotNull;
 
 public record ParseError(@Override @NotNull SourcePos sourcePos, @NotNull String message) implements Problem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.plain("Parser error: " + message);
   }
 
diff --git a/base/src/main/java/org/aya/concrete/remark/UnsupportedMarkdown.java b/base/src/main/java/org/aya/concrete/remark/UnsupportedMarkdown.java
index 4cd9a4c3e9..46f9af9c11 100644
--- a/base/src/main/java/org/aya/concrete/remark/UnsupportedMarkdown.java
+++ b/base/src/main/java/org/aya/concrete/remark/UnsupportedMarkdown.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.remark;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
@@ -18,7 +19,7 @@ public record UnsupportedMarkdown(
     return Severity.WARN;
   }
 
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.english("Unsupported markdown syntax: " + nodeName + ".");
   }
 }
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/AmbiguousNameError.java b/base/src/main/java/org/aya/concrete/resolve/error/AmbiguousNameError.java
index d871a138ee..5330566288 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/AmbiguousNameError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/AmbiguousNameError.java
@@ -4,6 +4,7 @@
 
 import kala.collection.Seq;
 import kala.collection.immutable.ImmutableSeq;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.concrete.stmt.QualifiedID;
 import org.aya.pretty.doc.Doc;
@@ -19,7 +20,7 @@ public record AmbiguousNameError(
     return Severity.ERROR;
   }
 
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.vcat(Doc.cat(
         Doc.english("The unqualified name"),
         Doc.styled(Style.code(), Doc.plain(name)),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/AmbiguousNameWarn.java b/base/src/main/java/org/aya/concrete/resolve/error/AmbiguousNameWarn.java
index 4119bd856b..af1189983a 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/AmbiguousNameWarn.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/AmbiguousNameWarn.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.resolve.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Style;
@@ -15,7 +16,7 @@ public record AmbiguousNameWarn(
     return Severity.WARN;
   }
 
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.vcat(Doc.sep(
       Doc.english("The name"),
       Doc.styled(Style.code(), Doc.plain(name)),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/DuplicateExportError.java b/base/src/main/java/org/aya/concrete/resolve/error/DuplicateExportError.java
index ee9f563d5a..06ed159780 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/DuplicateExportError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/DuplicateExportError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.resolve.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Style;
@@ -11,7 +12,7 @@ public record DuplicateExportError(
   @NotNull String name,
   @Override @NotNull SourcePos sourcePos
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The name"),
       Doc.styled(Style.code(), Doc.plain(name)),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/DuplicateModNameError.java b/base/src/main/java/org/aya/concrete/resolve/error/DuplicateModNameError.java
index 7593414e37..de394ea7db 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/DuplicateModNameError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/DuplicateModNameError.java
@@ -3,6 +3,7 @@
 package org.aya.concrete.resolve.error;
 
 import kala.collection.Seq;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.concrete.stmt.QualifiedID;
 import org.aya.pretty.doc.Doc;
@@ -13,7 +14,7 @@ public record DuplicateModNameError(
   @NotNull Seq<String> modName,
   @Override @NotNull SourcePos sourcePos
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The module name"),
       Doc.styled(Style.code(), Doc.plain(QualifiedID.join(modName))),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/DuplicateNameError.java b/base/src/main/java/org/aya/concrete/resolve/error/DuplicateNameError.java
index 39929d99ea..90650719ea 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/DuplicateNameError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/DuplicateNameError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.resolve.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.api.ref.Var;
 import org.aya.distill.BaseDistiller;
@@ -13,7 +14,7 @@ public record DuplicateNameError(
   @NotNull String name, @NotNull Var ref,
   @Override @NotNull SourcePos sourcePos
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The name"),
       Doc.plain(name),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/GeneralizedNotAvailableError.java b/base/src/main/java/org/aya/concrete/resolve/error/GeneralizedNotAvailableError.java
index 1028a73040..4554035f17 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/GeneralizedNotAvailableError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/GeneralizedNotAvailableError.java
@@ -10,10 +10,10 @@
 import org.jetbrains.annotations.NotNull;
 
 public record GeneralizedNotAvailableError(@Override @NotNull Expr expr) implements ExprProblem, ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The generalized variable"),
-      Doc.styled(Style.code(), expr.toDoc(DistillerOptions.DEFAULT)),
+      Doc.styled(Style.code(), expr.toDoc(options)),
       Doc.english("is not available here")
     );
   }
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/ModNameNotFoundError.java b/base/src/main/java/org/aya/concrete/resolve/error/ModNameNotFoundError.java
index 08abc26125..49b749e62f 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/ModNameNotFoundError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/ModNameNotFoundError.java
@@ -3,6 +3,7 @@
 package org.aya.concrete.resolve.error;
 
 import kala.collection.Seq;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.concrete.stmt.QualifiedID;
 import org.aya.pretty.doc.Doc;
@@ -13,7 +14,7 @@ public record ModNameNotFoundError(
   @NotNull Seq<String> modName,
   @Override @NotNull SourcePos sourcePos
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The module name"),
       Doc.styled(Style.code(), Doc.plain(QualifiedID.join(modName))),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/ModNotFoundError.java b/base/src/main/java/org/aya/concrete/resolve/error/ModNotFoundError.java
index 8d9691106f..d4e7aa9aac 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/ModNotFoundError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/ModNotFoundError.java
@@ -3,6 +3,7 @@
 package org.aya.concrete.resolve.error;
 
 import kala.collection.Seq;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.concrete.stmt.QualifiedID;
 import org.aya.pretty.doc.Doc;
@@ -13,7 +14,7 @@ public record ModNotFoundError(
   @NotNull Seq<String> modName,
   @Override @NotNull SourcePos sourcePos
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The module name"),
       Doc.styled(Style.code(), Doc.plain(QualifiedID.join(modName))),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/ModShadowingWarn.java b/base/src/main/java/org/aya/concrete/resolve/error/ModShadowingWarn.java
index 033d9f9ca6..8dbaeec371 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/ModShadowingWarn.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/ModShadowingWarn.java
@@ -3,6 +3,7 @@
 package org.aya.concrete.resolve.error;
 
 import kala.collection.Seq;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.concrete.stmt.QualifiedID;
 import org.aya.pretty.doc.Doc;
@@ -17,7 +18,7 @@ public record ModShadowingWarn(
     return Severity.WARN;
   }
 
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The module name"),
       Doc.styled(Style.code(), Doc.plain(QualifiedID.join(modName))),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/PrimDependencyError.java b/base/src/main/java/org/aya/concrete/resolve/error/PrimDependencyError.java
index fad40362a5..03c8115b8e 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/PrimDependencyError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/PrimDependencyError.java
@@ -3,6 +3,7 @@
 package org.aya.concrete.resolve.error;
 
 import kala.collection.immutable.ImmutableSeq;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.core.def.PrimDef;
 import org.aya.pretty.doc.Doc;
@@ -17,7 +18,7 @@ public record PrimDependencyError(
   @NotNull ImmutableSeq<PrimDef.ID> lack,
   @Override @NotNull SourcePos sourcePos
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     assert lack.isNotEmpty();
     return Doc.sep(
       Doc.plain("The prim"), Doc.styled(Style.code(), Doc.plain(name)),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/QualifiedNameNotFoundError.java b/base/src/main/java/org/aya/concrete/resolve/error/QualifiedNameNotFoundError.java
index 7e459c1c2c..b017610604 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/QualifiedNameNotFoundError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/QualifiedNameNotFoundError.java
@@ -3,6 +3,7 @@
 package org.aya.concrete.resolve.error;
 
 import kala.collection.Seq;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.concrete.stmt.QualifiedID;
 import org.aya.pretty.doc.Doc;
@@ -15,7 +16,7 @@ public record QualifiedNameNotFoundError(
   @NotNull String name,
   @Override @NotNull SourcePos sourcePos
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The qualified name"),
       Doc.styled(Style.code(),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/RedefinitionError.java b/base/src/main/java/org/aya/concrete/resolve/error/RedefinitionError.java
index 499cc94eae..4f1b11d4fa 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/RedefinitionError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/RedefinitionError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.resolve.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
@@ -13,7 +14,7 @@ public record RedefinitionError(
   @NotNull String name,
   @Override @NotNull SourcePos sourcePos
 ) implements Problem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(Doc.plain("Redefinition of"), Doc.plain(kind.prettyName),
       Doc.styled(Style.code(), Doc.plain(name)));
   }
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/ShadowingWarn.java b/base/src/main/java/org/aya/concrete/resolve/error/ShadowingWarn.java
index 7ea5a73d4a..f399881403 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/ShadowingWarn.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/ShadowingWarn.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.resolve.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Style;
@@ -15,7 +16,7 @@ public record ShadowingWarn(
     return Severity.WARN;
   }
 
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(Doc.english("The name"),
       Doc.styled(Style.code(), Doc.plain(name)),
       Doc.english("shadows a previous local definition from outer scope")
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/UnknownOperatorError.java b/base/src/main/java/org/aya/concrete/resolve/error/UnknownOperatorError.java
index 739ca72d44..7265a2f973 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/UnknownOperatorError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/UnknownOperatorError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.resolve.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Style;
@@ -11,7 +12,7 @@ public record UnknownOperatorError(
   @Override @NotNull SourcePos sourcePos,
   @NotNull String name
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("Unknown operator"),
       Doc.styled(Style.code(), Doc.plain(name)),
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/UnknownPrimError.java b/base/src/main/java/org/aya/concrete/resolve/error/UnknownPrimError.java
index db7aefeb95..29acfabb42 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/UnknownPrimError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/UnknownPrimError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.resolve.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
@@ -12,7 +13,7 @@ public record UnknownPrimError(
   @Override @NotNull SourcePos sourcePos,
   @NotNull String name
 ) implements Problem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.plain("Unknown primitive"),
       Doc.styled(Style.code(), Doc.plain(name)));
diff --git a/base/src/main/java/org/aya/concrete/resolve/error/UnqualifiedNameNotFoundError.java b/base/src/main/java/org/aya/concrete/resolve/error/UnqualifiedNameNotFoundError.java
index 3c52176f66..59fee8bb1c 100644
--- a/base/src/main/java/org/aya/concrete/resolve/error/UnqualifiedNameNotFoundError.java
+++ b/base/src/main/java/org/aya/concrete/resolve/error/UnqualifiedNameNotFoundError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.resolve.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.SourcePos;
 import org.aya.pretty.doc.Doc;
 import org.aya.pretty.doc.Style;
@@ -11,7 +12,7 @@ public record UnqualifiedNameNotFoundError(
   @NotNull String name,
   @Override @NotNull SourcePos sourcePos
 ) implements ResolveProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The name"),
       Doc.styled(Style.code(), Doc.plain(name)),
diff --git a/base/src/main/java/org/aya/core/visitor/Zonker.java b/base/src/main/java/org/aya/core/visitor/Zonker.java
index 10cf022470..2005bde561 100644
--- a/base/src/main/java/org/aya/core/visitor/Zonker.java
+++ b/base/src/main/java/org/aya/core/visitor/Zonker.java
@@ -3,6 +3,7 @@
 package org.aya.core.visitor;
 
 import kala.tuple.Unit;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.core.sort.Sort;
@@ -82,7 +83,7 @@ private void reportLevelSolverError(@NotNull SourcePos pos) {
   }
 
   public record UnsolvedMeta(@Override @NotNull SourcePos sourcePos) implements Problem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.plain("Unsolved meta");
     }
 
diff --git a/base/src/main/java/org/aya/tyck/error/BadTypeError.java b/base/src/main/java/org/aya/tyck/error/BadTypeError.java
index c67094e184..cc0c7494ca 100644
--- a/base/src/main/java/org/aya/tyck/error/BadTypeError.java
+++ b/base/src/main/java/org/aya/tyck/error/BadTypeError.java
@@ -20,13 +20,13 @@ public record BadTypeError(
     return Severity.ERROR;
   }
 
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.vcat(
       Doc.sep(Doc.english("Unable to"), action, Doc.english("the expression")),
-      Doc.par(1, expr.toDoc(DistillerOptions.DEFAULT)),
+      Doc.par(1, expr.toDoc(options)),
       Doc.sep(Doc.english("because the type"), thing, Doc.english("is not a"), Doc.cat(desired, Doc.plain(",")), Doc.english("but instead:")),
-      Doc.par(1, actualType.toDoc(DistillerOptions.DEFAULT)),
-      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), actualType.normalize(NormalizeMode.NF).toDoc(DistillerOptions.DEFAULT))))
+      Doc.par(1, actualType.toDoc(options)),
+      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), actualType.normalize(NormalizeMode.NF).toDoc(options))))
     );
   }
 
diff --git a/base/src/main/java/org/aya/tyck/error/ClausesProblem.java b/base/src/main/java/org/aya/tyck/error/ClausesProblem.java
index 9fb5431b00..e304ab8e36 100644
--- a/base/src/main/java/org/aya/tyck/error/ClausesProblem.java
+++ b/base/src/main/java/org/aya/tyck/error/ClausesProblem.java
@@ -34,12 +34,12 @@ record Conditions(
     @NotNull SourcePos conditionPos,
     @NotNull SourcePos iPos, @Nullable SourcePos jPos
   ) implements ClausesProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       var result = rhs != null ? Doc.sep(
         Doc.plain("unify"),
-        Doc.styled(Style.code(), lhs.toDoc(DistillerOptions.DEFAULT)),
+        Doc.styled(Style.code(), lhs.toDoc(options)),
         Doc.plain("and"),
-        Doc.styled(Style.code(), rhs.toDoc(DistillerOptions.DEFAULT))
+        Doc.styled(Style.code(), rhs.toDoc(options))
       ) : Doc.english("even reduce one of the clause(s) to check condition");
       return Doc.sep(
         Doc.plain("The"),
@@ -65,7 +65,7 @@ record Confluence(
     @NotNull Term lhs, @NotNull Term rhs,
     @NotNull SourcePos iPos, @NotNull SourcePos jPos
   ) implements ClausesProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.sep(
           Doc.plain("The"),
@@ -73,9 +73,9 @@ record Confluence(
           Doc.english("and the"),
           Doc.ordinal(j),
           Doc.english("clauses are not confluent because we failed to unify")),
-        Doc.par(1, lhs.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, lhs.toDoc(options)),
         Doc.plain("and"),
-        Doc.par(1, rhs.toDoc(DistillerOptions.DEFAULT))
+        Doc.par(1, rhs.toDoc(options))
       );
     }
 
@@ -92,16 +92,16 @@ record MissingCase(
     @Override @NotNull SourcePos sourcePos,
     @NotNull ImmutableSeq<Pattern> pats
   ) implements ClausesProblem {
-    @Override public @NotNull Doc describe() {
-      return Doc.sep(Doc.english("Unhandled case:"), Doc.commaList(pats.map(t -> t.toDoc(DistillerOptions.DEFAULT))));
+    @Override public @NotNull Doc describe(DistillerOptions options) {
+      return Doc.sep(Doc.english("Unhandled case:"), Doc.commaList(pats.map(t -> t.toDoc(options))));
     }
   }
 
   record SplitInterval(@Override @NotNull SourcePos sourcePos, @NotNull Pat pat) implements ClausesProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.sep(
         Doc.english("Cannot perform pattern matching"),
-        Doc.styled(Style.code(), pat.toDoc(DistillerOptions.DEFAULT))
+        Doc.styled(Style.code(), pat.toDoc(options))
       );
     }
   }
diff --git a/base/src/main/java/org/aya/tyck/error/CounterexampleError.java b/base/src/main/java/org/aya/tyck/error/CounterexampleError.java
index c7924167d5..68c9df13e1 100644
--- a/base/src/main/java/org/aya/tyck/error/CounterexampleError.java
+++ b/base/src/main/java/org/aya/tyck/error/CounterexampleError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.api.ref.Var;
@@ -10,7 +11,7 @@
 import org.jetbrains.annotations.NotNull;
 
 public record CounterexampleError(@Override @NotNull SourcePos sourcePos, @NotNull Var var) implements Problem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("The counterexample"),
       BaseDistiller.varDoc(var),
diff --git a/base/src/main/java/org/aya/tyck/error/FieldProblem.java b/base/src/main/java/org/aya/tyck/error/FieldProblem.java
index 3c81f89b9d..5a573f309f 100644
--- a/base/src/main/java/org/aya/tyck/error/FieldProblem.java
+++ b/base/src/main/java/org/aya/tyck/error/FieldProblem.java
@@ -3,6 +3,7 @@
 package org.aya.tyck.error;
 
 import kala.collection.immutable.ImmutableSeq;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.api.ref.Var;
@@ -16,7 +17,7 @@ record MissingFieldError(
     @Override @NotNull SourcePos sourcePos,
     @NotNull ImmutableSeq<Var> missing
   ) implements FieldProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.sep(Doc.english("Missing field(s):"), Doc.commaList(missing.view()
         .map(BaseDistiller::varDoc)
         .map(m -> Doc.styled(Style.code(), m))));
@@ -30,7 +31,7 @@ record NoSuchFieldError(
     @NotNull SourcePos sourcePos,
     @NotNull ImmutableSeq<String> notFound
   ) implements FieldProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.sep(Doc.english("No such field(s):"),
         Doc.commaList(notFound.view()
           .map(m -> Doc.styled(Style.code(), Doc.plain(m))))
diff --git a/base/src/main/java/org/aya/tyck/error/Goal.java b/base/src/main/java/org/aya/tyck/error/Goal.java
index bfbf712c1a..e8212e8bd6 100644
--- a/base/src/main/java/org/aya/tyck/error/Goal.java
+++ b/base/src/main/java/org/aya/tyck/error/Goal.java
@@ -13,15 +13,15 @@
 import org.jetbrains.annotations.NotNull;
 
 public record Goal(@NotNull CallTerm.Hole hole, ImmutableSeq<LocalVar> scope) implements Problem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     var meta = hole.ref().core();
     var doc = Doc.vcatNonEmpty(
       Doc.english("Goal of type"),
-      Doc.par(1, meta.result.toDoc(DistillerOptions.DEFAULT)),
-      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), meta.result.normalize(NormalizeMode.NF).toDoc(DistillerOptions.DEFAULT)))),
+      Doc.par(1, meta.result.toDoc(options)),
+      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), meta.result.normalize(NormalizeMode.NF).toDoc(options)))),
       Doc.plain("Context:"),
       Doc.vcat(meta.fullTelescope().map(param -> {
-        var paramDoc = param.toDoc(DistillerOptions.DEFAULT);
+        var paramDoc = param.toDoc(options);
         return Doc.par(1, scope.contains(param.ref()) ? paramDoc : Doc.sep(paramDoc, Doc.parened(Doc.english("not in scope"))));
       })),
       meta.conditions.value.isNotEmpty() ?
@@ -29,14 +29,14 @@ public record Goal(@NotNull CallTerm.Hole hole, ImmutableSeq<LocalVar> scope) im
           ImmutableSeq.of(Doc.plain("To ensure confluence:"))
             .concat(meta.conditions.value.map(tup -> Doc.par(1, Doc.cat(
               Doc.plain("Given "),
-              Doc.parened(tup._1.toDoc(DistillerOptions.DEFAULT)),
+              Doc.parened(tup._1.toDoc(options)),
               Doc.plain(", we should have: "),
-              tup._2.toDoc(DistillerOptions.DEFAULT)
+              tup._2.toDoc(options)
             )))))
         : Doc.empty()
     );
     return meta.body == null ? doc :
-      Doc.vcat(Doc.plain("Candidate exists:"), Doc.par(1, meta.body.toDoc(DistillerOptions.DEFAULT)), doc);
+      Doc.vcat(Doc.plain("Candidate exists:"), Doc.par(1, meta.body.toDoc(options)), doc);
   }
 
   @Override public @NotNull SourcePos sourcePos() {
diff --git a/base/src/main/java/org/aya/tyck/error/HoleProblem.java b/base/src/main/java/org/aya/tyck/error/HoleProblem.java
index 4266ffc8b6..3d05fa61a8 100644
--- a/base/src/main/java/org/aya/tyck/error/HoleProblem.java
+++ b/base/src/main/java/org/aya/tyck/error/HoleProblem.java
@@ -31,10 +31,10 @@ record BadSpineError(
     @Override @NotNull CallTerm.Hole term,
     @Override @NotNull SourcePos sourcePos
   ) implements HoleProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.english("Can't perform pattern unification on hole with the following spine:"),
-        Doc.commaList(term.args().map(a -> a.toDoc(DistillerOptions.DEFAULT)))
+        Doc.commaList(term.args().map(a -> a.toDoc(options)))
       );
     }
   }
@@ -45,10 +45,10 @@ record BadlyScopedError(
     @NotNull Seq<LocalVar> scopeCheck,
     @Override @NotNull SourcePos sourcePos
   ) implements HoleProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.english("The solution"),
-        Doc.par(1, solved.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, solved.toDoc(options)),
         Doc.plain("is not well-scoped"),
         Doc.cat(Doc.english("In particular, these variables are not in scope:"),
           Doc.ONE_WS,
@@ -66,13 +66,13 @@ record RecursionError(
     @NotNull Term sol,
     @Override @NotNull SourcePos sourcePos
   ) implements HoleProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.sep(
           Doc.english("Trying to solve hole"),
           Doc.styled(Style.code(), BaseDistiller.linkDef(term.ref())),
           Doc.plain("as")),
-        Doc.par(1, sol.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, sol.toDoc(options)),
         Doc.english("which is recursive"));
     }
   }
@@ -85,10 +85,10 @@ record CannotFindGeneralSolution(
     }
 
     @Override public @NotNull SeqLike<WithPos<Doc>> inlineHints() {
-      return eqns.map(eqn -> new WithPos<>(eqn.pos(), eqn.toDoc(DistillerOptions.DEFAULT)));
+      return eqns.map(eqn -> new WithPos<>(eqn.pos(), eqn.toDoc(options)));
     }
 
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.english("Solving equation(s) with not very general solution(s)");
     }
 
diff --git a/base/src/main/java/org/aya/tyck/error/LevelMismatchError.java b/base/src/main/java/org/aya/tyck/error/LevelMismatchError.java
index 95eed92f48..b4f8d1a67c 100644
--- a/base/src/main/java/org/aya/tyck/error/LevelMismatchError.java
+++ b/base/src/main/java/org/aya/tyck/error/LevelMismatchError.java
@@ -17,10 +17,10 @@ public record LevelMismatchError(
   @Nullable SourcePos pos,
   @NotNull ImmutableSeq<LevelEqnSet.Eqn> eqns
 ) implements Problem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.vcat(Doc.english("Cannot solve the following level equation(s):"),
       Doc.nest(2, Doc.vcat(
-        eqns.map(eqn -> eqn.toDoc(DistillerOptions.DEFAULT)))));
+        eqns.map(eqn -> eqn.toDoc(options)))));
   }
 
   @Override public @NotNull SourcePos sourcePos() {
@@ -29,7 +29,7 @@ public record LevelMismatchError(
 
   @Override public @NotNull SeqLike<WithPos<Doc>> inlineHints() {
     return eqns.view().map(eqn ->
-      new WithPos<>(eqn.sourcePos(), eqn.toDoc(DistillerOptions.DEFAULT)));
+      new WithPos<>(eqn.sourcePos(), eqn.toDoc(options)));
   }
 
   @Override public @NotNull Severity level() {
diff --git a/base/src/main/java/org/aya/tyck/error/LicitProblem.java b/base/src/main/java/org/aya/tyck/error/LicitProblem.java
index 68d066393b..8df69c2c9e 100644
--- a/base/src/main/java/org/aya/tyck/error/LicitProblem.java
+++ b/base/src/main/java/org/aya/tyck/error/LicitProblem.java
@@ -19,12 +19,12 @@ public sealed interface LicitProblem extends Problem {
   }
 
   record LicitMismatchError(@Override @NotNull Expr expr, @NotNull Term type) implements LicitProblem, ExprProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.english("Cannot check"),
-        Doc.par(1, expr.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, expr.toDoc(options)),
         Doc.english("against the Pi type"),
-        Doc.par(1, type.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, type.toDoc(options)),
         Doc.english("because explicitness do not match"));
     }
   }
@@ -34,9 +34,9 @@ record UnexpectedImplicitArgError(@Override @NotNull Arg<Expr.NamedArg> expr) im
       return expr.term().expr().sourcePos();
     }
 
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.sep(Doc.english("Unexpected implicit argument"),
-        Doc.styled(Style.code(), expr.toDoc(DistillerOptions.DEFAULT)));
+        Doc.styled(Style.code(), expr.toDoc(options)));
     }
   }
 }
diff --git a/base/src/main/java/org/aya/tyck/error/NotYetTyckedError.java b/base/src/main/java/org/aya/tyck/error/NotYetTyckedError.java
index 074bdaf0c1..31d7e9d533 100644
--- a/base/src/main/java/org/aya/tyck/error/NotYetTyckedError.java
+++ b/base/src/main/java/org/aya/tyck/error/NotYetTyckedError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourcePos;
 import org.aya.api.ref.Var;
@@ -11,7 +12,7 @@
 import org.jetbrains.annotations.NotNull;
 
 public record NotYetTyckedError(@Override @NotNull SourcePos sourcePos, @NotNull Var var) implements Problem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.cat(Doc.english("Attempting to use a definition"),
       Doc.styled(Style.code(), BaseDistiller.varDoc(var)),
       Doc.english("which is not yet typechecked"));
diff --git a/base/src/main/java/org/aya/tyck/error/PatternProblem.java b/base/src/main/java/org/aya/tyck/error/PatternProblem.java
index 5371725e46..067d6cfbc7 100644
--- a/base/src/main/java/org/aya/tyck/error/PatternProblem.java
+++ b/base/src/main/java/org/aya/tyck/error/PatternProblem.java
@@ -24,7 +24,7 @@ record PossiblePat(
     @Override @NotNull Pattern pattern,
     @NotNull CallTerm.ConHead available
   ) implements PatternProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.sep(
         Doc.english("Absurd pattern does not fit here because"),
         Doc.styled(Style.code(), BaseDistiller.varDoc(available.ref())),
@@ -38,12 +38,12 @@ record PossiblePat(
   }
 
   record SplittingOnNonData(@Override @NotNull Pattern pattern, @NotNull Term type) implements PatternProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.english("Cannot split on a non-inductive type"),
-        Doc.par(1, type.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, type.toDoc(options)),
         Doc.english("with a constructor pattern"),
-        Doc.par(1, pattern.toDoc(DistillerOptions.DEFAULT)));
+        Doc.par(1, pattern.toDoc(options)));
     }
 
     @Override public @NotNull Severity level() {
@@ -52,10 +52,10 @@ record SplittingOnNonData(@Override @NotNull Pattern pattern, @NotNull Term type
   }
 
   record UnavailableCtor(@Override @NotNull Pattern pattern, @NotNull Severity level) implements PatternProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.english("Cannot match with"),
-        Doc.par(1, pattern.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, pattern.toDoc(options)),
         Doc.cat(
           Doc.english("due to a failed index unification"),
           Doc.emptyIf(isError(), () -> Doc.english(", treating as bind pattern"))));
@@ -63,10 +63,10 @@ record UnavailableCtor(@Override @NotNull Pattern pattern, @NotNull Severity lev
   }
 
   record UnknownCtor(@Override @NotNull Pattern pattern) implements PatternProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.english("Unknown constructor"),
-        Doc.par(1, pattern.toDoc(DistillerOptions.DEFAULT))
+        Doc.par(1, pattern.toDoc(options))
       );
     }
 
@@ -76,12 +76,12 @@ record UnknownCtor(@Override @NotNull Pattern pattern) implements PatternProblem
   }
 
   record TupleNonSig(@Override @NotNull Pattern.Tuple pattern, @NotNull Term type) implements PatternProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.english("The tuple pattern"),
-        Doc.par(1, pattern.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, pattern.toDoc(options)),
         Doc.english("splits only on sigma types, while the actual type"),
-        Doc.par(1, type.freezeHoles(null).toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, type.freezeHoles(null).toDoc(options)),
         Doc.english("does not look like one"));
     }
 
@@ -91,12 +91,12 @@ record TupleNonSig(@Override @NotNull Pattern.Tuple pattern, @NotNull Term type)
   }
 
   record TooManyPattern(@Override @NotNull Pattern pattern, @NotNull Term retTy) implements PatternProblem {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.vcat(
         Doc.english("There is no parameter for the pattern"),
-        Doc.par(1, pattern.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, pattern.toDoc(options)),
         Doc.english("to match against, given the return type"),
-        Doc.par(1, retTy.toDoc(DistillerOptions.DEFAULT)),
+        Doc.par(1, retTy.toDoc(options)),
         Doc.parened(Doc.sep(
           Doc.english("and in case it's a function type, you may want to move its parameters before the"),
           Doc.styled(Style.code(), ":"),
diff --git a/base/src/main/java/org/aya/tyck/error/ProjIxError.java b/base/src/main/java/org/aya/tyck/error/ProjIxError.java
index 70a7431d8a..bb3596d0bb 100644
--- a/base/src/main/java/org/aya/tyck/error/ProjIxError.java
+++ b/base/src/main/java/org/aya/tyck/error/ProjIxError.java
@@ -2,13 +2,14 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.ExprProblem;
 import org.aya.concrete.Expr;
 import org.aya.pretty.doc.Doc;
 import org.jetbrains.annotations.NotNull;
 
 public record ProjIxError(@Override @NotNull Expr.ProjExpr expr, int actual, int expectedBound) implements ExprProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.sep(
       Doc.english("Cannot project the"),
       Doc.ordinal(actual),
diff --git a/base/src/main/java/org/aya/tyck/error/UnifyError.java b/base/src/main/java/org/aya/tyck/error/UnifyError.java
index 07f69ad87d..f184d0aeb3 100644
--- a/base/src/main/java/org/aya/tyck/error/UnifyError.java
+++ b/base/src/main/java/org/aya/tyck/error/UnifyError.java
@@ -15,14 +15,14 @@ public record UnifyError(
   @NotNull Term expected,
   @NotNull Term actual
 ) implements ExprProblem {
-  @Override public @NotNull Doc describe() {
+  @Override public @NotNull Doc describe(DistillerOptions options) {
     return Doc.vcat(
       Doc.english("Cannot check the expression of type"),
-      Doc.par(1, actual.toDoc(DistillerOptions.DEFAULT)),
-      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), actual.normalize(NormalizeMode.NF).toDoc(DistillerOptions.DEFAULT)))),
+      Doc.par(1, actual.toDoc(options)),
+      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), actual.normalize(NormalizeMode.NF).toDoc(options)))),
       Doc.english("against the type"),
-      Doc.par(1, expected.toDoc(DistillerOptions.DEFAULT)),
-      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), expected.normalize(NormalizeMode.NF).toDoc(DistillerOptions.DEFAULT))))
+      Doc.par(1, expected.toDoc(options)),
+      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), expected.normalize(NormalizeMode.NF).toDoc(options))))
     );
   }
 
diff --git a/base/src/main/java/org/aya/tyck/error/UnivArgsError.java b/base/src/main/java/org/aya/tyck/error/UnivArgsError.java
index 9d3ad4c3ff..a6cf8f3146 100644
--- a/base/src/main/java/org/aya/tyck/error/UnivArgsError.java
+++ b/base/src/main/java/org/aya/tyck/error/UnivArgsError.java
@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.error;
 
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.ExprProblem;
 import org.aya.concrete.Expr;
 import org.aya.pretty.doc.Doc;
@@ -13,7 +14,7 @@ public sealed interface UnivArgsError extends ExprProblem {
   }
 
   record SizeMismatch(@NotNull Expr.UnivArgsExpr expr, int expected) implements UnivArgsError {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.sep(Doc.plain("Expected"), Doc.plain(String.valueOf(expected)),
         Doc.english("universe arguments, but"),
         Doc.plain(String.valueOf(expr.univArgs().size())),
@@ -22,7 +23,7 @@ record SizeMismatch(@NotNull Expr.UnivArgsExpr expr, int expected) implements Un
   }
 
   record Misplaced(@NotNull Expr.UnivArgsExpr expr) implements UnivArgsError {
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return Doc.english("Universe argument should not be placed here");
     }
   }
diff --git a/lsp/src/main/java/org/aya/lsp/server/AyaService.java b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
index c0ea6efb20..707fe136f1 100644
--- a/lsp/src/main/java/org/aya/lsp/server/AyaService.java
+++ b/lsp/src/main/java/org/aya/lsp/server/AyaService.java
@@ -7,6 +7,7 @@
 import kala.collection.mutable.Buffer;
 import kala.collection.mutable.MutableHashMap;
 import kala.tuple.Tuple;
+import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.CollectingReporter;
 import org.aya.api.error.Problem;
 import org.aya.api.error.SourceFileLocator;
@@ -90,7 +91,7 @@ public void reportErrors(@NotNull CollectingReporter reporter) {
       Log.publishProblems(new PublishDiagnosticsParams(f.toUri().toString(), Collections.emptyList())));
     var diags = reporter.problems().stream()
       .filter(p -> p.sourcePos().belongsToSomeFile())
-      .peek(p -> Log.d(p.describe().debugRender()))
+      .peek(p -> Log.d(p.describe(DistillerOptions.DEFAULT).debugRender()))
       .flatMap(p -> Stream.concat(Stream.of(p), p.inlineHints().stream().map(t -> new InlineHintProblem(p, t))))
       .flatMap(p -> p.sourcePos().file().path().stream().map(uri -> Tuple.of(uri, p)))
       .collect(Collectors.groupingBy(
@@ -199,7 +200,7 @@ public record InlineHintProblem(@NotNull Problem owner, WithPos<Doc> docWithPos)
       return docWithPos.sourcePos();
     }
 
-    @Override public @NotNull Doc describe() {
+    @Override public @NotNull Doc describe(DistillerOptions options) {
       return docWithPos.data();
     }
 
@@ -208,7 +209,7 @@ public record InlineHintProblem(@NotNull Problem owner, WithPos<Doc> docWithPos)
     }
 
     @Override public @NotNull Doc brief() {
-      return describe();
+      return describe(DistillerOptions.DEFAULT);
     }
   }
 }