Main.case block in case block in _ is not accessible in this context

63 views Asked by At

Walking through the format string example in the TDD of Idris2, and trying to do my own version of a format string. Here is what has worked:

data ShowableFmt = NatFmt | CharFmt | DoubleFmt
data CallableFmt = ShwFmt ShowableFmt | StrFmt
data Fmt = CalFmt CallableFmt Fmt | LitFmt String Fmt | EndFmt

FmtType: Fmt -> Type
FmtType fmt = case fmt of 
    EndFmt => String
    LitFmt lit fmt => FmtType fmt
    CalFmt callable fmt => case callable of
        ShwFmt shwfmt => case shwfmt of
            NatFmt => Nat -> FmtType fmt
            CharFmt => Char -> FmtType fmt
            DoubleFmt => Double -> FmtType fmt
        StrFmt => String -> FmtType fmt

So I decide to tidy up a little bit, as we can see -> FmtType fmt is all over the place. So I do the following, refactoring the repetitive part out and leaving the data type unchanged:

FmtType: Fmt -> Type
FmtType fmt = case fmt of 
    EndFmt => String
    LitFmt lit fmt => FmtType fmt
    CalFmt callable fmt => (case callable of
        ShwFmt shwfmt => case shwfmt of
            NatFmt => Nat
            CharFmt => Char
            DoubleFmt => Double
        StrFmt => String) -> FmtType fmt

Here is the error message:

Error: While processing right hand side of FmtType. Main.case block in case block in FmtType is not accessible in this context.

This kind of surprised me because I thought case expression is just a normal first class expression like any other expressions. Am I wrong?

0

There are 0 answers