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

 > If T and S are datatypes, then how could they be equal?

 ``data S`` can be implemented with ``type S = T``, thus making them equal.
 Admittedly the use of ``data X`` to represent an abstract data type is
 awful, arguably we should get the syntax ``type X`` working which is a bit
 clearer.

 > And your `F Int ~ S` seems like it could just be an instance of the type
 family.

 Yes, I think you're right. The important thing is that if you write a type
 family instance in a signature, it does not indicate that there is
 *exactly* this reduction rule in the type family, just that it is
 derivable (though, what about injective type families? Ick.) David was
 specifically interested in playing around with alternative axiomatizations
 of type families by specifying equalities manually.

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