diff --git a/Parser/Basic.lean b/Parser/Basic.lean
index a7e57301..8073c041 100644
--- a/Parser/Basic.lean
+++ b/Parser/Basic.lean
@@ -22,11 +22,11 @@ variable [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m]
 This is a low-level parser to customize how the parser stream is used.
 -/
 @[inline]
-def tokenCore (next? : σ → Option (τ × σ)) : ParserT ε σ τ m (ULift τ) := do
+def tokenCore (next? : σ → Option (τ × σ)) : ParserT ε σ τ m τ := do
   match next? (← getStream) with
   | some (tok, stream) =>
     let _ ← setStream stream
-    return ⟨tok⟩
+    return tok
   | none => throwUnexpected
 
 /--
@@ -35,7 +35,7 @@ the unexpected token.
 -/
 @[specialize]
 def tokenMap (test : τ → Option α) : ParserT ε σ τ m α := do
-  let ⟨tok⟩ ← tokenCore Stream.next?
+  let tok ← tokenCore Stream.next?
   match test tok with
   | some x => return x
   | none => throwUnexpected tok
@@ -192,6 +192,7 @@ returned values of `p`. Consumes no input on error.
 def takeManyN (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Array α) :=
   withBacktracking do foldl Array.push (← take n p) p
 
+set_option linter.checkUnivs false in
 /--
 `takeUntil stop p` parses zero or more occurrences of `p` until `stop` succeeds, and returns the
 array of returned values of `p` and the output of `stop`. If `p` fails before `stop` is encountered,
@@ -245,14 +246,14 @@ all outputs.
 -/
 @[inline]
 def dropMany1 (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit :=
-  withBacktracking p *> foldl (Function.const α) () p
+  withBacktracking p *> foldl (Function.const α) PUnit.unit p
 
 /--
 `dropManyN n p` parses `n` or more occurrences of `p` until it fails, ignoring all outputs.
 -/
 @[inline]
 def dropManyN (n : Nat) (p : ParserT ε σ τ m α) : ParserT ε σ τ m PUnit :=
-  withBacktracking do drop n p *> foldl (Function.const α) () p
+  withBacktracking do drop n p *> foldl (Function.const α) PUnit.unit p
 
 /--
 `dropUntil stop p` runs `p` until `stop` succeeds, returns the output of `stop` ignoring all
diff --git a/Parser/Parser.lean b/Parser/Parser.lean
index 0d6d1c09..db980558 100644
--- a/Parser/Parser.lean
+++ b/Parser/Parser.lean
@@ -11,7 +11,7 @@ public import Parser.Stream
 public section
 
 /-- Parser result type. -/
-protected inductive Parser.Result.{u} (ε σ α : Type u) : Type u
+protected inductive Parser.Result (ε σ α : Type _) : Type u
   /-- Result: success! -/
   | ok : σ → α → Parser.Result ε σ α
   /-- Result: error! -/
@@ -156,7 +156,7 @@ def withBacktracking (p : ParserT ε σ τ m α) : ParserT ε σ τ m α := do
 /--
 `withCapture p` parses `p` and returns the output of `p` with the corresponding stream segment.
 -/
-def withCapture {ε σ α : Type _} [Parser.Stream σ τ] [Parser.Error ε σ τ] (p : ParserT ε σ τ m α) :
+def withCapture (p : ParserT ε σ τ m α) :
   ParserT ε σ τ m (α × Stream.Segment σ) := do
   let startPos ← getPosition
   let x ← p
diff --git a/lake-manifest.json b/lake-manifest.json
index 7f84bbad..e373cd5e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cec0a48936f58f4dd77b9fdff7cd09f32104480b",
+   "rev": "3b873385fdbca8b43ee1e3310bf282743091a14d",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "460b61adc7d183e43db2b99ac6c1dede9f7a76df",
+   "rev": "954dbc9873f3b4534dc9896604593406d0383520",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index 462fae72..badfbfd0 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,6 @@
 name = "Parser"
 defaultTargets = ["Parser"]
+allowImportAll = true
 
 [[require]]
 name = "batteries"
diff --git a/lean-toolchain b/lean-toolchain
index 18640c8b..2694eb76 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.31.0
+leanprover/lean4:v4.32.0-rc1