If your instances are allowed to depend on values that are in scope in your nested context then the choice of those values is effectively part of the name of the data type. Otherwise I can package one of those 'local' data type definitions up, pass it out into another context that brings it back under the `where` clause that defined the local data type with a different value. So, yes, unless you're willing to figure out how to somehow decide the equality of arbitrary values and functions. If you try to say you can't write that sort of scenario by using some sort of magical generative trick that says each invocation of the function that got you down to that data type gives you an entirely 'fresh' type, I suspect you'll run into subtle problems with unification / type checking. I'd love to be wrong, but my expectation is that all of these paths fail.