Missing feature: generic predicate constructors

[necto]

Hello, it seems natural to have generic predicate_ctor as most of the other constructs in the annotation language. E.g. to define this kind of predicate constructors:

  predicate_ctor unimix<t>(predicate (void*,t) vp1,
                           predicate (void*,t) vp2)
                          (void* addr, t v) =
    [0.5]vp1(addr, v) &*& [0.5]vp2(addr, v);

this does not work: Parse error.
Is there a fundamental reason why it is not supported?

P.S. It does not disturb me much, as, unless the predicate is not recursive, I can embed it directly.

[btj]

No fundamental reason; we just haven't needed it so far. Note that in some cases, a workaround is to use a block-local predicate (which can be in the scope of a type parameter of the enclosing function).

[necto]

How hard would it be to implement such a feature?

[btj]

I think we need type reification (#125) for this to be sound.