Typechecking errors in view when assigning to a constant with "role Simplify" annotation

[ComFreek]

The reproducing example below can be found in LATIN2: https://gl.mathhub.info/MMT/LATIN2/-/blob/devel/source/playground.mmt.

@florian-rabe Do you have any idea what the error could be?

This typechecks fine:

theory RoleSimplifyBug =
  include ☞latin:?TypedEquality ❙
  include ☞latin:?Proofs ❙
  my_rule : {A,a: tm A} ⊦ a ≐ a ❙ // ❘ role Simplify ❙
❚
view RoleSimplifyBug_view : ?RoleSimplifyBug -> ?RoleSimplifyBug =
  include ☞latin:?TypedEquality ❙
  my_rule = ?RoleSimplifyBug?my_rule ❙
❚

When commenting in the role Simplify for my_rule, I get:

1. the view's include errors with

   unknown error in declaration: general error: error while simplifying COMPOSE(composition)

2. the view's constant assignment errors with

   error while adding successfully parsed element latin:/playground?RoleSimplifyBug_view?[latin:/playground?RoleSimplifyBug]/my_rule: general error: error while simplifying {A,a:tm A}⊦a≐a (Pi [A : tp, a : (apply tm A)] (apply ded (apply equal A a a)))

[florian-rabe]

Does the view need include Proofs?

my_rule does not have the shape of a simplification rule. Or if it does, it would nonsensically rewrite a ---> a. That's probably causing errors downstream.

[ComFreek]

If I `include ☞latin:?Proofs in the view, I get

error while adding successfully parsed element latin:/playground?RoleSimplifyBug_view?[latin:/?Proofs]: add error: a declaration for the name [Proofs] already exists

That's the case independent of whether I have a ---> a or something like a ∘ a ---> a as my_rule:

theory RoleSimplifyBugABC =
  include ☞latin:?TypedEquality ❙
  include ☞latin:?Proofs ❙
  my_op   : {A: tp} tm A ⟶ tm A ⟶ tm A ❘ # 2 ∘ 3 prec 100 ❙
  my_rule : {A: tp,a: tm A} ⊦ my_op A a a ≐ a ❙ // ❘ role Simplify ❙
❚
view RoleSimplifyBug_view : ?RoleSimplifyBugABC -> ?RoleSimplifyBugABC =
  include ☞latin:?TypedEquality ❙
  include ☞latin:?Proofs ❙
  my_op = ?RoleSimplifyBugABC?my_op ❙
  my_rule = ?RoleSimplifyBugABC?my_rule ❙
❚

Perhaps we can discuss this tomorrow in our meeting.