[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 ezyang):

 OK, after a bit of hacking, I have a much better, gloriously simple
 solution:

 1. `data T` in hs-boot is treated as a "nominally distinct abstract type",
 whereas `data T` in hsig is treated as "totally abstract type"; the
 difference being that T may become definitionally equal to another type at
 some later point.

 2. When unifying TyCons in the type inference, when we would hard failure
 because a totally abstract TyCon doesn't unify with something else, we
 *instead* treat the constraint as irreducible and continue on. This
 prevents `f :: (H1.T ~ H2.T) => a -> b` from being treated as
 inaccessible. There may be some other cases I need to handle, but this is
 the big one.

 3. We continue to assume that abstract data is injective; e.g., `(T a ~ T
 b) => a -> b` should hold when T is totally abstract. When accepting a
 type synonym implementation of data, we need to ensure that it is
 injective. This can be done easily by (1) excluding any type synonyms
 which contain type families, and (2) ensuring that all type parameters of
 the type synonym are used (since "phantom" type parameters are not
 injective).

 4. If someone DOESN'T want us to assume that `T` is injective, they should
 declare an open type family instead ala `type family T a` instead of `data
 T a`. I suppose we should permit such a declaration to be *implemented*
 using a type synonym, but this doesn't seem very urgent since you can
 always write `type instance T a = Blah a` instead.

 No more nonsense with open type families. Phabricator incoming.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12680#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler