[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 Edward Z. Yang <ezyang@…>):

 In [changeset:"518f28959ec56cf27d6a8096a14a6ce9bc8b9816/ghc"
 518f2895/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="518f28959ec56cf27d6a8096a14a6ce9bc8b9816"
 New story for abstract data types in hsig files.

 Summary:
 In the old implementation of hsig files, we directly
 reused the implementation of abstract data types from
 hs-boot files.  However, this was WRONG.  Consider the
 following program (an abridged version of bkpfail24):

     {-# LANGUAGE GADTs #-}
     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 => a -> b
             f x = x

 Prior to this patch, M was accepted, because the type
 inference engine concluded that H1.T ~ H2.T does not
 hold (indeed, *presently*, it does not).  However, if
 we subsequently instantiate p with the same module for
 H1 and H2, H1.T ~ H2.T does hold!  Unsound.

 The key is that abstract types from signatures need to
 be treated like *skolem variables*, since you can interpret
 a Backpack unit as a record which is universally quantified
 over all of its abstract types, as such (with some fake
 syntax for structural records):

     p :: forall t1 t2. { f :: t1 ~ t2 => a -> b }
     p = { f = \x -> x } -- ill-typed

 Clearly t1 ~ t2 is not solvable inside p, and also clearly
 it could be true at some point in the future, so we better
 not treat the lambda expression after f as inaccessible.

 The fix seems to be simple: do NOT eagerly fail when trying
 to simplify the given constraints.  Instead, treat H1.T ~ H2.T
 as an irreducible constraint (rather than an insoluble
 one); this causes GHC to treat f as accessible--now we will
 typecheck the rest of the function (and correctly fail).
 Per the OutsideIn(X) paper, it's always sound to fail less
 when simplifying givens.

 We do NOT apply this fix to hs-boot files, where abstract
 data is also guaranteed to be nominally distinct (since
 it can't be implemented via a reexport or a type synonym.)
 This is a somewhat unnatural state of affairs (there's
 no way to really interpret this in Haskell land) but
 no reason to change behavior.

 I deleted "representationally distinct abstract data",
 which is never used anywhere in GHC.

 In the process of constructing this fix, I also realized
 our implementation of type synonym matching against abstract
 data was not sufficiently restrictive.  In order for
 a type synonym T to be well-formed type, it must be a
 nullary synonym (i.e., type T :: * -> *, not type T a = ...).
 Furthermore, since we use abstract data when defining
 instances, they must not have any type family applications.

 More details in #12680.  This probably deserves some sort
 of short paper report.

 Signed-off-by: Edward Z. Yang <ezyang at cs.stanford.edu>

 Test Plan: validate

 Reviewers: goldfire, simonpj, austin, bgamari

 Subscribers: thomie

 Differential Revision: https://phabricator.haskell.org/D2594
 }}}

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