From 7c1c0dc01eff1fee68f20eae65fb4223ca5e9387 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 7 Apr 2020 19:23:59 -0700 Subject: [PATCH] test: example that requires the instance arg reordering --- tests/lean/run/typeclass_loop.lean | 33 ++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/lean/run/typeclass_loop.lean diff --git a/tests/lean/run/typeclass_loop.lean b/tests/lean/run/typeclass_loop.lean new file mode 100644 index 0000000000..6483f497da --- /dev/null +++ b/tests/lean/run/typeclass_loop.lean @@ -0,0 +1,33 @@ +set_option trace.class_instances true + +example (M : Type → Type) [Monad M] : ExceptT Unit (ReaderT Unit (StateT Unit M)) Unit := do +ctx ← read; +pure () +/- +... +[class_instances] (1) ?x_8 : HasMonadLift + (ReaderT ?x_10 + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT + (OptionT (OptionT (OptionT (OptionT (OptionT (OptionT (OptionT (OptionT (OptionT (OptionT (OptionT List)))))))))))))))))))))))))))))) + (ExceptT Unit (ReaderT Unit (StateT Unit M))) := @ExceptT.exceptTOfExcept ?x_82 ?x_83 ?x_84 +failed is_def_eq +... +error: maximum class-instance resolution depth has been reached +-/