#12680: Permit type equality instances in signatures -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: feature request | Status: new Priority: low | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This all makes me a bit worried. First off, I think the best way to think about all of this is in terms of generativity and injectivity. As I read comment:10 and comment:11, I worry that these two concepts are being mixed, but they're really quite separable. (Below and throughout, we talk only of nominal equality.) '''Generativity:''' If `t1` and `t2` are ''generative'', then `t1 a ~ t2 b` implies `t1 ~ t2`. It has been pointed out to me that generativity really describes a set of types, any two of which have the property above. That viewpoint may be enlightening. In particular, it says that generativity is not really an inherent property of a type, but instead exists only by relationship to other types. '''Injectivity:''' If `t` is injective, then `t a ~ t b` implies that `a ~ b`. Now, to respond to specific points in comment:10 and comment:11:
So, that was a really long way of justifying why we can't just search replace `type S` with `type family S` and `type S = Int` with `type family S = Int`.
So what ''can'' we say? You say that we can't use type families because type family LHSs are not definitionally equal (in FC) to their RHSs. (These ''are'' definitionally equal in ''Haskell'', though.) I'm just a little lost as the upshot of the first section of comment:10.
a type synonym with no type families in it
I think what you mean here that you want a type synonym that is generative and injective. Only things that are generative and injective can appear as type patterns (that is, type/data family LHSs and instance heads). I call "generative and injective" ''matchable''. The reason that only matchable types can appear in type patterns is that matching on anything that's not matchable is ill-defined. (Try it.) One stumbling block here is that, of course, type synonyms are not generative -- a ''synonym'' can't be generative, roughly by definition! So what you really mean is that the expansion of the type synonym, after all vanilla synonyms are expanded, is matchable. And that no variables are lost en route. This is, I imagine, what is done to implement `TypeSynonymInstances`. Let's call type synonyms with this property "pre- matchable". Now we can say: `type T a` in a signature declares a pre-matchable type synonym. Any implementing module will need to supply a pre-matchable type synonym definition for these pre-matchable type synonyms. But I agree that this is a new beast, hitherto unknown.
But if H1 and H2 are instantiated in the same way, this equality could hold!
How can this happen? When I see `data`, I think you're declaring a matchable type. And matchable types are generative. Do I take that this equality between `H1` and `H2` can happen when mixing modules (as in "mix- in")? If `H1` and `H2` really ''can'' equal, then they would appear to be pre- matchable. In this case, how does a `data` definition differ from a `type` definition in a signature?
Open type families `type family T a` can be implemented by a type family, type synonym, data type or newtype.
So my signature can have `type family T a` and my module `data T a = MkT`? That feels very fishy. It seems you are using `type family` as a proxy for "type that is not necessarily generative nor injective". Perhaps generativity and injectivity properties should just be specified directly.
When unifying TyCons in the type inference,
This should already happen, if you set the results for `isGenerativeTyCon` and `isInjectiveTyCon` correctly. (And if the canonicalizer is implemented correctly.) You want only a mismatch between generative TyCons do have a hard error, and that should be what's implemented. -------------------- In the past, whenever I've been dwelling on these kinds of issues, I have found that always reducing the problems to generativity and injectivity to be helpful. It might be nice to have a concrete statement of what definitions in signatures mean in terms of these properties. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12680#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler