Documentation

Right-folding over Data inside PLC currently hardcoded to only ever return Data as a result, 'cause we need to be able to map built-in lists and pairs in the definition of the right fold for Data and we can only do that monomorphically (see Note [Representable built-in functions over polymorphic built-in types]), which forces us to always return a Data . Alternatively we could convert built-in lists and pairs to their non-built-in Scott/Church-encoded forms, map polymorphically and convert back at the call site, but we really only use this definition as a test, so it's fine to make it overly specific for the sake of keeping the actual test trivial.

metaTypeLet r = data in
    \(fConstr : integer -> list r -> r)
     (fMap : list (pair r r) -> r)
     (fList : list r -> r)
     (fI : integer -> r)
     (fB : bytestring -> r) ->
         fix {data} {r} \(rec : data -> r) (d : data) ->
             caseData
                 d
                 {r}
                 (\(i : integer) (ds : list data) -> fConstr i (omapList {data} rec ds)
                 (\(es : list (pair data data)) ->
                     fMap (omapList {pair data data} (obothPair {data} rec) es))
                 (\(ds : list data) -> fList (omapList {data} rec ds))
                 fI
                 fB