[GHC] #13361: Better type synonym merging/subtyping for Backpack

[GHC]

#13361: Better type synonym merging/subtyping for Backpack
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  low            |         Milestone:
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  backpack       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Here are two signatures which don't merge today in Backpack:

 {{{
 signature A where
     data T
     data U = Mk T
 signature A where
     data S
     data U = Mk S
 }}}

 On the one hand, this is not too surprising, because you never said that T
 and S were the same, so why should I decide that the declarations of U are
 compatible?  OK, but suppose I were to add the missing type synonym: which
 direction should I put it? What you will find is that, under Backpack's
 current subtyping rules, *neither* orientation is a subtype of the other:

 {{{
 signature A where
     data T
     type S = T
     data U = Mk T
 signature A where
     type T = S
     data S
     data U = Mk S
 }}}

 The first signature is a supertype of a module that says `data T =
 MkCommon`, but NOT of a module that says `data S = MkCommon`, since type
 synonym declarations and data declarations are not compatible.

 This doesn't smell very good. Indeed, ML's semantic signatures do not have
 this problem, because when I write these signatures, I actually get a
 semantic signature of the form `exists c. { type T = c, type S = c, ...
 }`; i.e., neither declaration is privileged.

 On the other hand, our behavior is inline with MixML, which does not have
 these as mutual subtypes. So it's not clear the complexity of changing our
 internal language justifies the marginal benefit that is to be gotten
 here. Not planning on fixing this unless someone shouts.

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