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@cs.stanford.edu>

Test Plan: validate

Reviewers: goldfire, simonpj, austin, bgamari

Subscribers: thomie

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

7 files changed, 140 insertions, 30 deletions

diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs
index c26f0c20b3..023c461322 100644
--- a/compiler/iface/BuildTyCl.hs
+++ b/compiler/iface/BuildTyCl.hs
@@ -9,7 +9,6 @@ module BuildTyCl (
         buildDataCon, mkDataConUnivTyVarBinders,
         buildPatSyn,
         TcMethInfo, buildClass,
-        distinctAbstractTyConRhs, totallyAbstractTyConRhs,
         mkNewTyConRhs, mkDataTyConRhs,
         newImplicitBinder, newTyConRepName
     ) where
@@ -39,10 +38,6 @@ import UniqSupply
 import Util
 import Outputable
 
-distinctAbstractTyConRhs, totallyAbstractTyConRhs :: AlgTyConRhs
-distinctAbstractTyConRhs = AbstractTyCon True
-totallyAbstractTyConRhs  = AbstractTyCon False
-
 mkDataTyConRhs :: [DataCon] -> AlgTyConRhs
 mkDataTyConRhs cons
   = DataTyCon {
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs
index 81d905de0b..795e5b1675 100644
--- a/compiler/iface/IfaceSyn.hs
+++ b/compiler/iface/IfaceSyn.hs
@@ -62,7 +62,7 @@ import Fingerprint
 import Binary
 import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
 import Var( TyVarBndr(..) )
-import TyCon ( Role (..), Injectivity(..) )
+import TyCon ( Role (..), Injectivity(..), HowAbstract(..) )
 import StaticFlags (opt_PprStyle_Debug)
 import Util( filterOut, filterByList )
 import DataCon (SrcStrictness(..), SrcUnpackedness(..))
@@ -209,7 +209,7 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars   :: [IfaceTvBndr]
                                      -- See Note [Storing compatibility] in CoAxiom
 
 data IfaceConDecls
-  = IfAbstractTyCon Bool                          -- c.f TyCon.AbstractTyCon
+  = IfAbstractTyCon HowAbstract                   -- c.f TyCon.AbstractTyCon
   | IfDataTyCon [IfaceConDecl] Bool [FieldLabelString] -- Data type decls
   | IfNewTyCon  IfaceConDecl   Bool [FieldLabelString] -- Newtype decls
 
@@ -697,7 +697,10 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
     fls = ifaceConDeclFields condecls
 
     pp_nd = case condecls of
-              IfAbstractTyCon d -> text "abstract" <> ppShowIface ss (parens (ppr d))
+              IfAbstractTyCon how ->
+                case how of
+                  DistinctNominalAbstract           -> text "abstract"
+                  SkolemAbstract                    -> text "skolem"
               IfDataTyCon{}     -> text "data"
               IfNewTyCon{}      -> text "newtype"
 
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 3f121bd898..d955d604fe 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -924,6 +924,11 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
                  ; stopWith ev "Decomposed TyConApp" }
          else canEqFailure ev eq_rel ty1 ty2 }
 
+  -- See Note [Skolem abstract data] (at SkolemAbstract)
+  | isSkolemAbstractTyCon tc1 || isSkolemAbstractTyCon tc2
+  = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
+       ; continueWith (CIrredEvCan { cc_ev = ev }) }
+
   -- Fail straight away for better error messages
   -- See Note [Use canEqFailure in canDecomposableTyConApp]
   | eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 7b0d34d871..b1f2518e7e 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -956,10 +956,41 @@ checkBootTyCon is_boot tc1 tc2
     check (roles1 == roles2) roles_msg `andThenCheck`
     check (eqTypeX env syn_rhs1 syn_rhs2) empty   -- nothing interesting to say
 
-  -- Type synonyms for hs-boot are questionable, so they
-  -- are not supported at the moment
-  | not is_boot && isAbstractTyCon tc1 && isTypeSynonymTyCon tc2
-  = check (roles1 == roles2) roles_msg
+  -- A skolem abstract TyCon can be implemented using a type synonym, but ONLY
+  -- if the type synonym is nullary and has no type family applications.
+  -- This arises from two properties of skolem abstract data:
+  --
+  --    For any T (with some number of paramaters),
+  --
+  --    1. T is a valid type (it is "curryable"), and
+  --
+  --    2. T is valid in an instance head (no type families).
+  --
+  -- See also 'HowAbstract' and Note [Skolem abstract data].
+  --
+  | isSkolemAbstractTyCon tc1
+  , Just (tvs, ty) <- synTyConDefn_maybe tc2
+  , Just (tc2', args) <- tcSplitTyConApp_maybe ty
+  = check (null (tcTyFamInsts ty))
+          (text "Illegal type family application in implementation of abstract data.")
+            `andThenCheck`
+    check (null tvs)
+          (text "Illegal parameterized type synonym in implementation of abstract data." $$
+           text "(Try eta reducing your type synonym so that it is nullary.)")
+            `andThenCheck`
+    -- Don't report roles errors unless the type synonym is nullary
+    checkUnless (not (null tvs)) $
+        ASSERT ( null roles2 )
+        -- If we have something like:
+        --
+        --  signature H where
+        --      data T a
+        --  module H where
+        --      data K a b = ...
+        --      type T = K Int
+        --
+        -- we need to drop the first role of K when comparing!
+        check (roles1 == drop (length args) (tyConRoles tc2')) roles_msg
 
   | Just fam_flav1 <- famTyConFlav_maybe tc1
   , Just fam_flav2 <- famTyConFlav_maybe tc2
@@ -997,11 +1028,8 @@ checkBootTyCon is_boot tc1 tc2
                 (text "Roles on abstract types default to" <+>
                  quotes (text "representational") <+> text "in boot files.")
 
-    eqAlgRhs tc (AbstractTyCon dis1) rhs2
-      | dis1      = check (isGenInjAlgRhs rhs2)   --Check compatibility
-                          (text "The natures of the declarations for" <+>
-                           quotes (ppr tc) <+> text "are different")
-      | otherwise = checkSuccess
+    eqAlgRhs _ (AbstractTyCon _) _rhs2
+      = checkSuccess -- rhs2 is guaranteed to be injective, since it's an AlgTyCon
     eqAlgRhs _  tc1@DataTyCon{} tc2@DataTyCon{} =
         checkListBy eqCon (data_cons tc1) (data_cons tc2) (text "constructors")
     eqAlgRhs _  tc1@NewTyCon{} tc2@NewTyCon{} =
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 6aff15b1e7..f5abe16634 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1427,7 +1427,7 @@ isPartialSig _                                       = False
 ************************************************************************
 -}
 
--- The syntax of xi types:
+-- The syntax of xi (ξ) types:
 -- xi ::= a | T xis | xis -> xis | ... | forall a. tau
 -- Two important notes:
 --      (i) No type families, unless we are under a ForAll
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 6715a8795a..b8db1d4bf6 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -932,7 +932,8 @@ tcDataDefn roles_info
        ; stupid_theta    <- zonkTcTypeToTypes emptyZonkEnv
                                               stupid_tc_theta
        ; kind_signatures <- xoptM LangExt.KindSignatures
-       ; is_boot         <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
+       ; tcg_env         <- getGblEnv
+       ; let hsc_src = tcg_src tcg_env
 
              -- Check that we don't use kind signatures without Glasgow extensions
        ; when (isJust mb_ksig) $
@@ -943,7 +944,7 @@ tcDataDefn roles_info
        ; tycon <- fixM $ \ tycon -> do
              { let res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs))
              ; data_cons <- tcConDecls tycon (final_bndrs, res_ty) cons
-             ; tc_rhs    <- mk_tc_rhs is_boot tycon data_cons
+             ; tc_rhs    <- mk_tc_rhs hsc_src tycon data_cons
              ; tc_rep_nm <- newTyConRepName tc_name
              ; return (mkAlgTyCon tc_name
                                   final_bndrs
@@ -956,10 +957,18 @@ tcDataDefn roles_info
        ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
        ; return tycon }
   where
-    mk_tc_rhs is_boot tycon data_cons
-      | null data_cons, is_boot         -- In a hs-boot file, empty cons means
-      = return totallyAbstractTyConRhs  -- "don't know"; hence totally Abstract
-      | otherwise
+    -- In hs-boot, a 'data' declaration with no constructors
+    -- indicates an nominally distinct abstract data type.
+    mk_tc_rhs HsBootFile _ []
+      = return (AbstractTyCon DistinctNominalAbstract)
+
+    -- In hsig, a 'data' declaration indicates a skolem
+    -- abstract data type. See 'HowAbstract' and Note
+    -- [Skolem abstract data] for more commentary.
+    mk_tc_rhs HsigFile _ []
+      = return (AbstractTyCon SkolemAbstract)
+
+    mk_tc_rhs _ tycon data_cons
       = case new_or_data of
           DataType -> return (mkDataTyConRhs data_cons)
           NewType  -> ASSERT( not (null data_cons) )
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index d0ecb70f26..5778ca8fce 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -10,7 +10,7 @@ The @TyCon@ datatype
 
 module TyCon(
         -- * Main TyCon data types
-        TyCon, AlgTyConRhs(..), visibleDataCons,
+        TyCon, AlgTyConRhs(..), HowAbstract(..), visibleDataCons,
         AlgTyConFlav(..), isNoParent,
         FamTyConFlav(..), Role(..), Injectivity(..),
         RuntimeRepInfo(..),
@@ -55,6 +55,7 @@ module TyCon(
         isDataSumTyCon_maybe,
         isEnumerationTyCon,
         isNewTyCon, isAbstractTyCon,
+        isSkolemAbstractTyCon,
         isFamilyTyCon, isOpenFamilyTyCon,
         isTypeFamilyTyCon, isDataFamilyTyCon,
         isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
@@ -721,7 +722,6 @@ data TyCon
                                        -- tycon's body. See Note [TcTyCon]
       }
 
-
 -- | Represents right-hand-sides of 'TyCon's for algebraic types
 data AlgTyConRhs
 
@@ -729,9 +729,7 @@ data AlgTyConRhs
     -- it's represented by a pointer.  Used when we export a data type
     -- abstractly into an .hi file.
   = AbstractTyCon
-      Bool      -- True  <=> It's definitely a distinct data type,
-                --           equal only to itself; ie not a newtype
-                -- False <=> Not sure
+      HowAbstract
 
     -- | Information about those 'TyCon's derived from a @data@
     -- declaration. This includes data types with no constructors at
@@ -789,6 +787,72 @@ data AlgTyConRhs
                              -- again check Trac #1072.
     }
 
+-- | An 'AbstractTyCon' represents some matchable type constructor (i.e., valid
+-- in instance heads), for which we do not know the implementation.  We refer to
+-- these as "abstract data".
+--
+-- At the moment, there are two flavors of abstract data, corresponding
+-- to whether or not the abstract data declaration occurred in an hs-boot
+-- file or an hsig file.
+--
+data HowAbstract
+  -- | Nominally distinct abstract data arises from abstract data
+  -- declarations in an hs-boot file.
+  --
+  -- Abstract data of this form is guaranteed to be nominally distinct
+  -- from all other declarations in the system; e.g., if I have
+  -- a @data T@ and @data S@ in an hs-boot file, it is safe to
+  -- assume that they will never equal each other.  This is something
+  -- of an implementation accident: it is a lot easier to assume that
+  -- @data T@ in @A.hs-boot@ indicates there will be @data T = ...@
+  -- in @A.hs@, than to permit the possibility that @A.hs@ reexports
+  -- it from somewhere else.
+  = DistinctNominalAbstract
+
+  -- Note [Skolem abstract data]
+  -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  -- Skolem abstract data arises from abstract data declarations
+  -- in an hsig file.
+  --
+  -- The best analogy is to interpret the abstract types in Backpack
+  -- unit as elaborating to universally quantified type variables;
+  -- e.g.,
+  --
+  --    unit p where
+  --        signature H where
+  --            data T
+  --            data S
+  --        module M where
+  --            import H
+  --            f :: (T ~ S) => a -> b
+  --            f x = x
+  --
+  -- elaborates as (with some fake structural types):
+  --
+  --    p :: forall t s. { f :: forall a b. t ~ s => a -> b }
+  --    p = { f = \x -> x } -- ill-typed
+  --
+  -- It is clear that inside p, t ~ s is not provable (and
+  -- if we tried to write a function to cast t to s, that
+  -- would not work), but if we call p @Int @Int, clearly Int ~ Int
+  -- is provable.  The skolem variables are all distinct from
+  -- one another, but we can't make assumptions like "f is
+  -- inaccessible", because the skolem variables will get
+  -- instantiated eventually!
+  --
+  -- Skolem abstract data still has the constraint that there
+  -- are no type family applications, to keep this data matchable.
+  | SkolemAbstract
+
+instance Binary HowAbstract where
+    put_ bh DistinctNominalAbstract          = putByte bh 0
+    put_ bh SkolemAbstract                   = putByte bh 1
+
+    get bh = do { h <- getByte bh
+                ; case h of
+                    0 -> return DistinctNominalAbstract
+                    _ -> return SkolemAbstract }
+
 -- | Some promoted datacons signify extra info relevant to GHC. For example,
 -- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep'
 -- constructor of 'PrimRep'. This data structure allows us to store this
@@ -1543,6 +1607,12 @@ isAbstractTyCon :: TyCon -> Bool
 isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon {} }) = True
 isAbstractTyCon _ = False
 
+-- | Test if the 'TyCon' is totally abstract; i.e., it is not even certain
+-- to be nominally distinct.
+isSkolemAbstractTyCon :: TyCon -> Bool
+isSkolemAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon SkolemAbstract }) = True
+isSkolemAbstractTyCon _ = False
+
 -- | Make an fake, abstract 'TyCon' from an existing one.
 -- Used when recovering from errors
 makeTyConAbstract :: TyCon -> TyCon
@@ -1640,7 +1710,7 @@ isGenInjAlgRhs :: AlgTyConRhs -> Bool
 isGenInjAlgRhs (TupleTyCon {})          = True
 isGenInjAlgRhs (SumTyCon {})            = True
 isGenInjAlgRhs (DataTyCon {})           = True
-isGenInjAlgRhs (AbstractTyCon distinct) = distinct
+isGenInjAlgRhs (AbstractTyCon {})       = False
 isGenInjAlgRhs (NewTyCon {})            = False
 
 -- | Is this 'TyCon' that for a @newtype@