PatternShadowsConstructor2.agda:12,9-10 The pattern variable x has the same name as the constructor A.x when checking the clause f (c y) x = x