[commit: ghc] master: New story for abstract data types in hsig files. (518f289)

Thu Oct 20 19:45:57 UTC 2016

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/518f28959ec56cf27d6a8096a14a6ce9bc8b9816/ghc

>---------------------------------------------------------------

commit 518f28959ec56cf27d6a8096a14a6ce9bc8b9816
Author: Edward Z. Yang <ezyang at cs.stanford.edu>
Date:   Wed Oct 12 23:55:41 2016 -0700

    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

>---------------------------------------------------------------

518f28959ec56cf27d6a8096a14a6ce9bc8b9816
 compiler/iface/BuildTyCl.hs                        |  5 --
 compiler/iface/IfaceSyn.hs                         |  9 ++-
 compiler/typecheck/TcCanonical.hs                  |  5 ++
 compiler/typecheck/TcRnDriver.hs                   | 46 +++++++++---
 compiler/typecheck/TcRnTypes.hs                    |  2 +-
 compiler/typecheck/TcTyClsDecls.hs                 | 21 ++++--
 compiler/types/TyCon.hs                            | 82 ++++++++++++++++++++--
 testsuite/tests/backpack/should_compile/all.T      |  2 +
 testsuite/tests/backpack/should_compile/bkp37.bkp  | 11 +++
 .../tests/backpack/should_compile/bkp37.stderr     | 10 +++
 testsuite/tests/backpack/should_compile/bkp38.bkp  | 16 +++++
 .../tests/backpack/should_compile/bkp38.stderr     | 10 +++
 testsuite/tests/backpack/should_fail/all.T         |  5 ++
 .../tests/backpack/should_fail/bkpfail10.stderr    |  2 +-
 testsuite/tests/backpack/should_fail/bkpfail23.bkp | 16 +++++
 .../tests/backpack/should_fail/bkpfail23.stderr    | 20 ++++++
 testsuite/tests/backpack/should_fail/bkpfail24.bkp | 19 +++++
 .../tests/backpack/should_fail/bkpfail24.stderr    | 32 +++++++++
 testsuite/tests/backpack/should_fail/bkpfail25.bkp | 24 +++++++
 .../tests/backpack/should_fail/bkpfail25.stderr    | 22 ++++++
 testsuite/tests/backpack/should_fail/bkpfail26.bkp | 18 +++++
 .../tests/backpack/should_fail/bkpfail26.stderr    | 19 +++++
 testsuite/tests/backpack/should_fail/bkpfail27.bkp | 18 +++++
 .../tests/backpack/should_fail/bkpfail27.stderr    | 18 +++++
 24 files changed, 401 insertions(+), 31 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc 518f28959ec56cf27d6a8096a14a6ce9bc8b9816