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

2 files changed, 60 insertions, 1 deletions

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
 --------------------------