Debug: Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = false
Debug: Starting resolution with 32 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded
Debug: Launching resolution fixpoint on 32 goals:
?X294 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.983 MetaCoq.Quotation.ToTemplate.Init.984} ?m6)
?X303 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.987 MetaCoq.Quotation.ToTemplate.Init.988} ?m7)
?X314 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.992 MetaCoq.Quotation.ToTemplate.Init.993} ?m8)
?X336 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1015 MetaCoq.Quotation.ToTemplate.Init.1016} ?m9)
?X345 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1017 MetaCoq.Quotation.ToTemplate.Init.1018} ?m10)
?X388 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1036 MetaCoq.Quotation.ToTemplate.Init.1037} ?T1)
?X397 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1038 MetaCoq.Quotation.ToTemplate.Init.1039} ?m2)
?X405 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1040 MetaCoq.Quotation.ToTemplate.Init.1041} ?m3)
?X420 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1047 MetaCoq.Quotation.ToTemplate.Init.1048} ?m)
?X430 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1051 MetaCoq.Quotation.ToTemplate.Init.1052} ?m20)
?X439 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1053 MetaCoq.Quotation.ToTemplate.Init.1054} ?m18)
?X445 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1055 MetaCoq.Quotation.ToTemplate.Init.1056} ?T7)
?X452 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1058 MetaCoq.Quotation.ToTemplate.Init.1059} ?m17)
?X461 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1060 MetaCoq.Quotation.ToTemplate.Init.1061} ?T8)
?X478 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1067 MetaCoq.Quotation.ToTemplate.Init.1068} ?T0)
?X486 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1069 MetaCoq.Quotation.ToTemplate.Init.1070} ?m4)
?X495 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1073 MetaCoq.Quotation.ToTemplate.Init.1074} ?T3@{c0:=cst_universes cb})
?X509 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1079 MetaCoq.Quotation.ToTemplate.Init.1080} ?m5)
?X543 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1099 MetaCoq.Quotation.ToTemplate.Init.1100} ?m0)
?X552 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1101 MetaCoq.Quotation.ToTemplate.Init.1102} ?T2)
?X565 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1107 MetaCoq.Quotation.ToTemplate.Init.1108} ?m1)
?X612 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1125 MetaCoq.Quotation.ToTemplate.Init.1126} ?m13)
?X620 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1127 MetaCoq.Quotation.ToTemplate.Init.1128} ?m12)
?X635 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1135 MetaCoq.Quotation.ToTemplate.Init.1136} ?m11)
?X652 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1146 MetaCoq.Quotation.ToTemplate.Init.1147} ?m14)
?X661 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1148 MetaCoq.Quotation.ToTemplate.Init.1149} ?T6)
?X674 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1154 MetaCoq.Quotation.ToTemplate.Init.1155} ?m15)
?X684 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1158 MetaCoq.Quotation.ToTemplate.Init.1159} ?m16)
?X694 : (Monad@{option_instance.u0 MetaCoq.Quotation.ToTemplate.Init.1161} TemplateMonad@{option_instance.u0
           MetaCoq.Quotation.ToTemplate.Init.1164})
?X704 : (Monad@{option_instance.u0 MetaCoq.Quotation.ToTemplate.Init.1166} TemplateMonad@{option_instance.u0
           MetaCoq.Quotation.ToTemplate.Init.1164})
?X714 : (Monad@{option_instance.u0 MetaCoq.Quotation.ToTemplate.Init.1168} TemplateMonad@{option_instance.u0
           MetaCoq.Quotation.ToTemplate.Init.1164})
?X756 : (Monad@{MetaCoq.Quotation.ToTemplate.Init.1193 MetaCoq.Quotation.ToTemplate.Init.1194} ?m19)
Debug:
Calling fixpoint on : 32 initial goals, 0 stuck goals and 0 non-stuck failures kept with no progress made in this run.
Stuck:
Failed:
Initial: Goal 1 evar: ?X294 status: initial
Goal 2 evar: ?X303 status: initial
Goal 3 evar: ?X314 status: initial
Goal 4 evar: ?X336 status: initial
Goal 5 evar: ?X345 status: initial
Goal 6 evar: ?X388 status: initial
Goal 7 evar: ?X397 status: initial
Goal 8 evar: ?X405 status: initial
Goal 9 evar: ?X420 status: initial
Goal 10 evar: ?X430 status: initial
Goal 11 evar: ?X439 status: initial
Goal 12 evar: ?X445 status: initial
Goal 13 evar: ?X452 status: initial
Goal 14 evar: ?X461 status: initial
Goal 15 evar: ?X478 status: initial
Goal 16 evar: ?X486 status: initial
Goal 17 evar: ?X495 status: initial
Goal 18 evar: ?X509 status: initial
Goal 19 evar: ?X543 status: initial
Goal 20 evar: ?X552 status: initial
Goal 21 evar: ?X565 status: initial
Goal 22 evar: ?X612 status: initial
Goal 23 evar: ?X620 status: initial
Goal 24 evar: ?X635 status: initial
Goal 25 evar: ?X652 status: initial
Goal 26 evar: ?X661 status: initial
Goal 27 evar: ?X674 status: initial
Goal 28 evar: ?X684 status: initial
Goal 29 evar: ?X694 status: initial
Goal 30 evar: ?X704 status: initial
Goal 31 evar: ?X714 status: initial
Goal 32 evar: ?X756 status: initial
Debug: considering goal 1 of status initial
Debug:
1: looking for (Monad@{MetaCoq.Quotation.ToTemplate.Init.983 MetaCoq.Quotation.ToTemplate.Init.984} ?m6) with backtracking
Debug: 1.1: exact TemplateMonad_Monad@{MetaCoq.Template.TemplateMonad.Core.17 MetaCoq.Template.TemplateMonad.Core.18} on
(Monad@{MetaCoq.Quotation.ToTemplate.Init.983 MetaCoq.Quotation.ToTemplate.Init.984} ?m6) failed with: Cannot unify TemplateMonad@{option_instance.u0
MetaCoq.Quotation.ToTemplate.Init.1163} and TemplateMonad@{option_instance.u0 MetaCoq.Quotation.ToTemplate.Init.1163}
Debug: 1.1: exact option_monad@{MetaCoq.Utils.monad_utils.16} on
(Monad@{MetaCoq.Quotation.ToTemplate.Init.983 MetaCoq.Quotation.ToTemplate.Init.984} ?m6) failed with: Cannot unify option and option
Debug:
1: no match for (Monad@{MetaCoq.Quotation.ToTemplate.Init.983 MetaCoq.Quotation.ToTemplate.Init.984} ?m6), 2 possibilities
Debug: Goal 1 has no more solutions, returning exception: NoApplicableHint