[GHC] #12680: Permit type equality instances in signatures

[GHC]

#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