Report arity errors correctly despite kinds

Trac #10516 pointed out that when reporting arity errors
(like "T needs 2 arguments but has been given 1"), we should
not count kind arguments, since they are implicit.  If we
include kind args in the count, we get very confusing error
messages indeed.

I did a little bit of refactoring which make some
error messages wobble around.  But the payload of
this fix is in TcValidity.tyConArityErr

compiler/typecheck/TcPat.hs

@@ -989,7 +989,7 @@ tcConArgs :: ConLike -> [TcSigmaType]
 
 tcConArgs con_like arg_tys (PrefixCon arg_pats) penv thing_inside
   = do  { checkTc (con_arity == no_of_args)     -- Check correct arity
-                  (arityErr "Constructor" con_like con_arity no_of_args)
+                  (arityErr "constructor" con_like con_arity no_of_args)
         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
         ; (arg_pats', res) <- tcMultiple tcConArg pats_w_tys
                                               penv thing_inside
@@ -1000,7 +1000,7 @@ tcConArgs con_like arg_tys (PrefixCon arg_pats) penv thing_inside
 
 tcConArgs con_like arg_tys (InfixCon p1 p2) penv thing_inside
   = do  { checkTc (con_arity == 2)      -- Check correct arity
-                  (arityErr "Constructor" con_like con_arity 2)
+                  (arityErr "constructor" con_like con_arity 2)
         ; let [arg_ty1,arg_ty2] = arg_tys       -- This can't fail after the arity check
         ; ([p1',p2'], res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
                                               penv thing_inside

compiler/typecheck/TcTyClsDecls.hs

@@ -2305,14 +2305,7 @@ addTyThingCtxt thing
   where
     name = getName thing
     flav = case thing of
-             ATyCon tc
-                | isClassTyCon tc       -> ptext (sLit "class")
-                | isTypeFamilyTyCon tc  -> ptext (sLit "type family")
-                | isDataFamilyTyCon tc  -> ptext (sLit "data family")
-                | isTypeSynonymTyCon tc -> ptext (sLit "type")
-                | isNewTyCon tc         -> ptext (sLit "newtype")
-                | isDataTyCon tc        -> ptext (sLit "data")
-
+             ATyCon tc -> text (tyConFlavour tc)
              _ -> pprTrace "addTyThingCtxt strange" (ppr thing)
                   Outputable.empty
 

compiler/typecheck/TcValidity.hs

@@ -23,7 +23,7 @@ import TcSimplify ( simplifyAmbiguityCheck )
 import TypeRep
 import TcType
 import TcMType
-import TysWiredIn ( coercibleClass, eqTyConName )
+import TysWiredIn ( coercibleClass, eqTyCon )
 import PrelNames
 import Type
 import Unify( tcMatchTyX )
@@ -439,7 +439,7 @@ check_syn_tc_app :: UserTypeCtxt -> Rank -> KindOrType
 -- which must be saturated,
 -- but not data families, which need not be saturated
 check_syn_tc_app ctxt rank ty tc tys
-  | tc_arity <= n_args   -- Saturated
+  | tc_arity <= length tys   -- Saturated
        -- Check that the synonym has enough args
        -- This applies equally to open and closed synonyms
        -- It's OK to have an *over-applied* type synonym
@@ -462,11 +462,8 @@ check_syn_tc_app ctxt rank ty tc tys
   = mapM_ check_arg tys
 
   | otherwise
-  = failWithTc (arityErr flavour (tyConName tc) tc_arity n_args)
+  = failWithTc (tyConArityErr tc tys)
   where
-    flavour | isTypeFamilyTyCon tc = "Type family"
-            | otherwise            = "Type synonym"
-    n_args = length tys
     tc_arity  = tyConArity tc
     check_arg | isTypeFamilyTyCon tc = check_arg_type  ctxt rank
               | otherwise            = check_mono_type ctxt synArgMonoType
@@ -642,12 +639,10 @@ check_eq_pred :: DynFlags -> PredType -> [TcType] -> TcM ()
 check_eq_pred dflags pred tys
   =         -- Equational constraints are valid in all contexts if type
             -- families are permitted
-    do { checkTc (n_tys == 3)
-                 (arityErr "Equality constraint" eqTyConName 3 n_tys)
+    do { checkTc (length tys == 3)
+                 (tyConArityErr eqTyCon tys)
        ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags)
                  (eqPredTyErr pred) }
-  where
-    n_tys = length tys
 
 check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
 check_tuple_pred under_syn dflags ctxt pred ts
@@ -710,18 +705,15 @@ solved to add+canonicalise another (Foo a) constraint.  -}
 check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
 check_class_pred dflags ctxt pred cls tys
   | isIPClass cls
-  = do { checkTc (arity == n_tys) arity_err
-       ; checkTc (okIPCtxt ctxt)  (badIPPred pred) }
+  = do { check_arity
+       ; checkTc (okIPCtxt ctxt) (badIPPred pred) }
 
   | otherwise
-  = do { checkTc (arity == n_tys) arity_err
+  = do { check_arity
        ; checkTc arg_tys_ok (predTyVarErr pred) }
   where
-    class_name = className cls
-    arity      = classArity cls
-    n_tys      = length tys
-    arity_err  = arityErr "Class" class_name arity n_tys
-
+    check_arity = checkTc (classArity cls == length tys)
+                          (tyConArityErr (classTyCon cls) tys)
     flexible_contexts = xopt Opt_FlexibleContexts     dflags
     undecidable_ok    = xopt Opt_UndecidableInstances dflags
 
@@ -806,9 +798,28 @@ constraintSynErr kind = hang (ptext (sLit "Illegal constraint synonym of kind:")
 dupPredWarn :: [[PredType]] -> SDoc
 dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprType (map head dups)
 
+tyConArityErr :: TyCon -> [TcType] -> SDoc
+-- For type-constructor arity errors, be careful to report
+-- the number of /type/ arguments required and supplied,
+-- ignoring the /kind/ arguments, which the user does not see.
+-- (e.g. Trac #10516)
+tyConArityErr tc tks
+  = arityErr (tyConFlavour tc) (tyConName tc)
+             tc_type_arity tc_type_args
+  where
+    tvs = tyConTyVars tc
+
+    kbs :: [Bool]  -- True for a Type arg, false for a Kind arg
+    kbs = map isTypeVar tvs
+
+    -- tc_type_arity = number of *type* args expected
+    -- tc_type_args  = number of *type* args encountered
+    tc_type_arity = count id kbs
+    tc_type_args  = count (id . fst) (kbs `zip` tks)
+
 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
-arityErr kind name n m
-  = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
+arityErr what name n m
+  = hsep [ ptext (sLit "The") <+> text what, quotes (ppr name), ptext (sLit "should have"),
            n_arguments <> comma, text "but has been given",
            if m==0 then text "none" else int m]
     where

compiler/types/TyCon.hs

@@ -68,6 +68,7 @@ module TyCon(
         tyConArity,
         tyConRoles,
         tyConParent,
+        tyConFlavour,
         tyConTuple_maybe, tyConClass_maybe,
         tyConFamInst_maybe, tyConFamInstSig_maybe, tyConFamilyCoercion_maybe,
         synTyConDefn_maybe, synTyConRhs_maybe, famTyConFlav_maybe,
@@ -1763,6 +1764,24 @@ instance Outputable TyCon where
   -- corresponding TyCon, so we add the quote to distinguish it here
   ppr tc = pprPromotionQuote tc <> ppr (tyConName tc)
 
+tyConFlavour :: TyCon -> String
+tyConFlavour (AlgTyCon { algTcParent = parent, algTcRhs = rhs })
+  | ClassTyCon _ <- parent = "class"
+  | otherwise = case rhs of
+                  TupleTyCon { tup_sort = sort }
+                     | isBoxed (tupleSortBoxity sort) -> "tuple"
+                     | otherwise                      -> "unboxed tuple"
+                  DataTyCon {}       -> "data type"
+                  NewTyCon {}        -> "newtype"
+                  DataFamilyTyCon {} -> "data family"
+                  AbstractTyCon {}   -> "abstract type"
+tyConFlavour (FamilyTyCon {})     = "type family"
+tyConFlavour (SynonymTyCon {})    = "type synonym"
+tyConFlavour (FunTyCon {})        = "built-in type"
+tyConFlavour (PrimTyCon {})       = "built-in type"
+tyConFlavour (PromotedDataCon {}) = "promoted data constructor"
+tyConFlavour (PromotedTyCon {})   = "promoted type constructor"
+
 pprPromotionQuote :: TyCon -> SDoc
 pprPromotionQuote (PromotedDataCon {}) = char '\''   -- Quote promoted DataCons
                                                      -- in types

testsuite/tests/gadt/T3163.stderr

-
-T3163.hs:8:5:
-    Illegal polymorphic or qualified type: forall s. s
-    In the definition of data constructor ‘Unreached’
-    In the data declaration for ‘Taker’
+
+T3163.hs:8:5: error:
+    Illegal polymorphic or qualified type: forall s. s
+    In the definition of data constructor ‘Unreached’
+    In the data type declaration for ‘Taker’

testsuite/tests/gadt/gadt11.stderr

-
-gadt11.hs:12:3:
-    Data constructor ‘L2’ returns type ‘T1 Bool’
-      instead of an instance of its parent type ‘T2 a’
-    In the definition of data constructor ‘L2’
-    In the data declaration for ‘T2’
+
+gadt11.hs:12:3: error:
+    Data constructor ‘L2’ returns type ‘T1 Bool’
+      instead of an instance of its parent type ‘T2 a’
+    In the definition of data constructor ‘L2’
+    In the data type declaration for ‘T2’

testsuite/tests/gadt/gadtSyntaxFail001.stderr

-
-gadtSyntaxFail001.hs:8:5:
-    Data constructor ‘C2’ has existential type variables, a context, or a specialised result type
-      C2 :: forall a. a -> Char -> Foo a Int
-      (Use ExistentialQuantification or GADTs to allow this)
-    In the definition of data constructor ‘C2’
-    In the data declaration for ‘Foo’
+
+gadtSyntaxFail001.hs:8:5: error:
+    Data constructor ‘C2’ has existential type variables, a context, or a specialised result type
+      C2 :: forall a. a -> Char -> Foo a Int
+      (Use ExistentialQuantification or GADTs to allow this)
+    In the definition of data constructor ‘C2’
+    In the data type declaration for ‘Foo’

testsuite/tests/gadt/gadtSyntaxFail002.stderr

-
-gadtSyntaxFail002.hs:8:5:
-    Data constructor ‘C2’ has existential type variables, a context, or a specialised result type
-      C2 :: forall a. a -> Char -> Foo a a
-      (Use ExistentialQuantification or GADTs to allow this)
-    In the definition of data constructor ‘C2’
-    In the data declaration for ‘Foo’
+
+gadtSyntaxFail002.hs:8:5: error:
+    Data constructor ‘C2’ has existential type variables, a context, or a specialised result type
+      C2 :: forall a. a -> Char -> Foo a a
+      (Use ExistentialQuantification or GADTs to allow this)
+    In the definition of data constructor ‘C2’
+    In the data type declaration for ‘Foo’

testsuite/tests/gadt/gadtSyntaxFail003.stderr

-
-gadtSyntaxFail003.hs:7:5:
-    Data constructor ‘C1’ has existential type variables, a context, or a specialised result type
-      C1 :: forall b a c. a -> Int -> c -> Foo b a
-      (Use ExistentialQuantification or GADTs to allow this)
-    In the definition of data constructor ‘C1’
-    In the data declaration for ‘Foo’
+
+gadtSyntaxFail003.hs:7:5: error:
+    Data constructor ‘C1’ has existential type variables, a context, or a specialised result type
+      C1 :: forall b a c. a -> Int -> c -> Foo b a
+      (Use ExistentialQuantification or GADTs to allow this)
+    In the definition of data constructor ‘C1’
+    In the data type declaration for ‘Foo’

testsuite/tests/gadt/records-fail1.stderr

-
-records-fail1.hs:7:1:
-    Constructors T1 and T4 have a common field ‘x’,
-      but have different result types
-    In the data declaration for ‘T’
+
+records-fail1.hs:7:1: error:
+    Constructors T1 and T4 have a common field ‘x’,
+      but have different result types
+    In the data type declaration for ‘T’

testsuite/tests/ghci/scripts/T9293.stderr

-
-<interactive>:5:1:
-    Illegal generalised algebraic data declaration for ‘T’
-      (Use GADTs to allow GADTs)
-    In the data declaration for ‘T’
-
-ghci057.hs:3:3:
-    Data constructor ‘C’ has existential type variables, a context, or a specialised result type
-      C :: T Int
-      (Use ExistentialQuantification or GADTs to allow this)
-    In the definition of data constructor ‘C’
-    In the data declaration for ‘T’
-
-ghci057.hs:3:3:
-    Data constructor ‘C’ has existential type variables, a context, or a specialised result type
-      C :: T Int
-      (Use ExistentialQuantification or GADTs to allow this)
-    In the definition of data constructor ‘C’
-    In the data declaration for ‘T’
+
+<interactive>:5:1: error:
+    Illegal generalised algebraic data declaration for ‘T’
+      (Use GADTs to allow GADTs)
+    In the data declaration for ‘T’
+
+ghci057.hs:3:3: error:
+    Data constructor ‘C’ has existential type variables, a context, or a specialised result type
+      C :: T Int
+      (Use ExistentialQuantification or GADTs to allow this)
+    In the definition of data constructor ‘C’
+    In the data type declaration for ‘T’
+
+ghci057.hs:3:3: error:
+    Data constructor ‘C’ has existential type variables, a context, or a specialised result type
+      C :: T Int
+      (Use ExistentialQuantification or GADTs to allow this)
+    In the definition of data constructor ‘C’
+    In the data type declaration for ‘T’

testsuite/tests/ghci/scripts/ghci057.stderr

-
-<interactive>:5:1:
-    Illegal generalised algebraic data declaration for ‘T’
-      (Use GADTs to allow GADTs)
-    In the data declaration for ‘T’
-
-ghci057.hs:3:3:
-    Data constructor ‘C’ has existential type variables, a context, or a specialised result type
-      C :: T Int
-      (Use ExistentialQuantification or GADTs to allow this)
-    In the definition of data constructor ‘C’
-    In the data declaration for ‘T’
-
-ghci057.hs:3:3:
-    Data constructor ‘C’ has existential type variables, a context, or a specialised result type
-      C :: T Int
-      (Use ExistentialQuantification or GADTs to allow this)
-    In the definition of data constructor ‘C’
-    In the data declaration for ‘T’
+
+<interactive>:5:1: error:
+    Illegal generalised algebraic data declaration for ‘T’
+      (Use GADTs to allow GADTs)
+    In the data declaration for ‘T’
+
+ghci057.hs:3:3: error:
+    Data constructor ‘C’ has existential type variables, a context, or a specialised result type
+      C :: T Int
+      (Use ExistentialQuantification or GADTs to allow this)
+    In the definition of data constructor ‘C’
+    In the data type declaration for ‘T’
+
+ghci057.hs:3:3: error:
+    Data constructor ‘C’ has existential type variables, a context, or a specialised result type
+      C :: T Int
+      (Use ExistentialQuantification or GADTs to allow this)
+    In the definition of data constructor ‘C’
+    In the data type declaration for ‘T’

testsuite/tests/indexed-types/should_fail/BadSock.stderr

-
-BadSock.hs:30:5:
-    Type family ‘Readable’ should have 1 argument, but has been given none
-    In the equations for closed type family ‘Foo’
-    In the type family declaration for ‘Foo’
+
+BadSock.hs:30:5: error:
+    The type family ‘Readable’ should have 1 argument, but has been given none
+    In the equations for closed type family ‘Foo’
+    In the type family declaration for ‘Foo’

testsuite/tests/indexed-types/should_fail/T2157.stderr

-
-T2157.hs:7:15:
-    Type synonym ‘S’ should have 2 arguments, but has been given 1
-    In the type instance declaration for ‘F’
+
+T2157.hs:7:15: error:
+    The type synonym ‘S’ should have 2 arguments, but has been given 1
+    In the type instance declaration for ‘F’

testsuite/tests/indexed-types/should_fail/T9433.stderr

 
-T9433.hs:14:6:
-    Type family ‘Id’ should have 1 argument, but has been given none
+T9433.hs:14:6: error:
+    The type family ‘Id’ should have 1 argument, but has been given none
     In the type signature for ‘x’: x :: Map Id [Bool]

testsuite/tests/module/mod60.stderr

-
-mod60.hs:3:4:
-    Constructor ‘Left’ should have 1 argument, but has been given none
-    In the pattern: Left
-    In an equation for ‘f’: f (Left) = error "foo"
+
+mod60.hs:3:4: error:
+    The constructor ‘Left’ should have 1 argument, but has been given none
+    In the pattern: Left
+    In an equation for ‘f’: f (Left) = error "foo"

testsuite/tests/parser/should_fail/ParserNoBinaryLiterals2.stderr

-
-ParserNoBinaryLiterals2.hs:8:4:
-    Constructor ‘W#’ should have 1 argument, but has been given 2
-    In the pattern: W# 0 b0##
-    In an equation for ‘f’: f (W# 0 b0##) = ()
+
+ParserNoBinaryLiterals2.hs:8:4: error:
+    The constructor ‘W#’ should have 1 argument, but has been given 2
+    In the pattern: W# 0 b0##
+    In an equation for ‘f’: f (W# 0 b0##) = ()

testsuite/tests/parser/should_fail/ParserNoBinaryLiterals3.stderr

-
-ParserNoBinaryLiterals3.hs:8:4:
-    Constructor ‘I#’ should have 1 argument, but has been given 2
-    In the pattern: I# 0 b0#
-    In an equation for ‘f’: f (I# 0 b0#) = ()
+
+ParserNoBinaryLiterals3.hs:8:4: error:
+    The constructor ‘I#’ should have 1 argument, but has been given 2
+    In the pattern: I# 0 b0#
+    In an equation for ‘f’: f (I# 0 b0#) = ()

testsuite/tests/polykinds/T10516.hs

+{-# LANGUAGE PolyKinds #-}
+module T10516 where
+
+type App f a = f a
+
+newtype X f a = X (f a)
+
+f :: f a -> X (App f) a
+f = X

testsuite/tests/polykinds/T10516.stderr

+
+T10516.hs:8:6: error:
+    The type synonym ‘App’ should have 2 arguments, but has been given 1
+    In the type signature for ‘f’: f :: f a -> X (App f) a