New story for abstract data types in hsig files.
authorEdward Z. Yang <ezyang@cs.stanford.edu>
Thu, 13 Oct 2016 06:55:41 +0000 (23:55 -0700)
committerEdward Z. Yang <ezyang@cs.stanford.edu>
Thu, 20 Oct 2016 19:45:30 +0000 (12:45 -0700)
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

24 files changed:
compiler/iface/BuildTyCl.hs
compiler/iface/IfaceSyn.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/types/TyCon.hs
testsuite/tests/backpack/should_compile/all.T
testsuite/tests/backpack/should_compile/bkp37.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_compile/bkp37.stderr [new file with mode: 0644]
testsuite/tests/backpack/should_compile/bkp38.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_compile/bkp38.stderr [new file with mode: 0644]
testsuite/tests/backpack/should_fail/all.T
testsuite/tests/backpack/should_fail/bkpfail10.stderr
testsuite/tests/backpack/should_fail/bkpfail23.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail23.stderr [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail24.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail24.stderr [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail25.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail25.stderr [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail26.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail26.stderr [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail27.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_fail/bkpfail27.stderr [new file with mode: 0644]

index c26f0c2..023c461 100644 (file)
@@ -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 {
index 81d905d..795e5b1 100644 (file)
@@ -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"
 
index 3f121bd..d955d60 100644 (file)
@@ -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 &&
index 7b0d34d..b1f2518 100644 (file)
@@ -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{} =
index 6aff15b..f5abe16 100644 (file)
@@ -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
index 6715a87..b8db1d4 100644 (file)
@@ -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) )
index d0ecb70..5778ca8 100644 (file)
@@ -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@
index 3ad6538..c9ba076 100644 (file)
@@ -29,3 +29,5 @@ test('bkp34', normal, backpack_compile, [''])
 # instance merging when heads overlap prefers an arbitrary instance
 test('bkp35', expect_broken(0), backpack_compile, [''])
 test('bkp36', normal, backpack_compile, [''])
+test('bkp37', normal, backpack_compile, [''])
+test('bkp38', normal, backpack_compile, [''])
diff --git a/testsuite/tests/backpack/should_compile/bkp37.bkp b/testsuite/tests/backpack/should_compile/bkp37.bkp
new file mode 100644 (file)
index 0000000..7f116dc
--- /dev/null
@@ -0,0 +1,11 @@
+{-# LANGUAGE FlexibleInstances #-}
+unit p where
+    signature A where
+        data K a
+        instance Show (K Int)
+        instance Show (K Bool)
+unit q where
+    module A where
+        type K = []
+unit r where
+    dependency p[A=q:A]
diff --git a/testsuite/tests/backpack/should_compile/bkp37.stderr b/testsuite/tests/backpack/should_compile/bkp37.stderr
new file mode 100644 (file)
index 0000000..90438e8
--- /dev/null
@@ -0,0 +1,10 @@
+[1 of 3] Processing p
+  [1 of 1] Compiling A[sig]           ( p/A.hsig, nothing )
+[2 of 3] Processing q
+  Instantiating q
+  [1 of 1] Compiling A                ( q/A.hs, bkp37.out/q/A.o )
+[3 of 3] Processing r
+  Instantiating r
+  [1 of 1] Including p[A=q:A]
+    Instantiating p[A=q:A]
+    [1 of 1] Compiling A[sig]           ( p/A.hsig, bkp37.out/p/p-HVmFlcYSefiK5n1aDP1v7x/A.o )
diff --git a/testsuite/tests/backpack/should_compile/bkp38.bkp b/testsuite/tests/backpack/should_compile/bkp38.bkp
new file mode 100644 (file)
index 0000000..9523675
--- /dev/null
@@ -0,0 +1,16 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE RoleAnnotations #-}
+unit p where
+    signature A where
+        type role K nominal
+        data K a
+        instance Show (K Int)
+        instance Show (K Bool)
+unit q where
+    module A where
+        type role T representational nominal
+        data T a b = MkT
+            deriving (Show)
+        type K = T ()
+unit r where
+    dependency p[A=q:A]
diff --git a/testsuite/tests/backpack/should_compile/bkp38.stderr b/testsuite/tests/backpack/should_compile/bkp38.stderr
new file mode 100644 (file)
index 0000000..bb9ef66
--- /dev/null
@@ -0,0 +1,10 @@
+[1 of 3] Processing p
+  [1 of 1] Compiling A[sig]           ( p/A.hsig, nothing )
+[2 of 3] Processing q
+  Instantiating q
+  [1 of 1] Compiling A                ( q/A.hs, bkp38.out/q/A.o )
+[3 of 3] Processing r
+  Instantiating r
+  [1 of 1] Including p[A=q:A]
+    Instantiating p[A=q:A]
+    [1 of 1] Compiling A[sig]           ( p/A.hsig, bkp38.out/p/p-HVmFlcYSefiK5n1aDP1v7x/A.o )
index d414cf0..22e87d5 100644 (file)
@@ -19,3 +19,8 @@ test('bkpfail20', normal, backpack_compile_fail, [''])
 test('bkpfail21', normal, backpack_compile_fail, [''])
 # it does fail, but not quite in the right way yet...
 test('bkpfail22', expect_broken(0), backpack_compile_fail, [''])
+test('bkpfail23', normal, backpack_compile_fail, [''])
+test('bkpfail24', normal, backpack_compile_fail, [''])
+test('bkpfail25', normal, backpack_compile_fail, [''])
+test('bkpfail26', normal, backpack_compile_fail, [''])
+test('bkpfail27', normal, backpack_compile_fail, [''])
index 2c2b2f2..248ef63 100644 (file)
@@ -13,7 +13,7 @@ bkpfail10.bkp:8:9: error:
     Type constructor ‘q:H.H’ has conflicting definitions in the module
     and its hsig file
     Main module: data q:H.H a = q:H.H a
-    Hsig file:  abstract q:H.H
+    Hsig file:  skolem q:H.H
     The types have different kinds
 
 bkpfail10.bkp:10:9: error:
diff --git a/testsuite/tests/backpack/should_fail/bkpfail23.bkp b/testsuite/tests/backpack/should_fail/bkpfail23.bkp
new file mode 100644 (file)
index 0000000..a7e52ce
--- /dev/null
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs, RoleAnnotations #-}
+unit p where
+    signature H where
+        type role F phantom
+        data F a
+    module M where
+        import H
+        -- This will typecheck
+        f :: (F a ~ F b) => a -> b
+        f x = x
+unit h where
+    module H where
+        -- But this is an invalid implementation of F
+        type F a = ()
+unit r where
+    dependency p[H=h:H]
diff --git a/testsuite/tests/backpack/should_fail/bkpfail23.stderr b/testsuite/tests/backpack/should_fail/bkpfail23.stderr
new file mode 100644 (file)
index 0000000..ac5fd06
--- /dev/null
@@ -0,0 +1,20 @@
+[1 of 3] Processing p
+  [1 of 2] Compiling H[sig]           ( p/H.hsig, nothing )
+  [2 of 2] Compiling M                ( p/M.hs, nothing )
+[2 of 3] Processing h
+  Instantiating h
+  [1 of 1] Compiling H                ( h/H.hs, bkpfail23.out/h/H.o )
+[3 of 3] Processing r
+  Instantiating r
+  [1 of 1] Including p[H=h:H]
+    Instantiating p[H=h:H]
+    [1 of 2] Compiling H[sig]           ( p/H.hsig, bkpfail23.out/p/p-6KeuBvYi0jvLWqVbkSAZMq/H.o )
+
+bkpfail23.bkp:14:9: error:
+    Type constructor ‘h:H.F’ has conflicting definitions in the module
+    and its hsig file
+    Main module: type h:H.F a = ()
+    Hsig file:  type role h:H.F phantom
+                skolem h:H.F a
+    Illegal parameterized type synonym in implementation of abstract data.
+    (Try eta reducing your type synonym so that it is nullary.)
diff --git a/testsuite/tests/backpack/should_fail/bkpfail24.bkp b/testsuite/tests/backpack/should_fail/bkpfail24.bkp
new file mode 100644 (file)
index 0000000..d560bc7
--- /dev/null
@@ -0,0 +1,19 @@
+{-# LANGUAGE GADTs #-}
+unit p where
+    signature H1 where
+        data T
+    signature H2 where
+        data T
+    module M where
+        import qualified H1
+        import qualified H2
+
+        -- This is NOT an insoluble given, so we
+        -- should complain a doesn't match b
+        f :: H1.T ~ H2.T => a -> b
+        f x = x
+
+        -- This equality does NOT hold, we should
+        -- complain that H1.T doesn't match H2.T
+        g :: H1.T -> H2.T
+        g x = x
diff --git a/testsuite/tests/backpack/should_fail/bkpfail24.stderr b/testsuite/tests/backpack/should_fail/bkpfail24.stderr
new file mode 100644 (file)
index 0000000..53312d2
--- /dev/null
@@ -0,0 +1,32 @@
+[1 of 1] Processing p
+  [1 of 3] Compiling H1[sig]          ( p/H1.hsig, nothing )
+  [2 of 3] Compiling H2[sig]          ( p/H2.hsig, nothing )
+  [3 of 3] Compiling M                ( p/M.hs, nothing )
+
+bkpfail24.bkp:14:15: error:
+    • Could not deduce: a ~ b
+      from the context: {H1.T} ~ {H2.T}
+        bound by the type signature for:
+                   f :: {H1.T} ~ {H2.T} => a -> b
+        at bkpfail24.bkp:13:9-34
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. {H1.T} ~ {H2.T} => a -> b
+        at bkpfail24.bkp:13:9-34
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall a b. {H1.T} ~ {H2.T} => a -> b
+        at bkpfail24.bkp:13:9-34
+    • In the expression: x
+      In an equation for ‘f’: f x = x
+    • Relevant bindings include
+        x :: a (bound at bkpfail24.bkp:14:11)
+        f :: a -> b (bound at bkpfail24.bkp:14:9)
+
+bkpfail24.bkp:19:15: error:
+    • Couldn't match expected type ‘{H2.T}’
+                  with actual type ‘{H1.T}’
+      NB: ‘{H1.T}’ is defined at bkpfail24.bkp:4:9-14
+          ‘{H2.T}’ is defined at bkpfail24.bkp:6:9-14
+    • In the expression: x
+      In an equation for ‘g’: g x = x
diff --git a/testsuite/tests/backpack/should_fail/bkpfail25.bkp b/testsuite/tests/backpack/should_fail/bkpfail25.bkp
new file mode 100644 (file)
index 0000000..322a70a
--- /dev/null
@@ -0,0 +1,24 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+unit p where
+    signature H where
+        data T a
+    module M where
+        import H
+        instance Functor T
+
+unit q where
+    module H where
+        -- No good!
+        type T a = a
+
+unit r where
+    dependency p[H=q:H]
+
+{-
+If we get:
+
+     The type synonym ‘T’ should have 1 argument, but has been given none 
+     In the instance declaration for ‘Functor T’
+
+that is too late! Need to catch this earlier.
+-}
diff --git a/testsuite/tests/backpack/should_fail/bkpfail25.stderr b/testsuite/tests/backpack/should_fail/bkpfail25.stderr
new file mode 100644 (file)
index 0000000..1440948
--- /dev/null
@@ -0,0 +1,22 @@
+[1 of 3] Processing p
+  [1 of 2] Compiling H[sig]           ( p/H.hsig, nothing )
+  [2 of 2] Compiling M                ( p/M.hs, nothing )
+
+bkpfail25.bkp:7:18: warning: [-Wmissing-methods (in -Wdefault)]
+    • No explicit implementation for
+        ‘fmap’
+    • In the instance declaration for ‘Functor T’
+[2 of 3] Processing q
+  Instantiating q
+  [1 of 1] Compiling H                ( q/H.hs, bkpfail25.out/q/H.o )
+[3 of 3] Processing r
+  Instantiating r
+  [1 of 1] Including p[H=q:H]
+    Instantiating p[H=q:H]
+    [1 of 2] Compiling H[sig]           ( p/H.hsig, bkpfail25.out/p/p-D5Mg3foBSCrDbQDKH4WGSG/H.o )
+
+bkpfail25.bkp:12:9: error:
+    Type constructor ‘q:H.T’ has conflicting definitions in the module
+    and its hsig file
+    Main module: type q:H.T a = a
+    Hsig file:  skolem q:H.T a
diff --git a/testsuite/tests/backpack/should_fail/bkpfail26.bkp b/testsuite/tests/backpack/should_fail/bkpfail26.bkp
new file mode 100644 (file)
index 0000000..5ea5b6b
--- /dev/null
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeSynonymInstances #-}
+unit p where
+    signature H where
+        data T a
+    module M where
+        import H
+        instance Functor T where
+            fmap = undefined
+
+unit q where
+    module H where
+        -- The type synonym is not eta reduced, so we reject it.
+        -- This test will start passing if GHC automatically eta
+        -- reduces type synonyms when it can, see #12701
+        type T a = [a]
+
+unit r where
+    dependency p[H=q:H]
diff --git a/testsuite/tests/backpack/should_fail/bkpfail26.stderr b/testsuite/tests/backpack/should_fail/bkpfail26.stderr
new file mode 100644 (file)
index 0000000..4c49bd1
--- /dev/null
@@ -0,0 +1,19 @@
+[1 of 3] Processing p
+  [1 of 2] Compiling H[sig]           ( p/H.hsig, nothing )
+  [2 of 2] Compiling M                ( p/M.hs, nothing )
+[2 of 3] Processing q
+  Instantiating q
+  [1 of 1] Compiling H                ( q/H.hs, bkpfail26.out/q/H.o )
+[3 of 3] Processing r
+  Instantiating r
+  [1 of 1] Including p[H=q:H]
+    Instantiating p[H=q:H]
+    [1 of 2] Compiling H[sig]           ( p/H.hsig, bkpfail26.out/p/p-D5Mg3foBSCrDbQDKH4WGSG/H.o )
+
+bkpfail26.bkp:15:9: error:
+    Type constructor ‘q:H.T’ has conflicting definitions in the module
+    and its hsig file
+    Main module: type q:H.T a = [a]
+    Hsig file:  skolem q:H.T a
+    Illegal parameterized type synonym in implementation of abstract data.
+    (Try eta reducing your type synonym so that it is nullary.)
diff --git a/testsuite/tests/backpack/should_fail/bkpfail27.bkp b/testsuite/tests/backpack/should_fail/bkpfail27.bkp
new file mode 100644 (file)
index 0000000..fc992e8
--- /dev/null
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies #-}
+unit p where
+    signature H where
+        data T
+    module M where
+        import H
+        instance Show T where
+            show = undefined
+
+unit q where
+    module H where
+        -- Illegal type family!
+        type family F
+        type instance F = Bool
+        type T = F
+
+unit r where
+    dependency p[H=q:H]
diff --git a/testsuite/tests/backpack/should_fail/bkpfail27.stderr b/testsuite/tests/backpack/should_fail/bkpfail27.stderr
new file mode 100644 (file)
index 0000000..b24587a
--- /dev/null
@@ -0,0 +1,18 @@
+[1 of 3] Processing p
+  [1 of 2] Compiling H[sig]           ( p/H.hsig, nothing )
+  [2 of 2] Compiling M                ( p/M.hs, nothing )
+[2 of 3] Processing q
+  Instantiating q
+  [1 of 1] Compiling H                ( q/H.hs, bkpfail27.out/q/H.o )
+[3 of 3] Processing r
+  Instantiating r
+  [1 of 1] Including p[H=q:H]
+    Instantiating p[H=q:H]
+    [1 of 2] Compiling H[sig]           ( p/H.hsig, bkpfail27.out/p/p-D5Mg3foBSCrDbQDKH4WGSG/H.o )
+
+bkpfail27.bkp:15:9: error:
+    Type constructor ‘q:H.T’ has conflicting definitions in the module
+    and its hsig file
+    Main module: type q:H.T = q:H.F
+    Hsig file:  skolem q:H.T
+    Illegal type family application in implementation of abstract data.