[GHC] #10725: Figure out how to support type synonym implementions of abstract data

2 Aug 2015

      #10725: Figure out how to support type synonym implementions of abstract data
-------------------------------------+-------------------------------------
              Reporter:  ezyang      |             Owner:  ezyang
                  Type:  task        |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.10.2
  (Type checker)                     |
              Keywords:  backpack    |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 A classic example we have used when describing Backpack is that you might
 want to abstract over is different types of strings: String, ByteString,
 Text, etc.

 Unfortunately, with every implementation of Backpack we have had so far,
 you can't actually do this!  For example, say you use a type synonym to
 get an existing data type to the "right name"; you get this error:

 {{{
 A.hs-boot:2:6:
     Type constructor `T' has conflicting definitions in the module and its
 hs-boot file
     Main module: type T = String
     Boot file:   abstract(False) T
                      No C type associated
                      RecFlag NonRecursive
                      FamilyInstance: none
 }}}

 How can we make this work? Could it be as simple as just relaxing the
 restriction here? This seems to work OK with shaping, so long as we refer
 to the type synonym (and not the original type in question!) If some type
 checker experts could weight in that would be quite useful.

 ----

 Probably the biggest danger is interaction with machinery that works with
 type families. For example, this is accepted:

 {{{
 -- A.hs-boot
 module A where
 data T

 -- B.hs
 {-# LANGUAGE TypeFamilies #-}
 module B where
 import {-# SOURCE #-} qualified A

 data T = T

 type family F a :: *
 type instance F A.T = Bool
 type instance F T = Int
 }}}

 This doesn't lead to unsoundness today, because A.T must always be defined
 in A.hs (and thus have a unique nominal identity). But it's dangerous for
 this to be accepted today with signatures, since T could refer to B.T.
 (The moral of the story is that after shaping, you have to recheck all
 pairs of families; you can't assume that because they were typechecked
 earlier that they're OK.)

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10725
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler