Check that a default type signature aligns with the non-default signature

Before, GHC was extremely permissive about the form a default type
signature could take on in a class declaration. Notably, it would accept
garbage like this:

  class Monad m => MonadSupply m where
    fresh :: m Integer
    default fresh :: MonadTrans t => t m Integer
    fresh = lift fresh

And then give an extremely confusing error message when you actually
tried to declare an empty instance of MonadSupply. We now do extra
validity checking of default type signatures to ensure that they align
with their non-default type signature counterparts. That is, a default
type signature is allowed to differ from the non-default one only in its
context - they must otherwise be alpha-equivalent.

Fixes #12918.

Test Plan: ./validate

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: mpickering, dfeuer, thomie

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

GHC Trac Issues: #12918

13 files changed, 406 insertions, 13 deletions

diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index 3069d80128..75b17ef039 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -227,6 +227,10 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 -- and   e :: ty
 -- then  wrap e :: rho
 -- That is, wrap :: ty ~> rho
+--
+-- If you don't need the HsWrapper returned from this function, consider
+-- using tcSplitNestedSigmaTys in TcType, which is a pure alternative that
+-- only computes the returned TcRhoType.
 
 deeplyInstantiate orig ty =
   deeply_instantiate orig
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index d3e308fac0..a66f401603 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2448,16 +2448,17 @@ checkValidClass cls
         ; checkForLevPoly empty tau1
 
         ; unless constrained_class_methods $
-          mapM_ check_constraint (tail (theta1 ++ theta2))
+          mapM_ check_constraint (tail (cls_pred:op_theta))
 
-        ; check_dm ctxt sel_id dm
+        ; check_dm ctxt sel_id cls_pred tau2 dm
         }
         where
           ctxt    = FunSigCtxt op_name True -- Report redundant class constraints
           op_name = idName sel_id
           op_ty   = idType sel_id
-          (_,theta1,tau1) = tcSplitSigmaTy op_ty
-          (_,theta2,_)    = tcSplitSigmaTy tau1
+          (_,cls_pred,tau1) = tcSplitMethodTy op_ty
+          -- See Note [Splitting nested sigma types]
+          (_,op_theta,tau2) = tcSplitNestedSigmaTys tau1
 
           check_constraint :: TcPredType -> TcM ()
           check_constraint pred -- See Note [Class method constraints]
@@ -2482,21 +2483,81 @@ checkValidClass cls
         where
           fam_tvs = tyConTyVars fam_tc
 
-    check_dm :: UserTypeCtxt -> Id -> DefMethInfo -> TcM ()
+    check_dm :: UserTypeCtxt -> Id -> PredType -> Type -> DefMethInfo -> TcM ()
     -- Check validity of the /top-level/ generic-default type
     -- E.g for   class C a where
     --             default op :: forall b. (a~b) => blah
     -- we do not want to do an ambiguity check on a type with
     -- a free TyVar 'a' (Trac #11608).  See TcType
-    -- Note [TyVars and TcTyVars during type checking]
+    -- Note [TyVars and TcTyVars during type checking] in TcType
     -- Hence the mkDefaultMethodType to close the type.
-    check_dm ctxt sel_id (Just (dm_name, dm_spec@(GenericDM {})))
-      = setSrcSpan (getSrcSpan dm_name) $
+    check_dm ctxt sel_id vanilla_cls_pred vanilla_tau
+             (Just (dm_name, dm_spec@(GenericDM dm_ty)))
+      = setSrcSpan (getSrcSpan dm_name) $ do
             -- We have carefully set the SrcSpan on the generic
             -- default-method Name to be that of the generic
             -- default type signature
-        checkValidType ctxt (mkDefaultMethodType cls sel_id dm_spec)
-    check_dm _ _ _ = return ()
+
+          -- First, we check that that the method's default type signature
+          -- aligns with the non-default type signature.
+          -- See Note [Default method type signatures must align]
+          let cls_pred = mkClassPred cls $ mkTyVarTys $ classTyVars cls
+              -- Note that the second field of this tuple contains the context
+              -- of the default type signature, making it apparent that we
+              -- ignore method contexts completely when validity-checking
+              -- default type signatures. See the end of
+              -- Note [Default method type signatures must align]
+              -- to learn why this is OK.
+              --
+              -- See also Note [Splitting nested sigma types]
+              -- for an explanation of why we don't use tcSplitSigmaTy here.
+              (_, _, dm_tau) = tcSplitNestedSigmaTys dm_ty
+
+              -- Given this class definition:
+              --
+              --  class C a b where
+              --    op         :: forall p q. (Ord a, D p q)
+              --               => a -> b -> p -> (a, b)
+              --    default op :: forall r s. E r
+              --               => a -> b -> s -> (a, b)
+              --
+              -- We want to match up two types of the form:
+              --
+              --   Vanilla type sig: C aa bb => aa -> bb -> p -> (aa, bb)
+              --   Default type sig: C a  b  => a  -> b  -> s -> (a,  b)
+              --
+              -- Notice that the two type signatures can be quantified over
+              -- different class type variables! Therefore, it's important that
+              -- we include the class predicate parts to match up a with aa and
+              -- b with bb.
+              vanilla_phi_ty = mkPhiTy [vanilla_cls_pred] vanilla_tau
+              dm_phi_ty      = mkPhiTy [cls_pred] dm_tau
+
+          traceTc "check_dm" $ vcat
+              [ text "vanilla_phi_ty" <+> ppr vanilla_phi_ty
+              , text "dm_phi_ty"      <+> ppr dm_phi_ty ]
+
+          -- Actually checking that the types align is done with a call to
+          -- tcMatchTys. We need to get a match in both directions to rule
+          -- out degenerate cases like these:
+          --
+          --  class Foo a where
+          --    foo1         :: a -> b
+          --    default foo1 :: a -> Int
+          --
+          --    foo2         :: a -> Int
+          --    default foo2 :: a -> b
+          unless (isJust $ tcMatchTys [dm_phi_ty, vanilla_phi_ty]
+                                      [vanilla_phi_ty, dm_phi_ty]) $ addErrTc $
+               hang (text "The default type signature for"
+                     <+> ppr sel_id <> colon)
+                 2 (ppr dm_ty)
+            $$ (text "does not match its corresponding"
+                <+> text "non-default type signature")
+
+          -- Now do an ambiguity check on the default type signature.
+          checkValidType ctxt (mkDefaultMethodType cls sel_id dm_spec)
+    check_dm _ _ _ _ _ = return ()
 
 checkFamFlag :: Name -> TcM ()
 -- Check that we don't use families without -XTypeFamilies
@@ -2538,6 +2599,137 @@ representative example:
 
 This fixes Trac #9415, #9739
 
+Note [Default method type signatures must align]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC enforces the invariant that a class method's default type signature
+must "align" with that of the method's non-default type signature, as per
+GHC Trac #12918. For instance, if you have:
+
+  class Foo a where
+    bar :: forall b. Context => a -> b
+
+Then a default type signature for bar must be alpha equivalent to
+(forall b. a -> b). That is, the types must be the same modulo differences in
+contexts. So the following would be acceptable default type signatures:
+
+    default bar :: forall b. Context1 => a -> b
+    default bar :: forall x. Context2 => a -> x
+
+But the following are NOT acceptable default type signatures:
+
+    default bar :: forall b. b -> a
+    default bar :: forall x. x
+    default bar :: a -> Int
+
+Note that a is bound by the class declaration for Foo itself, so it is
+not allowed to differ in the default type signature.
+
+The default type signature (default bar :: a -> Int) deserves special mention,
+since (a -> Int) is a straightforward instantiation of (forall b. a -> b). To
+write this, you need to declare the default type signature like so:
+
+    default bar :: forall b. (b ~ Int). a -> b
+
+As noted in #12918, there are several reasons to do this:
+
+1. It would make no sense to have a type that was flat-out incompatible with
+   the non-default type signature. For instance, if you had:
+
+     class Foo a where
+       bar :: a -> Int
+       default bar :: a -> Bool
+
+   Then that would always fail in an instance declaration. So this check
+   nips such cases in the bud before they have the chance to produce
+   confusing error messages.
+
+2. Internally, GHC uses TypeApplications to instantiate the default method in
+   an instance. See Note [Default methods in instances] in TcInstDcls.
+   Thus, GHC needs to know exactly what the universally quantified type
+   variables are, and when instantiated that way, the default method's type
+   must match the expected type.
+
+3. Aesthetically, by only allowing the default type signature to differ in its
+   context, we are making it more explicit the ways in which the default type
+   signature is less polymorphic than the non-default type signature.
+
+You might be wondering: why are the contexts allowed to be different, but not
+the rest of the type signature? That's because default implementations often
+rely on assumptions that the more general, non-default type signatures do not.
+For instance, in the Enum class declaration:
+
+    class Enum a where
+      enum :: [a]
+      default enum :: (Generic a, GEnum (Rep a)) => [a]
+      enum = map to genum
+
+    class GEnum f where
+      genum :: [f a]
+
+The default implementation for enum only works for types that are instances of
+Generic, and for which their generic Rep type is an instance of GEnum. But
+clearly enum doesn't _have_ to use this implementation, so naturally, the
+context for enum is allowed to be different to accomodate this. As a result,
+when we validity-check default type signatures, we ignore contexts completely.
+
+Note that when checking whether two type signatures match, we must take care to
+split as many foralls as it takes to retrieve the tau types we which to check.
+See Note [Splitting nested sigma types].
+
+Note [Splitting nested sigma types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this type synonym and class definition:
+
+  type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
+
+  class Each s t a b where
+    each         ::                                      Traversal s t a b
+    default each :: (Traversable g, s ~ g a, t ~ g b) => Traversal s t a b
+
+It might seem obvious that the tau types in both type signatures for `each`
+are the same, but actually getting GHC to conclude this is surprisingly tricky.
+That is because in general, the form of a class method's non-default type
+signature is:
+
+  forall a. C a => forall d. D d => E a b
+
+And the general form of a default type signature is:
+
+  forall f. F f => E a f -- The variable `a` comes from the class
+
+So it you want to get the tau types in each type signature, you might find it
+reasonable to call tcSplitSigmaTy twice on the non-default type signature, and
+call it once on the default type signature. For most classes and methods, this
+will work, but Each is a bit of an exceptional case. The way `each` is written,
+it doesn't quantify any additional type variables besides those of the Each
+class itself, so the non-default type signature for `each` is actually this:
+
+  forall s t a b. Each s t a b => Traversal s t a b
+
+Notice that there _appears_ to only be one forall. But there's actually another
+forall lurking in the Traversal type synonym, so if you call tcSplitSigmaTy
+twice, you'll also go under the forall in Traversal! That is, you'll end up
+with:
+
+  (a -> f b) -> s -> f t
+
+A problem arises because you only call tcSplitSigmaTy once on the default type
+signature for `each`, which gives you
+
+  Traversal s t a b
+
+Or, equivalently:
+
+  forall f. Applicative f => (a -> f b) -> s -> f t
+
+This is _not_ the same thing as (a -> f b) -> s -> f t! So now tcMatchTy will
+say that the tau types for `each` are not equal.
+
+A solution to this problem is to use tcSplitNestedSigmaTys instead of
+tcSplitSigmaTy. tcSplitNestedSigmaTys will always split any foralls that it
+sees until it can't go any further, so if you called it on the default type
+signature for `each`, it would return (a -> f b) -> s -> f t like we desired.
+
 ************************************************************************
 *                                                                      *
                 Checking role validity
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 41a5bddac1..a2d806359d 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -66,7 +66,7 @@ module TcType (
   tcTyConAppTyCon, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
   tcGetTyVar_maybe, tcGetTyVar, nextRole,
-  tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
+  tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
 
   ---------------------------------
   -- Predicates.
@@ -1358,6 +1358,34 @@ tcSplitSigmaTy ty = case tcSplitForAllTys ty of
                         (tvs, rho) -> case tcSplitPhiTy rho of
                                         (theta, tau) -> (tvs, theta, tau)
 
+-- | Split a sigma type into its parts, going underneath as many @ForAllTy@s
+-- as possible. For example, given this type synonym:
+--
+-- @
+-- type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
+-- @
+--
+-- if you called @tcSplitSigmaTy@ on this type:
+--
+-- @
+-- forall s t a b. Each s t a b => Traversal s t a b
+-- @
+--
+-- then it would return @([s,t,a,b], [Each s t a b], Traversal s t a b)@. But
+-- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return
+-- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@.
+tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
+-- NB: This is basically a pure version of deeplyInstantiate (from Inst) that
+-- doesn't compute an HsWrapper.
+tcSplitNestedSigmaTys ty
+    -- If there's a forall, split it apart and try splitting the rho type
+    -- underneath it.
+  | Just (arg_tys, tvs1, theta1, rho1) <- tcDeepSplitSigmaTy_maybe ty
+  = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1
+    in (tvs1 ++ tvs2, theta1 ++ theta2, mkFunTys arg_tys rho2)
+    -- If there's no forall, we're done.
+  | otherwise = ([], [], ty)
+
 -----------------------
 tcDeepSplitSigmaTy_maybe
   :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
diff --git a/docs/users_guide/8.2.1-notes.rst b/docs/users_guide/8.2.1-notes.rst
index 7e75461ac0..e654f20399 100644
--- a/docs/users_guide/8.2.1-notes.rst
+++ b/docs/users_guide/8.2.1-notes.rst
@@ -45,6 +45,12 @@ Compiler
   syntax can be used, in addition to a new form for specifying the cost centre
   name. See :ref:`scc-pragma` for examples.
 
+- GHC is now much more particular about :ghc-flag:`-XDefaultSignatures`. The
+  type signature for a default method of a type class must now be the same as
+  the corresponding main method's type signature modulo differences in the
+  signatures' contexts. Otherwise, the typechecker will reject that class's
+  definition. See :ref:`class-default-signatures` for further details.
+
 - It is now possible to explicitly pick a strategy to use when deriving a
   class instance using the :ghc-flag:`-XDerivingStrategies` language extension
   (see :ref:`deriving-strategies`).
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 2f322d5153..9df6ffb511 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -4892,6 +4892,59 @@ empty instance, however, the default implementation ``map to genum`` is
 filled-in, and type-checked with the type
 ``(Generic a, GEnum (Rep a)) => [a]``.
 
+The type signature for a default method of a type class must take on the same
+form as the corresponding main method's type signature. Otherwise, the
+typechecker will reject that class's definition. By "take on the same form", we
+mean that the default type signature should differ from the main type signature
+only in their contexts. Therefore, if you have a method ``bar``: ::
+
+      class Foo a where
+        bar :: forall b. C => a -> b -> b
+
+Then a default method for ``bar`` must take on the form: ::
+
+      default bar :: forall b. C' => a -> b -> b
+
+``C`` is allowed to be different from ``C'``, but the right-hand sides of the
+type signatures must coincide. We require this because when you declare an
+empty instance for a class that uses :ghc-flag:`-XDefaultSignatures`, GHC
+implicitly fills in the default implementation like this: ::
+
+      instance Foo Int where
+        bar = default_bar @Int
+
+Where ``@Int`` utilizes visible type application
+(:ref:`visible-type-application`) to instantiate the ``b`` in
+``default bar :: forall b. C' => a -> b -> b``. In order for this type
+application to work, the default type signature for ``bar`` must have the same
+type variable order as the non-default signature! But there is no obligation
+for ``C`` and ``C'`` to be the same (see, for instance, the ``Enum`` example
+above, which relies on this).
+
+To further explain this example, the right-hand side of the default
+type signature for ``bar`` must be something that is alpha-equivalent to
+``forall b. a -> b -> b`` (where ``a`` is bound by the class itself, and is
+thus free in the methods' type signatures). So this would also be an acceptable
+default type signature: ::
+
+      default bar :: forall x. C' => a -> x -> x
+
+But not this (since the free variable ``a`` is in the wrong place): ::
+
+      default bar :: forall b. C' => b -> a -> b
+
+Nor this, since we can't match the type variable ``b`` with the concrete type
+``Int``: ::
+
+      default bar :: C' => a -> Int -> Int
+
+That last one deserves a special mention, however, since ``a -> Int -> Int`` is
+a straightforward instantiation of ``forall b. a -> b -> b``. You can still
+write such a default type signature, but you now must use type equalities to
+do so: ::
+
+      default bar :: forall b. (C', b ~ Int) => a -> b -> b
+
 We use default signatures to simplify generic programming in GHC
 (:ref:`generic-programming`).
 
@@ -8090,7 +8143,7 @@ slightly more general than the Haskell 98 version.
 Because the code generator must store and move arguments as well
 as variables, the logic above applies equally well to function arguments,
 which may not be levity-polymorphic.
-  
+
 
 Levity-polymorphic bottoms
 --------------------------
diff --git a/testsuite/tests/generics/T10361b.hs b/testsuite/tests/generics/T10361b.hs
index 6ecd99e644..e655c7c4c0 100644
--- a/testsuite/tests/generics/T10361b.hs
+++ b/testsuite/tests/generics/T10361b.hs
@@ -16,7 +16,9 @@ class Convert a where
     type instance Result a = GResult (Rep a)
 
     convert :: a -> Result a
-    default convert :: (Generic a, GConvert (Rep a)) => a -> GResult (Rep a)
+    default convert
+            :: (Generic a, GConvert (Rep a), Result a ~ GResult (Rep a))
+            => a -> Result a
     convert x = gconvert (from x)
 
 instance Convert Float where
diff --git a/testsuite/tests/typecheck/should_fail/T12151.stderr b/testsuite/tests/typecheck/should_fail/T12151.stderr
index 6433879281..17d484e0ea 100644
--- a/testsuite/tests/typecheck/should_fail/T12151.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12151.stderr
@@ -1,5 +1,11 @@
 
 T12151.hs:9:13: error:
+    • The default type signature for put: forall t. t
+      does not match its corresponding non-default type signature
+    • When checking the class method: put :: forall a. Put a => a
+      In the class declaration for ‘Put’
+
+T12151.hs:9:13: error:
     • Could not deduce (Put a0)
       from the context: Put a
         bound by the type signature for:
diff --git a/testsuite/tests/typecheck/should_fail/T12918a.hs b/testsuite/tests/typecheck/should_fail/T12918a.hs
new file mode 100644
index 0000000000..303cefe9b9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12918a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DefaultSignatures #-}
+module T12918a where
+
+import Control.Monad.Trans.Class
+
+class Monad m => MonadSupply m where
+  fresh :: m Integer
+  default fresh :: MonadTrans t => t m Integer
+  fresh = lift fresh
diff --git a/testsuite/tests/typecheck/should_fail/T12918a.stderr b/testsuite/tests/typecheck/should_fail/T12918a.stderr
new file mode 100644
index 0000000000..3712a33f9a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12918a.stderr
@@ -0,0 +1,8 @@
+
+T12918a.hs:8:11: error:
+    • The default type signature for fresh:
+        forall (t :: (* -> *) -> * -> *). MonadTrans t => t m Integer
+      does not match its corresponding non-default type signature
+    • When checking the class method:
+        fresh :: forall (m :: * -> *). MonadSupply m => m Integer
+      In the class declaration for ‘MonadSupply’
diff --git a/testsuite/tests/typecheck/should_fail/T12918b.hs b/testsuite/tests/typecheck/should_fail/T12918b.hs
new file mode 100644
index 0000000000..837555ad98
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12918b.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+module T12918b where
+
+class Foo1 a where
+  -- These ones should be rejected
+  bar1         :: a -> b
+  default bar1 :: b -> a
+  bar1 = undefined
+
+  bar2         :: a -> b
+  default bar2 :: x
+  bar2 = undefined
+
+  bar3         :: a -> b
+  default bar3 :: a -> Int
+  bar3 = undefined
+
+  bar4         :: a -> Int
+  default bar4 :: a -> b
+  bar4 = undefined
+
+  -- These ones are OK
+  baz1         :: forall b c. a -> b -> c
+  default baz1 :: forall b c. a -> b -> c
+  baz1 = undefined
+
+  baz2         :: forall b c. a -> b -> c
+  default baz2 :: forall c b. a -> b -> c
+  baz2 = undefined
+
+  baz3         :: a -> b -> c
+  default baz3 :: a -> x -> y
+  baz3 = undefined
diff --git a/testsuite/tests/typecheck/should_fail/T12918b.stderr b/testsuite/tests/typecheck/should_fail/T12918b.stderr
new file mode 100644
index 0000000000..cc62c75aac
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12918b.stderr
@@ -0,0 +1,41 @@
+
+T12918b.hs:8:11: error:
+    • The default type signature for bar1: forall b. b -> a
+      does not match its corresponding non-default type signature
+    • When checking the class method:
+        bar1 :: forall a. Foo1 a => forall b. a -> b
+      In the class declaration for ‘Foo1’
+
+T12918b.hs:12:11: error:
+    • The default type signature for bar2: forall x. x
+      does not match its corresponding non-default type signature
+    • When checking the class method:
+        bar2 :: forall a. Foo1 a => forall b. a -> b
+      In the class declaration for ‘Foo1’
+
+T12918b.hs:12:11: error:
+    • Could not deduce (Foo1 a0)
+      from the context: Foo1 a
+        bound by the type signature for:
+                   bar2 :: Foo1 a => x
+        at T12918b.hs:12:11-14
+      The type variable ‘a0’ is ambiguous
+    • In the ambiguity check for ‘bar2’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      When checking the class method:
+        bar2 :: forall a. Foo1 a => forall b. a -> b
+      In the class declaration for ‘Foo1’
+
+T12918b.hs:16:11: error:
+    • The default type signature for bar3: a -> Int
+      does not match its corresponding non-default type signature
+    • When checking the class method:
+        bar3 :: forall a. Foo1 a => forall b. a -> b
+      In the class declaration for ‘Foo1’
+
+T12918b.hs:20:11: error:
+    • The default type signature for bar4: forall b. a -> b
+      does not match its corresponding non-default type signature
+    • When checking the class method:
+        bar4 :: forall a. Foo1 a => a -> Int
+      In the class declaration for ‘Foo1’
diff --git a/testsuite/tests/typecheck/should_fail/T7437.stderr b/testsuite/tests/typecheck/should_fail/T7437.stderr
index 53905f7b6a..d305cee426 100644
--- a/testsuite/tests/typecheck/should_fail/T7437.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7437.stderr
@@ -1,5 +1,13 @@
 
 T7437.hs:14:13: error:
+    • The default type signature for put:
+        forall t. (Generic t, GPut (Rep t)) => t -> [()]
+      does not match its corresponding non-default type signature
+    • When checking the class method:
+        put :: forall a. Put a => a -> [()]
+      In the class declaration for ‘Put’
+
+T7437.hs:14:13: error:
     • Could not deduce (Put a0)
       from the context: (Put a, Generic t, GPut (Rep t))
         bound by the type signature for:
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 493ac77cee..94c215f900 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -418,6 +418,8 @@ test('T12803', normal, compile_fail, [''])
 test('T12042', [], multimod_compile_fail, ['T12042', ''])
 test('T12966', normal, compile_fail, [''])
 test('T12837', normal, compile_fail, [''])
+test('T12918a', normal, compile_fail, [''])
+test('T12918b', normal, compile_fail, [''])
 test('T12921', normal, compile_fail, [''])
 test('T12973', normal, compile_fail, [''])
 test('StrictBinds', normal, compile_fail, [''])