typeside t schema s : t constraints c1 : s constraints c2 : s ---------------------------------- constraints (infer c1 -> c2 : s) : s