Normalization problem

[aya-prover]

Normalization problem

[ice1000]

I'd like to assign @tsao-chi this time to investigate the issue.

[mio-19]

error given by aya:

      In file /home/user/aya-prover/base/src/test/resources/success/refparo5.aya:86:35 ->

      84 |   => new Event (new EventT { | agentT => Entity }) { | agent => john }
      85 | 
      86 | def proof-john-runs : john-runs => (proof-john-runs-event, (run1, (idp john, unit)))
                                              ^-----------------------------------------------^

    Error: Expected type: john-runs
           Normalized: Σ (e : Event new { | agentT ⇒ Entity }) ** (_ : Σ (_ : RunImpl e.agent)
           ** (_ : Σ (_ : Path (λ i ⇒ Entity) e.agent john) ** (_ : Unit)))
           Want: sigma type
           Because we want to type a term such as: (proof-john-runs-event, (run1, (idp
           john, unit)))
    What are you doing?

      In file /home/user/aya-prover/base/src/test/resources/success/refparo5.aya:92:35 ->

      90 |   => (proof-john-runs-event, (run1, (idp john, unit)))
      91 | 
      92 | def proof-john-runs : john-runs => proof-john-runs-impl
                                              ^------------------^

    Error: Expected type: john-runs
           Normalized: Σ (e : Event new { | agentT ⇒ Entity }) ** (_ : Σ (_ : RunImpl e.agent)
           ** (_ : Σ (_ : Path (λ i ⇒ Entity) e.agent john) ** (_ : Unit)))
           Actual type: Σ (e : Event new { | agentT ⇒ Entity }) (_ : Σ (_ : RunImpl john)
           (_ : Σ (_ : Path (λ _ ⇒ Entity) john john) (_ : Unit) ** (_ : Unit)) ** (_ : Σ
           (_ : Path (λ _ ⇒ Entity) john john) (_ : Unit) ** (_ : Unit))) ** (_ : Σ (_ : RunImpl
           john) (_ : Σ (_ : Path (λ _ ⇒ Entity) john john) (_ : Unit) ** (_ : Unit)) **
           (_ : Σ (_ : Path (λ _ ⇒ Entity) john john) (_ : Unit) ** (_ : Unit)))
           Normalized: Σ (e : Event new { | agentT ⇒ Entity }) (_ : Σ (_ : RunImpl john)
           (_ : Σ (_ : Path (λ _ ⇒ Entity) john john) (_ : Unit) ** (_ : Unit)) ** (_ : Σ
           (_ : Path (λ _ ⇒ Entity) john john) (_ : Unit) ** (_ : Unit))) ** (_ : Σ (_ : RunImpl
           john) (_ : Σ (_ : Path (λ _ ⇒ Entity) john john) (_ : Unit) ** (_ : Unit)) **
           (_ : Σ (_ : Path (λ _ ⇒ Entity) john john) (_ : Unit) ** (_ : Unit)))
           They don't match, sorry
    What are you doing?

I don't know where to hunt down the issue further.

[ice1000]

I don't know where to hunt down the issue further.

You can look at the place where the error is reported by putting a breakpoint at Reporter.report

[ice1000]

When you see Error: Expected type: john-runs, you can search in the codebase for Expected type:, and you'll get some results. You can find-usages these classes and see how they're used (where are they reported), and you can debug. You can tyck these code in your head to see if they should or should not tyck, and if the compiler does something different, one of you must be wrong. So you can fix the compiler or change your mind. This is how bug-fixing in Aya works.