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

13 Oct 2016

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

 goldfire and I had a chat, and here were the conclusions:

 1. comment:10 is totally nonsense, ignore it.

 2. I'm happy to give up on abstract type synonyms. Maybe someone will find
 them useful for something, but they're not necessary for the Backpack use-
 cases I have in mind.

 3. We agreed that these two examples should fundamentally work the same
 way:

 {{{
 unit p where
   signature H1 where
     data T
   signature H2 where
     data T
   module M where
     import qualified H1
     import qualified H2
     f :: H1.T -> H2.T
     f x = x -- ill typed; the Ts are NOT obviously equal
     g :: (H1.T ~ H2.T) => a -> b
     g x = x -- ill typed (H1.T ~ H2.T should not make this inaccessible)

 unit q where
   signature H1 where
     data T1
   signature H2 where
     data T2
   module M where
     import H1
     import H2
     f :: T1 -> T2
     f x = x -- ill typed
     g :: (T1 ~ T2) => a -> b
     g x = x -- ill typed (T1 ~ T2 should not make this inaccessible)
 }}}

 4. Here's what you do: totally abstract data types (`data T` in an hsig
 file) are generative AND injective. They can only be implemented by `data`
 (except, see below). The only difference is that we do not eagerly fail
 when we come up with an insoluble constraint in the givens involving a
 totally abstract type. As the OutsideIn(X) paper states, it is sound to
 not eagerly fail when simplifying givens, and removing a failure case
 should not impact guess-freeness of the solver. While it is true that when
 the solver encounters a wanted `T1 ~ T2` (where T1/T2 are totally
 abstract) it could kick this constraint out to the use-site, but this is
 silly; we really do want to report a type error here.

 5. Under certain restricted circumstances, we can implement totally
 abstract data with a type synonym. But there are quite a few conditions
 that need to be upheld: it must be generative, injective, and partially
 applicable. A sufficient condition for the type synonym is for it to have
 NO type parameters and for it to have no type family applications.

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