I speak to much this same point in this old stack overflow response, though to exactly the opposite conclusion, and to exactly the opposite pet peeve.
https://stackoverflow.com/a/5316014/34707
Let me see if I can try to explain why I think reasonable people can disagree here and why I ultimately adopted the "wrong" vocabulary from your perspective.
To be explicit:
Viewing a type as a space, 'reify' in the reflection library takes some space 'a' and splits it into individual fibers for each term in 'a', finding the appropriate one and handing it back to you as a fresh type 's' that captures just that singular value. The result is significantly less abstract, as we gained detail on the type, now every point in the original space 'a' is a new space. At the type level the fresh 's' in s `Reifies` a now concretely names exactly one inhabitant of 'a'.
On the flip side, 'reflect' in the reflection library forgets this finer fibration / structure on space, losing the information about which fiber the answer came from, being forgetful is precisely the justification of it being the 'reflect' half of the reify -| reflect pairing.
I confess I don't necessarily anticipate this changing your mind but it was not chosen blindly, reflect is the forgetful mapping here, reification is free and left adjoint to it, at least in the context of reflection-the-library, where a quantifier is being injected to track the particular member.
This gets more muddled when you remove the quantifier, like here, now everything becomes the same size, nothing is being forgotten when you use "magicDict" to transform 5 :: Natural into dictionary for KnownNat (5 :: Nat) or use the single member of the dictionary to get your value back. If anything it goes the other way, because you _could_ evilly produce a dictionary from 6 :: Natural and nothing but your conscience stops you. But when used in a way that doesn't violate coherence of instance resolution, no finer fibration was introduced, reflect isn't forgetful, neither is reify, you produce singleton instances in a thin category from singleton types. In that framework, really neither term seems fully appropriate here -- or rather both do depending on your chosen perspective. This is where I believe the religious wars about which is concrete and which is abstract start up, because both uses satisfy that definition in this narrow case of isomorphism, no information is lost on either end.
It is only when you actually introduce a quantifier to ensure 's' is fresh (as it is used in the reflection library to ensure this doesn't compromise instance resolution safety in general) that there is a bias introduced and 'reflect' forgets this hallucinated structure, finally forcing a 'handedness' on the terminology to use.
I do not feel that I chose the vocabulary without due consideration of the precise meaning of the words used.
-Edward