
1. ?U does not unify with anything
X1.foo.{u v} : Type u → Type (v+1) → Type (max u (v+1))

2. ?U unifies with a constant, no others above: done
X2.foo : Type 1

3. ?U unifies with a constant, and one above: error
inductive_resultant_level_inference.lean:35:0: error: universe level of type_of(arg #1) of 'X3.foo.mk' is too big for the corresponding inductive datatype

4. ?U unifies with a meta, but nesting recursor goes to Prop: error
inductive_resultant_level_inference.lean:46:0: error: invalid nested occurrence 'X4.bar.{1} X4.foo', either both must eliminate to Type or both must eliminate only to Prop

5. ?U unifies with a meta: old approach, set level-param
X5.foo.{u} : Sort u → Sort (max 1 u)

6. ?U unifies with a shifted meta, no others above: set level-param to be inverse of meta
X6.foo.{u} : Sort u → Type (u+2)

7. ?U unifies with a max: error
inductive_resultant_level_inference.lean:82:0: error: resultant level unifies with complex level 'max u_1 u_2', provide the universe levels explicitly

8. wrapping inductive returns element in different universe: error
inductive_resultant_level_inference.lean:92:0: error: nested occurrence 'X8.bar.{(max 1 v)} foo' lives in universe 'succ (max 1 v)' but must live in resultant universe 'max 1 v'

9. nesting with no other level params
X9.foo : Type

10. original 1343
X10.bug : Type

11. unifies with constant, result sort different: error
inductive_resultant_level_inference.lean:130:0: error: nested occurrence 'X11.foo bug' lives in universe '1' but must live in resultant universe '2'

12. multiple nestings
X12.bug : Type 1

13. ?U indirectly assigned to a constant
X13.bug : Type 4

14. No resultant level and lps are used in intro rule: error
inductive_resultant_level_inference.lean:175:2: error: resultant universe must be provided, when using explicit universe levels
