1. 17 Nov, 2016 1 commit
    • Edward Z. Yang's avatar
      Test for type synonym loops on TyCon. · 31398fbc
      Edward Z. Yang authored
      Previously, we tested for type synonym loops by doing
      a syntactic test on the literal type synonym declarations.
      However, in some cases, loops could go through hs-boot
      files, leading to an infinite loop (#12042); a similar
      situation can occur when signature merging.
      This commit replaces the syntactic test with a test on
      TyCon, simply by walking down all type synonyms until
      we bottom out, or find we've looped back.  It's a lot
      Signed-off-by: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>
      Test Plan: validate
      Reviewers: simonpj, austin, bgamari
      Subscribers: goldfire, thomie
      Differential Revision: https://phabricator.haskell.org/D2656
      GHC Trac Issues: #12042
  2. 20 Oct, 2016 2 commits
    • Edward Z. Yang's avatar
    • Edward Z. Yang's avatar
      New story for abstract data types in hsig files. · 518f2895
      Edward Z. Yang authored
      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
  3. 08 Oct, 2016 1 commit