Illformed term produced by backend

[4ever2]

The streamlet TraceVerifier gives illformed $\lambda_\square$ terms when translated with the agda2lambox backend.

It fails with the following error when checking wellformedness.

Error while checking TraceVerifier.Streamlet.Protocol.⟦_⟧∗:
Constant not found in environment TraceVerifier.Streamlet.Protocol.⟦_⟧∗

The $\lambda_\square$ term:

(((MPfile ("Protocol" "Streamlet" "TraceVerifier")) "$10214_$10215$8727")
 (ConstantDecl (constant_body (Some 
 (tLambda nAnon 
  (tLambda nAnon 
    (tLambda nAnon 
      (tLetIn nAnon tBox
        (tCase ((inductive ((MPfile ("Protocol" "Streamlet" "TraceVerifier")) "ValidTrace") 0) 0) 
              (tRel 1)
              ((() (tApp (tConst ((MPfile ("Protocol" "Streamlet" "Global" "State")) "initGlobalState")) (tRel 3))) 
              ((nAnon nAnon nAnon nAnon) 
                (tApp 
                  (tApp 
                    (tApp 
                      (tApp 
                        (tConst ((MPfile ("Protocol" "Streamlet" "TraceVerifier")) "$10214_$10215")) 
                        (tRel 7)) 
                      (tRel 2)) 
                    (tApp 
                      (tApp 
                        (tApp 
                          (tConst ((MPfile ("Protocol" "Streamlet" "TraceVerifier")) "$10214_$10215$8727")) 
                          (tRel 7)) 
                        tBox) 
                      (tRel 1))) 
                  (tRel 0)))))))))))))

Protocol.Streamlet.TraceVerifier.$10214_$10215$8727:
  constant declaration:
    body: λ _ _ _ →
            let _ = □
            in case<Protocol.Streamlet.TraceVerifier.ValidTrace{0},0> @1 of
                 λ<[]> Protocol.Streamlet.Global.State.initGlobalState @3
                 λ<[_, _, _, _]>
                   Protocol.Streamlet.TraceVerifier.$10214_$10215 @7 @2
                     (Protocol.Streamlet.TraceVerifier.$10214_$10215$8727 @7 □ @1)
                     @0

[flupe]

Could be related to #10, as ⟦_⟧∗ and ValidTrace seem to be defined by induction-recursion.

[flupe]

Actually nothing to do with induction-recursion, for some reason ⟦_⟧∗ is recursive but the funMutuals field is not populated.

Compiling definition:  Protocol.Streamlet.TraceVerifier.⟦_⟧∗
Function mutuals: []
treeless body: λ a _ b →
                 let c = error "TUnreachable" in
                 case b of
                   Protocol.Streamlet.TraceVerifier.ValidTrace.[] →
                     Protocol.Streamlet.Global.State.initGlobalState a
                   Protocol.Streamlet.TraceVerifier.ValidTrace._∷_⊣_ _ d e f →
                     Protocol.Streamlet.TraceVerifier.⟦_⟧
                       a d (Protocol.Streamlet.TraceVerifier.⟦_⟧∗ a _ e) f

Well, it's not recursive per se, but a recursive call appears as a type-parameter in one of the branches. I have to investigate how to fix this.