max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: example that requires the instance arg reordering

Browse source
This commit is contained in:
Daniel Selsam 2020-04-07 19:23:59 -07:00 • committed by Leonardo de Moura
parent fd61812b6e
commit 7c1c0dc01e
1 changed files with 33 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
tests/lean/run/typeclass_loop.lean Normal file
View file

@ -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
-/