From 467d63dbb3c9605e700089e2c57e9fcb74c4c23c Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 11 Dec 2024 17:41:25 +0000
Subject: [PATCH] "fix" test

Turns out I had a typo in the argument list. The problem was not with implicit universes, rather it was with implicit parameters.
Also adds new testcases to expose this bug properly
---
 tests/lean/run/derivingToExpr.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
index 237b52ba5de7..f9b71309d4b3 100644
--- a/tests/lean/run/derivingToExpr.lean
+++ b/tests/lean/run/derivingToExpr.lean
@@ -61,10 +61,11 @@ inductive WithAmbientUniverse (α : Type u)
   | foo (a : α)
   deriving ToExpr
 
+set_option trace.Elab.Deriving.toExpr true in
 -- A test with: an ambient universe `u`, a directly specified universe `v`, and
 -- an implicit universe `w`
 universe u in
-structure WithAmbientUniverseTriple.{v} (α : Type u) (β : Type v) (y : Type w) where
+structure WithAmbientUniverseTriple.{v} (α : Type u) (β : Type v) (γ : Type w) where
   a : α
   b : β
   c : γ
@@ -95,3 +96,14 @@ structure ExplicitAmbientPair.{v} (α : Type u) (β : Type v) where
   deriving ToExpr
 
 end NoAutoImplicit
+
+-- Test with an implicit parameter to the inductive type
+inductive ImplicitParameter
+  | foo (a : α)
+  deriving ToExpr
+
+-- Test where the type parameter is a variable, with an implicit universe
+variable {α : Type u} in
+inductive VariableParameter : Type
+  | foo (a : α)
+  deriving ToExpr