• Edward Z. Yang's avatar
    New story for abstract data types in hsig files. · 518f2895
    Edward Z. Yang authored
    
    
    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: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>
    
    Test Plan: validate
    
    Reviewers: goldfire, simonpj, austin, bgamari
    
    Subscribers: thomie
    
    Differential Revision: https://phabricator.haskell.org/D2594
    518f2895
all.T 1.49 KB