Skip to content

Error: The conclusion of a builder is a mixin whose parameters depend on other mixins #474

@SamuelArsac

Description

@SamuelArsac

I have this error when trying to define an instance using a factory. Using a different factory for the same structure gave me a similar error.

I haven't been able to reproduce the error on a smaller example.

Here is the file where this happens (the instance definition is a the very bottom).

Linked to issue #432.

The full error message
The conclusion of a builder is a mixin whose parameters depend on other mixins: extract-conclusion-params c0 
 (prod `local_mixin_cat_IsQuiver` 
   (app [global (indt «IsQuiver.axioms_»), c0]) c1 \
   prod `local_mixin_cat_Quiver_IsPreCat` 
    (app [global (indt «Quiver_IsPreCat.axioms_»), c0, c1]) c2 \
    prod `local_mixin_cat_PreCat_IsCat` 
     (app [global (indt «PreCat_IsCat.axioms_»), c0, c1, c2]) c3 \
     prod `local_mixin_Pullback_Cat_has_pb` 
      (app [global (indt «Cat_has_pb.axioms_»), c0, c1, c2, c3]) c4 \
      prod `fresh_name_20` 
       (app
         [global (const «Cat_is_Adhesive_quasi.phant_axioms»), c0, c1, c2, 
          c3, c4, c0, 
          app
           [global (const «id_phant»), 
            sort (typ «Cat_is_Adhesive_quasi.phant_axioms.u2»), c0], 
          app
           [global
             (const «Builders_19.Builders_19_𝐂__canonical__Pullback_Cat_pb»), 
            c0, c1, c2, c3, c4], 
          app
           [global (const «id_phant»), 
            sort (typ «Cat_is_Adhesive_quasi.phant_axioms.u4»), c0], 
          app [global (indc «Cat_pb.Class»), c0, c1, c2, c3, c4], 
          app
           [global (const «id_phant»), global (indt «Cat_pb.type»), 
            app
             [global
               (const
                 «Builders_19.Builders_19_𝐂__canonical__Pullback_Cat_pb»), 
              c0, c1, c2, c3, c4]], c1, 
          app
           [global (const «id_phant»), 
            app [global (indt «IsQuiver.axioms_»), c0], c1], c2, 
          app
           [global (const «id_phant»), 
            app [global (indt «Quiver_IsPreCat.axioms_»), c0, c1], c2], 
          c3, 
          app
           [global (const «id_phant»), 
            app [global (indt «PreCat_IsCat.axioms_»), c0, c1, c2], c3], 
          c4, 
          app
           [global (const «id_phant»), 
            app [global (indt «Cat_has_pb.axioms_»), c0, c1, c2, c3], c4], 
          app
           [global (const «id_phant»), 
            app [global (indt «Cat_pb.axioms_»), c0], 
            app [global (indc «Cat_pb.Class»), c0, c1, c2, c3, c4]]]) c5 \
       app
        [global (indt «Rm_Adhesive.Rm_Q_Adhesive_is_Rm_Adhesive.axioms_»), 
         c0, c1, c2, c3, c4, 
         app
          [global (const «Builders_1.HB_unnamed_factory_3»), c0, c1, c2, 
           c3, c4, 
           app
            [global (const «Builders_11.HB_unnamed_factory_13»), c0, c1, 
             c2, c3, c4, 
             app
              [global (const «Builders_19.HB_unnamed_factory_21»), c0, c1, 
               c2, c3, c4, c5]]], 
         app
          [global (const «Rm_Adhesive.Builders_1.HB_unnamed_factory_3»), 
           c0, c1, c2, c3, c4, 
           app
            [global (const «Builders_1.HB_unnamed_factory_3»), c0, c1, c2, 
             c3, c4, 
             app
              [global (const «Builders_11.HB_unnamed_factory_13»), c0, c1, 
               c2, c3, c4, 
               app
                [global (const «Builders_19.HB_unnamed_factory_21»), c0, 
                 c1, c2, c3, c4, c5]]], 
           app
            [global (const «Builders_1.HB_unnamed_factory_5»), c0, c1, c2, 
             c3, c4, 
             app
              [global (const «Builders_11.HB_unnamed_factory_13»), c0, c1, 
               c2, c3, c4, 
               app
                [global (const «Builders_19.HB_unnamed_factory_21»), c0, 
                 c1, c2, c3, c4, c5]]]]]) X0^1

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions