Reject oversaturated VKAs in type family equations

8 files changed, 108 insertions, 2 deletions

diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index a3b7975b8e..7bf5e20431 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -3806,6 +3806,9 @@ wrongKindOfFamily family
                  | isDataFamilyTyCon family = text "data family"
                  | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
 
+-- | Produce an error for oversaturated type family equations with too many
+-- required arguments.
+-- See Note [Oversaturated type family equations] in TcValidity.
 wrongNumberOfParmsErr :: Arity -> SDoc
 wrongNumberOfParmsErr max_args
   = text "Number of parameters must match family declaration; expected"
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 3b88fe1c89..ca58877bcb 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -2056,7 +2056,17 @@ checkFamPatBinders fam_tc qtvs pats rhs
          --    data instance forall a.  T Int = MkT Int
          -- See Note [Unused explicitly bound variables in a family pattern]
        ; check_tvs bad_qtvs (text "bound by a forall")
-                            (text "used in") }
+                            (text "used in")
+
+         -- Check for oversaturated visible kind arguments in a type family
+         -- equation.
+         -- See Note [Oversaturated type family equations]
+       ; when (isTypeFamilyTyCon fam_tc) $
+           case drop (tyConArity fam_tc) pats of
+             [] -> pure ()
+             spec_arg:_ ->
+               addErr $ text "Illegal oversaturated visible kind argument:"
+                    <+> quotes (char '@' <> pprParendType spec_arg) }
   where
     pat_tvs       = tyCoVarsOfTypes pats
     exact_pat_tvs = exactTyCoVarsOfTypes pats
@@ -2401,6 +2411,62 @@ type application, like @x \@Bool 1@. (Of course it does nothing, but it is
 permissible.) In the type family case, the only sensible explanation is that
 the user has made a mistake -- thus we throw an error.
 
+Note [Oversaturated type family equations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type family tycons have very rigid arities. We want to reject something like
+this:
+
+  type family Foo :: Type -> Type where
+    Foo x = ...
+
+Because Foo has arity zero (i.e., it doesn't bind anything to the left of the
+double colon), we want to disallow any equation for Foo that has more than zero
+arguments, such as `Foo x = ...`. The algorithm here is pretty simple: if an
+equation has more arguments than the arity of the type family, reject.
+
+Things get trickier when visible kind application enters the picture. Consider
+the following example:
+
+  type family Bar (x :: j) :: forall k. Either j k where
+    Bar 5 @Symbol = ...
+
+The arity of Bar is two, since it binds two variables, `j` and `x`. But even
+though Bar's equation has two arguments, it's still invalid. Imagine the same
+equation in Core:
+
+    Bar Nat 5 Symbol = ...
+
+Here, it becomes apparent that Bar is actually taking /three/ arguments! So
+we can't just rely on a simple counting argument to reject
+`Bar 5 @Symbol = ...`, since it only has two user-written arguments.
+Moreover, there's one explicit argument (5) and one visible kind argument
+(@Symbol), which matches up perfectly with the fact that Bar has one required
+binder (x) and one specified binder (j), so that's not a valid way to detect
+oversaturation either.
+
+To solve this problem in a robust way, we do the following:
+
+1. When kind-checking, we count the number of user-written *required*
+   arguments and check if there is an equal number of required tycon binders.
+   If not, reject. (See `wrongNumberOfParmsErr` in TcTyClsDecls.)
+
+   We perform this step during kind-checking, not during validity checking,
+   since we can give better error messages if we catch it early.
+2. When validity checking, take all of the (Core) type patterns from on
+   equation, drop the first n of them (where n is the arity of the type family
+   tycon), and check if there are any types leftover. If so, reject.
+
+   Why does this work? We know that after dropping the first n type patterns,
+   none of the leftover types can be required arguments, since step (1) would
+   have already caught that. Moreover, the only places where visible kind
+   applications should be allowed are in the first n types, since those are the
+   only arguments that can correspond to binding forms. Therefore, the
+   remaining arguments must correspond to oversaturated uses of visible kind
+   applications, which are precisely what we want to reject.
+
+Note that we only perform this check for type families, and not for data
+families. This is because it is perfectly acceptable to oversaturate data
+family instance equations: see Note [Arity of data families] in FamInstEnv.
 
 ************************************************************************
 *                                                                      *
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 5146dbc00e..7a08e21e23 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -629,7 +629,6 @@ test('T14735', normal, compile, [''])
 test('T15180', normal, compile, [''])
 test('T15232', normal, compile, [''])
 test('T15788', normal, compile, [''])
-test('T15793', normal, compile, [''])
 test('T15807a', normal, compile, [''])
 test('T13833', normal, compile, [''])
 test('T14185', expect_broken(14185), compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T15793.hs b/testsuite/tests/typecheck/should_fail/T15793.hs
index 4e96d83f10..4e96d83f10 100644
--- a/testsuite/tests/typecheck/should_compile/T15793.hs
+++ b/testsuite/tests/typecheck/should_fail/T15793.hs
diff --git a/testsuite/tests/typecheck/should_fail/T15793.stderr b/testsuite/tests/typecheck/should_fail/T15793.stderr
new file mode 100644
index 0000000000..d160947e3b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15793.stderr
@@ -0,0 +1,5 @@
+
+T15793.hs:18:3: error:
+    • Illegal oversaturated visible kind argument: ‘@a’
+    • In the equations for closed type family ‘F2’
+      In the type family declaration for ‘F2’
diff --git a/testsuite/tests/typecheck/should_fail/T16255.hs b/testsuite/tests/typecheck/should_fail/T16255.hs
new file mode 100644
index 0000000000..ef2f0a9cb6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16255.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+module T16255 where
+
+import Data.Kind
+import GHC.TypeLits
+
+data SBool :: Bool -> Type
+type family F1 :: forall k. k -> Type where
+  F1 @Bool = SBool
+
+data family D1 :: forall k. k -> Type
+-- Note that this similar-looking data family instance is OK, since data family
+-- instances permit oversaturation in their equations.
+data instance D1 @Bool :: Bool -> Type
+
+type family F2 (x :: j) :: forall k. Either j k where
+  F2 5 @Symbol = Left 4
diff --git a/testsuite/tests/typecheck/should_fail/T16255.stderr b/testsuite/tests/typecheck/should_fail/T16255.stderr
new file mode 100644
index 0000000000..74379a316c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16255.stderr
@@ -0,0 +1,10 @@
+
+T16255.hs:13:3: error:
+    • Illegal oversaturated visible kind argument: ‘@Bool’
+    • In the equations for closed type family ‘F1’
+      In the type family declaration for ‘F1’
+
+T16255.hs:21:3: error:
+    • Illegal oversaturated visible kind argument: ‘@Symbol’
+    • In the equations for closed type family ‘F2’
+      In the type family declaration for ‘F2’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 2b8561909f..a87c846c49 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -492,6 +492,7 @@ test('T15592a', normal, compile_fail, [''])
 test('T15629', normal, compile_fail, [''])
 test('T15767', normal, compile_fail, [''])
 test('T15648', [extra_files(['T15648a.hs'])], multimod_compile_fail, ['T15648', '-v0 -fprint-equality-relations'])
+test('T15793', normal, compile_fail, [''])
 test('T15796', normal, compile_fail, [''])
 test('T15807', normal, compile_fail, [''])
 test('T15954', normal, compile_fail, [''])
@@ -508,3 +509,4 @@ test('T16059d', [extra_files(['T16059b.hs'])], multimod_compile_fail,
     ['T16059d', '-v0'])
 test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail,
     ['T16059e', '-v0'])
+test('T16255', normal, compile_fail, [''])