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

[GHC]

#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 (Type    |                 Version:  7.10.2
  checker)                           |
      Resolution:                    |                Keywords:  backpack
Operating System:  Unknown/Multiple  |            Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by ezyang:

Old description:

> 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.)

New description:

 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 with synonyms (or
 even hs-boot files that don't have the "defined in the implementing
 module" requirement) it's dangerous; we need to notice that the type
 instance is inconsistent when we finally see the implementation.

--

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