> > I can't find anywhere a restriction that unary > > constructors must be applied to an argument pattern. > > I think the second side condition of rule 35 enforces it: the instantiated > type of the constructor must be of the form tau^(k) t Ah. This makes sense. Thanks.