Datatype that has parameter but doesn't use it

[davidweichiang]

This program doesn't compile

data foo a = Bar | Baz;
data nat = Zero | Succ nat;
define f = \x: foo nat . (x, x);
f Bar

because foo nat is not positive (robust). Should it be?