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

8 files changed, 111 insertions, 1 deletions

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, [''])