Unification did not find a solution for the variables

module ERR1
  syntax L ::= "repeat"
             | "stop"
             | "either" L "or" L
  rule repeat ~> E => E
  rule stop ~> _ => .
  rule (either P or _) #as E:L => P ~> E
  rule (either _ or P) #as E:L => P ~> E
endmodule

Commands to reproduce: kompile --backend haskell err1.k krun -cPGM='either repeat or stop'

Console log:

kore-exec: [332574] Error (ErrorRewritesInstantiation):
    While rewriting the configuration:
        \and{SortGeneratedTopCell{}}(
            /* term: */
            /* Fl Fn D Sfa Cl */
            Lbl'-LT-'generatedTop'-GT-'{}(
                /* Fl Fn D Sfa Cl */
                Lbl'-LT-'k'-GT-'{}(
                    /* Fl Fn D Sfa Cl */
                    kseq{}(
                        /* Fl Fn D Sfa Cli */
                        /* Inj: */ inj{SortL{}, SortKItem{}}(
                            /* Fl Fn D Sfa Cl */ Lblstop'Unds'ERR1'Unds'L{}()
                        ),
                        /* Fl Fn D Sfa Cl */
                        kseq{}(
                            /* Fl Fn D Sfa Cli */
                            /* Inj: */ inj{SortL{}, SortKItem{}}(
                                /* Fl Fn D Sfa Cl */
                                Lbleither'Unds'or'UndsUnds'ERR1'Unds'L'Unds'L'Unds'L{}(
                                    /* Fl Fn D Sfa Cl */
                                    Lblrepeat'Unds'ERR1'Unds'L{}(),
                                    /* Fl Fn D Sfa Cl */
                                    Lblstop'Unds'ERR1'Unds'L{}()
                                )
                            ),
                            /* Fl Fn D Sfa Cl */ dotk{}()
                        )
                    )
                ),
                /* Fl Fn D Sfa Cl */
                Lbl'-LT-'generatedCounter'-GT-'{}(
                    /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
                )
            ),
        \and{SortGeneratedTopCell{}}(
            /* predicate: */
            /* D Sfa */ \top{SortGeneratedTopCell{}}(),
            /* substitution: */
            \top{SortGeneratedTopCell{}}()
        ))
    Unable to instantiate semantic rule at /home/vasil/work/K/k/k-distribution/k-tutorial/1_basic/03_parsing/err1.k:6:8-6:22
    Unification did not find a solution for the variables:
        RuleVar'Unds'0 RuleVar'Unds'DotVar1
    The unification solution was:
    \and{SortGeneratedTopCell{}}(
        /* term: */
        /* Spa */
        \rewrites{SortGeneratedTopCell{}}(
            /* Spa */
            \and{SortGeneratedTopCell{}}(
                /* D Sfa */ \top{SortGeneratedTopCell{}}(),
                /* Fn Sfa */
                Lbl'-LT-'generatedTop'-GT-'{}(
                    /* Fn Sfa */
                    Lbl'-LT-'k'-GT-'{}(
                        /* Fn Sfa */
                        kseq{}(
                            /* Fl Fn D Sfa Cli */
                            /* Inj: */ inj{SortL{}, SortKItem{}}(
                                /* Fl Fn D Sfa Cl */
                                Lblstop'Unds'ERR1'Unds'L{}()
                            ),
                            /* Fn Sfa */
                            append{}(
                                /* Fl Fn D Sfa */ RuleVar'Unds'0:SortK{},
                                /* Fl Fn D Sfa */ RuleVar'Unds'DotVar1:SortK{}
                            )
                        )
                    ),
                    /* Fl Fn D Sfa */
                    RuleVar'Unds'DotVar0:SortGeneratedCounterCell{}
                )
            ),
            /* Fl Fn D Spa */
            Lbl'-LT-'generatedTop'-GT-'{}(
                /* Fl Fn D Spa */
                Lbl'-LT-'k'-GT-'{}(
                    /* Fl Fn D Sfa */ RuleVar'Unds'DotVar1:SortK{}
                ),
                /* Fl Fn D Sfa */
                RuleVar'Unds'DotVar0:SortGeneratedCounterCell{}
            )
        ),
    \and{SortGeneratedTopCell{}}(
        /* predicate: */
        /* Sfa */
        \equals{SortK{}, SortGeneratedTopCell{}}(
            /* Fl Fn D Sfa Cl */
            kseq{}(
                /* Fl Fn D Sfa Cli */
                /* Inj: */ inj{SortL{}, SortKItem{}}(
                    /* Fl Fn D Sfa Cl */
                    Lbleither'Unds'or'UndsUnds'ERR1'Unds'L'Unds'L'Unds'L{}(
                        /* Fl Fn D Sfa Cl */ Lblrepeat'Unds'ERR1'Unds'L{}(),
                        /* Fl Fn D Sfa Cl */ Lblstop'Unds'ERR1'Unds'L{}()
                    )
                ),
                /* Fl Fn D Sfa Cl */ dotk{}()
            ),
            /* Fn Sfa */
            append{}(
                /* Fl Fn D Sfa */ RuleVar'Unds'0:SortK{},
                /* Fl Fn D Sfa */ RuleVar'Unds'DotVar1:SortK{}
            )
        ),
        /* substitution: */
        /* Spa */
        \equals{SortGeneratedCounterCell{}, SortGeneratedTopCell{}}(
            /* Fl Fn D Sfa */ RuleVar'Unds'DotVar0:SortGeneratedCounterCell{},
            /* Fl Fn D Sfa Cl */
            Lbl'-LT-'generatedCounter'-GT-'{}(
                /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
            )
        )
    ))
    Error! Please report this.
    CallStack (from HasCallStack):
      checkSubstitutionCoverage, called at src/Kore/Rewrite/RewriteStep.hs:239:13 in kore-0.55.0.0-FRX9PCSQ3EDF8aiIsr3fMb:Kore.Rewrite.RewriteStep
Created bug report: kore-exec.tar.gz
[Error] Critical: Backend crashed during rewriting with exit code 1

runtimeverification / haskell-backend

Unification did not find a solution for the variables #2913