Universe issue with a lot of typeclass calls

Stream: lean4

[Segev Elazar Mittelman]

stuck at solving universe constraint
?u.100581+1 =?= imax ?u.100541 ?u.100544
while trying to unify
(x : ?m.939) → ?m.942 x : Sort (imax ?u.100541 ?u.100544)
with
(x : ?m.939) → ?m.942 x : Sort (imax ?u.100541 ?u.100544)

I'm getting the above error at a bizzare place in a function which partially decides a typing relation for some language. Every toplevel match gives this error.

      | Nat.succ size' =>
        DecOpt.checkerBacktrack
          [fun _ =>
            match t_1 with
            | CedarType.boolType (BoolType.ff) =>
              match c_1 with
              | Prod.mk (CedarExpr.lit P) (PathSet.allpaths) =>
                DecOpt.andOptList
                  [DecOpt.decOpt (HasTypePrim b_1 P (CedarType.boolType (BoolType.ff))) initSize,
                    DecOpt.decOpt (HasTypePrim b_1 P (CedarType.boolType (BoolType.ff))) initSize]
              | _ => Option.some Bool.false
            | _ => Option.some Bool.false,
            fun _ =>
            match c_1 with
            | Prod.mk (CedarExpr.lit P) (PathSet.somepaths (List.nil)) =>
              DecOpt.andOptList
                [DecOpt.decOpt (HasTypePrim b_1 P t_1) initSize,
                  DecOpt.andOptList
                    [DecOpt.decOpt (Ne t_1 (CedarType.boolType (BoolType.ff))) initSize,
                      DecOpt.andOptList
                        [DecOpt.decOpt (HasTypePrim b_1 P t_1) initSize,
                          DecOpt.decOpt (Ne t_1 (CedarType.boolType (BoolType.ff))) initSize]]]
            | _ => Option.some Bool.false,
            fun _ =>
            match c_1 with
            | Prod.mk (CedarExpr.var X) (PathSet.somepaths (List.nil)) =>
              DecOpt.andOptList
                [DecOpt.decOpt (HasTypeVar b_1 X t_1) initSize, DecOpt.decOpt (HasTypeVar b_1 X t_1) initSize]
            | _ => Option.some Bool.false,

The errors disappear when I delete this much later case in this list:

            fun _ =>

            match t_1 with

            | CedarType.boolType (BoolType.anyBool) =>

              match c_1 with

              | Prod.mk (CedarExpr.binaryApp (BinaryOp.containsAny) E1 E2) (PathSet.somepaths (List.nil)) =>

                EnumeratorCombinators.enumerating Enum.enum

                  (fun ets =>

                    EnumeratorCombinators.enumeratingOpt

                      (EnumSizedSuchThat.enumSizedST (fun ns => DefinedEntities ets ns) initSize)

                      (fun ns =>

                        EnumeratorCombinators.enumerating Enum.enum

                          (fun T =>

                            DecOpt.andOptList

                              [DecOpt.decOpt (WfCedarType ns T) initSize,

                                EnumeratorCombinators.enumerating Enum.enum

                                  (fun T1 =>

                                    DecOpt.andOptList

                                      [DecOpt.decOpt (SubType T1 T) initSize,

                                        EnumeratorCombinators.enumerating Enum.enum

                                          (fun T2 =>

                                            DecOpt.andOptList

                                              [DecOpt.decOpt (SubType T2 T) initSize,

                                                EnumeratorCombinators.enumerating Enum.enum

                                                  (fun acts =>

                                                    EnumeratorCombinators.enumerating Enum.enum

                                                      (fun R =>

                                                        DecOpt.andOptList

                                                          [DecOpt.decOpt

                                                              (Eq b_1

                                                                (Environment.MkEnvironment (Schema.MkSchema ets acts)

                                                                  R))

                                                              initSize,

                                                            EnumeratorCombinators.enumerating Enum.enum

                                                              (fun x1 =>

                                                                DecOpt.andOptList

                                                                  [aux_dec initSize size' a_1 b_1 (Prod.mk E1 x1)

                                                                      (CedarType.setType T1),

                                                                    EnumeratorCombinators.enumerating Enum.enum

                                                                      (fun x2 =>

                                                                        aux_dec initSize size' a_1 b_1 (Prod.mk E2 x2)

                                                                          (CedarType.setType T2))

                                                                      (min 2 initSize)])

                                                              (min 2 initSize)])

                                                      (min 2 initSize))

                                                  (min 2 initSize)])

                                          (min 2 initSize)])

                                  (min 2 initSize)])

                          (min 2 initSize))

                      (min 2 initSize))

                  (min 2 initSize)

              | _ => Option.some Bool.false

            | _ => Option.some Bool.false,

])

I do not know why this happens, and I'm not sure how best to figure this out. Any advice would be greatly appreciated.

Best,
-Segev

[Segev Elazar Mittelman]

Very interestingly, this error also disappears if I annotate the _ in fun _ => as

fun (_ : Unit) =>
   match t_1 with ....

[Aaron Liu]

can you give a #mwe

[Segev Elazar Mittelman]

I can try to make one, but I suspect this problem is triggered by the sheer size of this function, I think the universe inference is getting overwhelmed. Just tried deleting all but the problematic section and the section that that causes an error in and the error also resolved.

[Aaron Liu]

that's not how universe inference works

[Aaron Liu]

if it was getting overwhelmed you would see something like (deterministic) timeout at 'whnf', maximum number of heatbeats (20000) has been reached

[Aaron Liu]

"stuck at solving universe constraint" is a different error