Care about specificity in pattern type args

Close #20443.

6 files changed, 40 insertions, 4 deletions

diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 332ea601b1..3d740948ca 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -1214,9 +1214,11 @@ tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
         { checkTc (con_arity == no_of_args)     -- Check correct arity
                   (arityErr (text "constructor") con_like con_arity no_of_args)
 
-        ; let con_binders = conLikeUserTyVarBinders con_like
-        ; checkTc (type_args `leLength` con_binders)
-                  (conTyArgArityErr con_like (length con_binders) (length type_args))
+              -- forgetting to filter out inferred binders led to #20443
+        ; let con_spec_binders = filter ((== SpecifiedSpec) . binderArgFlag) $
+                                 conLikeUserTyVarBinders con_like
+        ; checkTc (type_args `leLength` con_spec_binders)
+                  (conTyArgArityErr con_like (length con_spec_binders) (length type_args))
 
         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
         ; (type_args', (arg_pats', res))
@@ -1226,7 +1228,7 @@ tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
           -- This unification is straight from Figure 7 of
           -- "Type Variables in Patterns", Haskell'18
         ; _ <- zipWithM (unifyType Nothing) type_args' (substTyVars tenv $
-                                                        binderVars con_binders)
+                                                        binderVars con_spec_binders)
           -- OK to drop coercions here. These unifications are all about
           -- guiding inference based on a user-written type annotation
           -- See Note [Typechecking type applications in patterns]
diff --git a/testsuite/tests/typecheck/should_compile/T20443a.hs b/testsuite/tests/typecheck/should_compile/T20443a.hs
new file mode 100644
index 0000000000..c4b552a3f2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T20443a.hs
@@ -0,0 +1,13 @@
+module T20443a where
+
+import Data.Kind
+
+data Proxy t where
+  Proxy :: forall {k} (t :: k) . Proxy t
+
+a :: () -> Proxy Int
+-- a = Proxy @Type @Int -- This would, rightfully, not compile
+a () = Proxy @Int
+
+b :: Proxy Int -> ()
+b (Proxy @Int) = ()       -- This should compile, but doesn't
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9dc8cd5fba..1a7c9567ce 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -688,6 +688,7 @@ test('T16204b', normal, compile, [''])
 test('T16225', normal, compile, [''])
 test('T13951', normal, compile, [''])
 test('T16312', normal, compile, ['-O'])
+test('T20443a', normal, compile, [''])
 test('T16411', normal, compile, [''])
 test('T16609', normal, compile, [''])
 test('T16827', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T20443b.hs b/testsuite/tests/typecheck/should_fail/T20443b.hs
new file mode 100644
index 0000000000..03b44f343d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20443b.hs
@@ -0,0 +1,13 @@
+module T20443b where
+
+import Data.Kind
+
+data Proxy t where
+  Proxy :: forall {k} (t :: k) . Proxy t
+
+a :: () -> Proxy Int
+-- a = Proxy @Type @Int -- This would, rightfully, not compile
+a () = Proxy @Int
+
+b :: Proxy Int -> ()
+b (Proxy @Type @Int) = ()
diff --git a/testsuite/tests/typecheck/should_fail/T20443b.stderr b/testsuite/tests/typecheck/should_fail/T20443b.stderr
new file mode 100644
index 0000000000..050b945db0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T20443b.stderr
@@ -0,0 +1,6 @@
+
+T20443b.hs:13:4: error:
+    • Too many type arguments in constructor pattern for ‘Proxy’
+      Expected no more than 1; got 2
+    • In the pattern: Proxy @Type @Int
+      In an equation for ‘b’: b (Proxy @Type @Int) = ()
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 7e72cbd1c8..aea4b132cb 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -571,6 +571,7 @@ test('ExplicitSpecificity9', normal, compile_fail, [''])
 test('ExplicitSpecificity10', normal, compile_fail, [''])
 test('T18357', normal, compile_fail, [''])
 test('T18357a', normal, compile_fail, [''])
+test('T20443b', normal, compile_fail, [''])
 test('T18357b', normal, compile_fail, [''])
 test('T17301', normal, compile_fail, [''])
 test('T17567', normal, compile_fail, [''])