Namespace notation might not be optimal, because it's not clear at a glance that this is an aspect and not a regular qualified import of a type (an important distinction if you have multiple versions of the same type imported, e.g. Bytestring). Why not make it look like type application instead? Modifying your example:

allEven :: (Integral a) => [a] -> Bool@A_All_

And for that matter, I'd rather not be forced to write a signature (what if I want to use this in a where clause?) So... does this break anything?

allEven = foldMap@A_All_ even

Which means, for this invocation of foldMap, instances within A_All_ are in effect for all of its constraints. You could chain multiple @'s together so long as they don't produce any relevant overlapping instances.

Good point, and it brought up some interesting follow-up thoughts. First of all I like this "annotative" notation vs stating aspects in constraints. The main reason is that the latter would make type signatures even worse:

	allEven :: (Integral a, b ~ Bool, HasAspect A_All_ b) => [a] -> b

But before I go on, let's first introduce better names and start at

	allEven :: (Integral a) => [a] -> Bool@Conjunctive

At first glance I thought your suggested notation might clash with TypeApplication. But then I noticed that no, it's actually more of a TypeAnnotation-like kind annotation. That might mean that this exact syntax should stay untouched in case we want some more general kind annotations later. So maybe something like this with a different operator? Another conclusion of that is that maybe we would want to apply aspect annotations inside TypeAnnotations. I imagine that might look something like (Maybe @Bool@Disjunctive). So the @ sign does make sense. Combining both thoughts, maybe an operator like "@+" would be best, because in a way the aspect is added to the type. And if other kind applications should be added later they could still use the @. So to step outside of TypeApplication again, the example would now look something like

	allEven :: (Integral a) => [a] -> Bool @+Conjunctive

or, to keep the function signature clean

	allEven :: (Integral a) => [a] -> Bool
	allEven = (foldMap even) :: Bool @+Conjunctive

Maybe there's some way to save a few bytes in this case like

	allEven :: (Integral a) => [a] -> Bool
	allEven = foldMap even :: @@+Conjunctive -- a step back to TypeApplication

Chaining several aspects would be straightforward: (Bool @+Disjunctive@+Conjunctive) (here it produces a conflict), (Maybe @a@+Multiplicative@+Distributive) etc.

Looking at this as a type with an operator leads in yet a completely different direction: Could part of this already be implemented via type families? Sadly not, for two reasons. Most importantly instances can not be hidden. To change that might be the most powerful result of this whole idea. The other part is also interesting. If "@+" was a type-level operator, its second argument would have to be an aspect. And seeing how aspects would be more or less restricted modules, this would open the question if modules should have a representation as a kind as well, the same way constraints do. I think that sounds really interesting. But neither aspects nor modules make sense as kinds until we also have some type level tools to work with them. Apart from those tools we would need here I have little idea what such tools might be, but it sounds worth exploring separately. For this particular proposal my conclusion is just that the implementation would have to be easy to adapt.

To avoid surprises, they shouldn't propagate -- when foldMap invokes even, it sees the default Monoid instance for Bool (i.e. none). If it were also a function that needs a Monoid, you'd need another @. There's potential for boilerplate here. Falling back to doing it in the type signature could force propagation? I'm not sure it's ever a safe idea, though.

That sounds like a gateway to inconsistency. I think the solution is that adding an aspect to, say, an Int would not apply that aspects to all Int's, but only to the ones unifying with the annotated one. So just like with any other type property. Or to tie this back to the beginning, I suppose the notation we're discussing here should actually just be syntactic sugar for something constraint-related. All propagation rules would follow from that in a natural fashion.

So much to think about…

Cheers,
MarLinn