Fix #14045 by omitting an unnecessary check
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Sat, 29 Jul 2017 01:43:38 +0000 (21:43 -0400)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Sat, 29 Jul 2017 15:31:56 +0000 (11:31 -0400)
Previously, we checked the number of patterns in a data instances
for all data families whose kind did not end in a kind variable.
But, of course, undersaturating instances can happen even without
the kind ending in a kind variable. So I've omitted the arity check.
Data families aren't as particular about their arity as type families
are (because data families can be undersaturated). Still, this change
degrades error messages when instances don't have the right arity;
now, instead of reporting a simple mismatch in the number of patterns,
GHC reports kind errors. The new errors are fully accurate, but perhaps
not as easy to work with. Still, with the new flexibility of allowing
data family instances with varying numbers of patterns, I don't see
a better way.

This commit also improves source fidelity in some error messages,
requiring more changes than really are necessary. But without these
changes, error messages around mismatched associated instance heads
were poor.

test cases: indexed-types/should_compile/T14045,
            indexed-types/should_fail/T14045a

14 files changed:
compiler/hsSyn/HsDecls.hs
compiler/typecheck/TcGenDeriv.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcValidity.hs
testsuite/tests/indexed-types/should_compile/T14045.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr
testsuite/tests/indexed-types/should_fail/T14045a.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T14045a.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/all.T

index 8b7d9c6..2163300 100644 (file)
@@ -37,7 +37,7 @@ module HsDecls (
   -- ** Instance declarations
   InstDecl(..), LInstDecl, NewOrData(..), FamilyInfo(..),
   TyFamInstDecl(..), LTyFamInstDecl, instDeclDataFamInsts,
-  DataFamInstDecl(..), LDataFamInstDecl, pprDataFamInstFlavour,
+  DataFamInstDecl(..), LDataFamInstDecl, pprDataFamInstFlavour, pprFamInstLHS,
   TyFamEqn(..), TyFamInstEqn, LTyFamInstEqn, TyFamDefltEqn, LTyFamDefltEqn,
   HsTyPats,
   LClsInstDecl, ClsInstDecl(..),
@@ -1408,7 +1408,6 @@ data DataFamInstDecl pass
     -- For details on above see note [Api annotations] in ApiAnnotation
 deriving instance (DataId pass) => Data (DataFamInstDecl pass)
 
-
 ----------------- Class instances -------------
 
 -- | Located Class Instance Declaration
@@ -1473,7 +1472,7 @@ ppr_fam_inst_eqn (L _ (TyFamEqn { tfe_tycon = tycon
                                 , tfe_pats  = pats
                                 , tfe_fixity = fixity
                                 , tfe_rhs   = rhs }))
-    = pp_fam_inst_lhs tycon pats fixity [] <+> equals <+> ppr rhs
+    = pprFamInstLHS tycon pats fixity [] Nothing <+> equals <+> ppr rhs
 
 ppr_fam_deflt_eqn :: (SourceTextX pass, OutputableBndrId pass)
                   => LTyFamDefltEqn pass -> SDoc
@@ -1497,21 +1496,22 @@ pprDataFamInstDecl top_lvl (DataFamInstDecl { dfid_tycon = tycon
   = pp_data_defn pp_hdr defn
   where
     pp_hdr ctxt = ppr_instance_keyword top_lvl
-              <+> pp_fam_inst_lhs tycon pats fixity ctxt
+              <+> pprFamInstLHS tycon pats fixity ctxt (dd_kindSig defn)
 
 pprDataFamInstFlavour :: DataFamInstDecl pass -> SDoc
 pprDataFamInstFlavour (DataFamInstDecl { dfid_defn = (HsDataDefn { dd_ND = nd }) })
   = ppr nd
 
-pp_fam_inst_lhs :: (SourceTextX pass, OutputableBndrId pass)
+pprFamInstLHS :: (SourceTextX pass, OutputableBndrId pass)
    => Located (IdP pass)
    -> HsTyPats pass
    -> LexicalFixity
    -> HsContext pass
+   -> Maybe (LHsKind pass)
    -> SDoc
-pp_fam_inst_lhs thing (HsIB { hsib_body = typats }) fixity context
+pprFamInstLHS thing (HsIB { hsib_body = typats }) fixity context mb_kind_sig
                                               -- explicit type patterns
-   = hsep [ pprHsContext context, pp_pats typats]
+   = hsep [ pprHsContext context, pp_pats typats, pp_kind_sig ]
    where
      pp_pats (patl:patsr)
        | fixity == Infix
@@ -1519,7 +1519,13 @@ pp_fam_inst_lhs thing (HsIB { hsib_body = typats }) fixity context
           , hsep (map (pprHsType.unLoc) patsr)]
        | otherwise = hsep [ pprPrefixOcc (unLoc thing)
                    , hsep (map (pprHsType.unLoc) (patl:patsr))]
-     pp_pats [] = empty
+     pp_pats [] = pprPrefixOcc (unLoc thing)
+
+     pp_kind_sig
+       | Just k <- mb_kind_sig
+       = dcolon <+> ppr k
+       | otherwise
+       = empty
 
 instance (SourceTextX pass, OutputableBndrId pass)
        => Outputable (ClsInstDecl pass) where
index 7e79c12..00ed9ed 100644 (file)
@@ -1679,7 +1679,7 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
                                     fam_tc rep_lhs_tys rep_rhs_ty
         -- Check (c) from Note [GND and associated type families] in TcDeriv
         checkValidTyFamEqn (Just (cls, cls_tvs, lhs_env)) fam_tc rep_tvs'
-                           rep_cvs' rep_lhs_tys rep_rhs_ty loc
+                           rep_cvs' rep_lhs_tys rep_rhs_ty pp_lhs loc
         newFamInst SynFamilyInst axiom
       where
         cls_tvs     = classTyVars cls
@@ -1696,6 +1696,7 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
         (rep_tvs, rep_cvs) = partition isTyVar rep_tcvs
         rep_tvs'    = toposortTyVars rep_tvs
         rep_cvs'    = toposortTyVars rep_cvs
+        pp_lhs      = ppr (mkTyConApp fam_tc rep_lhs_tys)
 
 nlHsAppType :: LHsExpr GhcPs -> Type -> LHsExpr GhcPs
 nlHsAppType e s = noLoc (e `HsAppType` hs_ty)
index e9f3432..7367c20 100644 (file)
@@ -882,11 +882,10 @@ checkExpectedKind :: HsType GhcRn
                   -> TcKind
                   -> TcKind
                   -> TcM TcType
-checkExpectedKind hs_ty ty act exp = fstOf3 <$> checkExpectedKindX Nothing hs_ty ty act exp
+checkExpectedKind hs_ty ty act exp = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
 
-checkExpectedKindX :: Outputable hs_ty
-                   => Maybe (VarEnv Kind)  -- Possibly, instantiations for kind vars
-                   -> hs_ty                -- HsType whose kind we're checking
+checkExpectedKindX :: Maybe (VarEnv Kind)  -- Possibly, instantiations for kind vars
+                   -> SDoc                 -- HsType whose kind we're checking
                    -> TcType               -- the type whose kind we're checking
                    -> TcKind               -- the known kind of that type, k
                    -> TcKind               -- the expected kind, exp_kind
@@ -896,11 +895,11 @@ checkExpectedKindX :: Outputable hs_ty
 --      (checkExpectedKind ty act_kind exp_kind)
 -- checks that the actual kind act_kind is compatible
 --      with the expected kind exp_kind
-checkExpectedKindX mb_kind_env hs_ty ty act_kind exp_kind
+checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
  = do { (ty', new_args, act_kind') <- instantiate ty act_kind exp_kind
       ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                   , uo_expected = exp_kind
-                                  , uo_thing    = Just (ppr hs_ty)
+                                  , uo_thing    = Just pp_hs_ty
                                   , uo_visible  = True } -- the hs_ty is visible
       ; co_k <- uType KindLevel origin act_kind' exp_kind
       ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
index 703089d..dc8eb0c 100644 (file)
@@ -626,9 +626,10 @@ tcDataFamInstDecl mb_clsinfo
     (L loc decl@(DataFamInstDecl
        { dfid_pats = pats
        , dfid_tycon = fam_tc_name
-       , dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
-                                     , dd_ctxt = ctxt, dd_cons = cons
-                                     , dd_derivs = derivs } }))
+       , dfid_fixity = fixity
+       , dfid_defn = HsDataDefn { dd_ND = new_or_data, dd_cType = cType
+                                , dd_ctxt = ctxt, dd_cons = cons
+                                , dd_kindSig = m_ksig, dd_derivs = derivs } }))
   = setSrcSpan loc             $
     tcAddDataFamInstCtxt decl  $
     do { fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_tc_name
@@ -640,7 +641,7 @@ tcDataFamInstDecl mb_clsinfo
          -- Kind check type patterns
        ; let mb_kind_env = thdOf3 <$> mb_clsinfo
        ; tcFamTyPats (famTyConShape fam_tc) mb_clsinfo pats
-                     (kcDataDefn mb_kind_env (unLoc fam_tc_name) pats defn) $
+                     (kcDataDefn mb_kind_env decl) $
              \tvs pats res_kind ->
     do { stupid_theta <- solveEqualities $ tcHsContext ctxt
 
@@ -708,7 +709,7 @@ tcDataFamInstDecl mb_clsinfo
          -- Remember to check validity; no recursion to worry about here
          -- Check that left-hand sides are ok (mono-types, no type families,
          -- consistent instantiations, etc)
-       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats' extra_pats
+       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats' extra_pats pp_hs_pats
 
          -- Result kind must be '*' (otherwise, we have too few patterns)
        ; checkTc (isLiftedTypeKind final_res_kind) $
@@ -741,6 +742,7 @@ tcDataFamInstDecl mb_clsinfo
       = go pats (tv : etad_tvs)
     go pats etad_tvs = (reverse pats, etad_tvs)
 
+    pp_hs_pats = pprFamInstLHS fam_tc_name pats fixity (unLoc ctxt) m_ksig
 
 {- *********************************************************************
 *                                                                      *
index 77c5c23..17da32f 100644 (file)
@@ -1088,8 +1088,8 @@ tcDefaultAssocDecl _ (d1:_:_)
   = failWithTc (text "More than one default declaration for"
                 <+> ppr (tfe_tycon (unLoc d1)))
 
-tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
-                                           , tfe_pats = hs_tvs
+tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = lname@(L _ tc_name)
+                                           , tfe_pats = hs_tvs, tfe_fixity = fixity
                                            , tfe_rhs = rhs })]
   | HsQTvs { hsq_implicit = imp_vars, hsq_explicit = exp_vars } <- hs_tvs
   = -- See Note [Type-checking default assoc decls]
@@ -1111,6 +1111,7 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
        ; let pats = HsIB { hsib_vars = imp_vars ++ map hsLTyVarName exp_vars
                          , hsib_body = map hsLTyVarBndrToType exp_vars
                          , hsib_closed = False } -- this field is ignored, anyway
+             pp_lhs = pprFamInstLHS lname pats fixity [] Nothing
 
           -- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
           -- the LHsQTyVars used for declaring a tycon, but the names here
@@ -1122,7 +1123,7 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
           -- enclosing class. So it's treated more as a freestanding beast.
        ; (pats', rhs_ty)
            <- tcFamTyPats shape Nothing pats
-              (kcTyFamEqnRhs Nothing (mkFamApp fam_tc_name pats) rhs) $
+              (kcTyFamEqnRhs Nothing pp_lhs rhs) $
               \tvs pats rhs_kind ->
               do { rhs_ty <- solveEqualities $
                              tcCheckLHsType rhs rhs_kind
@@ -1165,26 +1166,29 @@ proper tcMatchTys here.)  -}
 -------------------------
 kcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn GhcRn -> TcM ()
 kcTyFamInstEqn fam_tc_shape@(FamTyConShape { fs_name = fam_tc_name })
-    (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
-                     , tfe_pats  = pats
-                     , tfe_rhs   = hs_ty }))
+    (L loc (TyFamEqn { tfe_tycon  = lname@(L _ eqn_tc_name)
+                     , tfe_pats   = pats
+                     , tfe_fixity = fixity
+                     , tfe_rhs    = hs_ty }))
   = setSrcSpan loc $
     do { checkTc (fam_tc_name == eqn_tc_name)
                  (wrongTyFamName fam_tc_name eqn_tc_name)
        ; discardResult $
          tc_fam_ty_pats fam_tc_shape Nothing -- not an associated type
-                        pats (kcTyFamEqnRhs Nothing (mkFamApp fam_tc_name pats) hs_ty) }
+                        pats (kcTyFamEqnRhs Nothing pp_lhs hs_ty) }
+  where
+    pp_lhs = pprFamInstLHS lname pats fixity [] Nothing
 
 -- Infer the kind of the type on the RHS of a type family eqn. Then use
 -- this kind to check the kind of the LHS of the equation. This is useful
 -- as the callback to tc_fam_ty_pats and the kind-checker to
 -- tcFamTyPats.
 kcTyFamEqnRhs :: Maybe ClsInstInfo
-              -> HsType GhcRn         -- ^ Eqn LHS (for errors only)
+              -> SDoc                 -- ^ Eqn LHS (for errors only)
               -> LHsType GhcRn        -- ^ Eqn RHS
               -> TcKind               -- ^ Inferred kind of left-hand side
               -> TcM ([TcType], TcKind)  -- ^ New pats, inst'ed kind of left-hand side
-kcTyFamEqnRhs mb_clsinfo lhs_ty rhs_hs_ty lhs_ki
+kcTyFamEqnRhs mb_clsinfo pp_lhs_ty rhs_hs_ty lhs_ki
   = do { -- It's still possible the lhs_ki has some foralls. Instantiate these away.
          (_lhs_ty', new_pats, insted_lhs_ki)
            <- instantiateTyUntilN mb_kind_env 0 bogus_ty lhs_ki
@@ -1194,26 +1198,21 @@ kcTyFamEqnRhs mb_clsinfo lhs_ty rhs_hs_ty lhs_ki
   where
     mb_kind_env = thdOf3 <$> mb_clsinfo
 
-    bogus_ty = pprPanic "kcTyFamEqnRhs" (ppr lhs_ty $$ ppr rhs_hs_ty)
-
-  -- useful when we need an HsType GhcRn for error messages
-  -- not exported from this module
-mkFamApp :: Name -> HsTyPats GhcRn -> HsType GhcRn
-mkFamApp fam_tc_name (HsIB { hsib_body = pats })
-  = unLoc $ mkHsAppTys (noLoc $ HsTyVar NotPromoted (noLoc fam_tc_name)) pats
+    bogus_ty = pprPanic "kcTyFamEqnRhs" (pp_lhs_ty $$ ppr rhs_hs_ty)
 
 tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
                -> TcM CoAxBranch
 -- Needs to be here, not in TcInstDcls, because closed families
 -- (typechecked here) have TyFamInstEqns
 tcTyFamInstEqn fam_tc_shape@(FamTyConShape { fs_name = fam_tc_name }) mb_clsinfo
-    (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
-                     , tfe_pats  = pats
-                     , tfe_rhs   = hs_ty }))
+    (L loc (TyFamEqn { tfe_tycon  = lname@(L _ eqn_tc_name)
+                     , tfe_pats   = pats
+                     , tfe_fixity = fixity
+                     , tfe_rhs    = hs_ty }))
   = ASSERT( fam_tc_name == eqn_tc_name )
     setSrcSpan loc $
     tcFamTyPats fam_tc_shape mb_clsinfo pats
-                (kcTyFamEqnRhs mb_clsinfo (mkFamApp fam_tc_name pats) hs_ty) $
+                (kcTyFamEqnRhs mb_clsinfo pp_lhs hs_ty) $
                     \tvs pats res_kind ->
     do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
 
@@ -1225,12 +1224,12 @@ tcTyFamInstEqn fam_tc_shape@(FamTyConShape { fs_name = fam_tc_name }) mb_clsinfo
        ; return (mkCoAxBranch tvs' [] pats' rhs_ty'
                               (map (const Nominal) tvs')
                               loc) }
+  where
+    pp_lhs = pprFamInstLHS lname pats fixity [] Nothing
 
 kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
                                   -- (associated types only)
-           -> Name                -- ^ the family name, for error msgs only
-           -> HsTyPats GhcRn      -- ^ the patterns, for error msgs only
-           -> HsDataDefn GhcRn    -- ^ the RHS
+           -> DataFamInstDecl GhcRn
            -> TcKind              -- ^ the kind of the tycon applied to pats
            -> TcM ([TcType], TcKind)
              -- ^ the kind signature might force instantiation
@@ -1238,8 +1237,13 @@ kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
              -- See Note [Instantiating a family tycon]
 -- Used for 'data instance' only
 -- Ordinary 'data' is handled by kcTyClDec
-kcDataDefn mb_kind_env fam_name pats
-           (HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
+kcDataDefn mb_kind_env
+           (DataFamInstDecl
+             { dfid_tycon  = fam_name
+             , dfid_pats   = pats
+             , dfid_fixity = fixity
+             , dfid_defn   = HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind } })
+           res_k
   = do  { _ <- tcHsContext ctxt
         ; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
           -- See Note [Failing early in kcDataDefn]
@@ -1266,7 +1270,7 @@ kcDataDefn mb_kind_env fam_name pats
         ; (ev_binds, (_, new_args, co))
             <- solveEqualities $
                checkConstraints skol_info tvs' [] $
-               checkExpectedKindX mb_kind_env hs_fam_app
+               checkExpectedKindX mb_kind_env pp_fam_app
                                   bogus_ty res_k inner_res_kind'
 
         ; let Pair lhs_ki rhs_ki = tcCoercionKind co
@@ -1281,7 +1285,7 @@ kcDataDefn mb_kind_env fam_name pats
         ; return (new_args, lhs_ki) }
   where
     bogus_ty   = pprPanic "kcDataDefn" (ppr fam_name <+> ppr pats)
-    hs_fam_app = mkFamApp fam_name pats
+    pp_fam_app = pprFamInstLHS fam_name pats fixity (unLoc ctxt) mb_kind
 
 {-
 Kind check type patterns and kind annotate the embedded type variables.
@@ -1346,10 +1350,10 @@ two bad things could happen:
 
 -----------------
 data TypeOrDataFamily = TypeFam | DataFam
-data FamTyConShape = FamTyConShape { fs_name :: Name
-                                   , fs_arity :: Arity
-                                   , fs_flavor :: TypeOrDataFamily
-                                   , fs_binders :: [TyConBinder]
+data FamTyConShape = FamTyConShape { fs_name     :: Name
+                                   , fs_arity    :: Arity -- the visible args
+                                   , fs_flavor   :: TypeOrDataFamily
+                                   , fs_binders  :: [TyConBinder]
                                    , fs_res_kind :: Kind }
   -- See Note [Type-checking type patterns]
 
@@ -1392,13 +1396,12 @@ tc_fam_ty_pats (FamTyConShape { fs_name = name, fs_arity = arity
          -- understand.
          let should_check_arity
                | TypeFam <- flav = True
-                  -- check for data families that don't have any polymorphism
-                  -- why not always? See [Arity of data families] in FamInstEnv
-               | otherwise       = isEmptyVarSet (tyCoVarsOfType res_kind)
+                  -- why not check data families? See [Arity of data families] in FamInstEnv
+               | otherwise       = False
 
        ; when should_check_arity $
          checkTc (arg_pats `lengthIs` arity) $
-         wrongNumberOfParmsErr (arity - count isInvisibleTyConBinder binders)
+         wrongNumberOfParmsErr arity
                       -- report only explicit arguments
 
          -- Kind-check and quantify
@@ -2655,9 +2658,10 @@ checkValidClass cls
              -- Check that any default declarations for associated types are valid
            ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
              checkValidTyFamEqn mb_cls fam_tc
-                                fam_tvs [] (mkTyVarTys fam_tvs) rhs loc }
+                                fam_tvs [] (mkTyVarTys fam_tvs) rhs pp_lhs loc }
         where
           fam_tvs = tyConTyVars fam_tc
+          pp_lhs  = ppr (mkTyConApp fam_tc (mkTyVarTys fam_tvs))
 
     check_dm :: UserTypeCtxt -> Id -> PredType -> Type -> DefMethInfo -> TcM ()
     -- Check validity of the /top-level/ generic-default type
index d896f41..4c2b7b6 100644 (file)
@@ -1539,13 +1539,13 @@ type AssocInstArgShape = (Maybe Type, Type)
 checkConsistentFamInst
                :: Maybe ClsInstInfo
                -> TyCon              -- ^ Family tycon
-               -> [TyVar]            -- ^ Type variables of the family instance
                -> [Type]             -- ^ Type patterns from instance
+               -> SDoc               -- ^ pretty-printed user-written instance head
                -> TcM ()
 -- See Note [Checking consistent instantiation]
 
 checkConsistentFamInst Nothing _ _ _ = return ()
-checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc _at_tvs at_tys
+checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pats
   = do { -- Check that the associated type indeed comes from this class
          checkTc (Just clas == tyConAssoc_maybe fam_tc)
                  (badATErr (className clas) (tyConName fam_tc))
@@ -1578,7 +1578,7 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc _at_tvs at_tys
 
     pp_exp_act
       = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
-             , text "  Actual:" <+> ppr (mkTyConApp fam_tc at_tys)
+             , text "  Actual:" <+> pp_hs_pats
              , sdocWithDynFlags $ \dflags ->
                ppWhen (has_poly_args dflags) $
                vcat [ text "where the `<tv>' arguments are type variables,"
@@ -1668,7 +1668,9 @@ checkValidCoAxBranch mb_clsinfo fam_tc
                     (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
                                 , cab_lhs = typats
                                 , cab_rhs = rhs, cab_loc = loc })
-  = checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
+  = checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
+  where
+    pp_lhs = ppr (mkTyConApp fam_tc typats)
 
 -- | Do validity checks on a type family equation, including consistency
 -- with any enclosing class instance head, termination, and lack of
@@ -1679,11 +1681,12 @@ checkValidTyFamEqn :: Maybe ClsInstInfo
                    -> [CoVar] -- ^ bound covars in the equation
                    -> [Type]  -- ^ type patterns
                    -> Type    -- ^ rhs
+                   -> SDoc    -- ^ user-written LHS
                    -> SrcSpan
                    -> TcM ()
-checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
+checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
   = setSrcSpan loc $
-    do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats []
+    do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats [] pp_lhs
 
          -- The argument patterns, and RHS, are all boxed tau types
          -- E.g  Reject type family F (a :: k1) :: k2
@@ -1724,6 +1727,7 @@ checkFamInstRhs lhsTys famInsts
 checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
                   -> [Type]   -- ^ patterns the user wrote
                   -> [Type]   -- ^ "extra" patterns from a data instance kind sig
+                  -> SDoc     -- ^ pretty-printed user-written instance head
                   -> TcM ()
 -- Patterns in a 'type instance' or 'data instance' decl should
 -- a) contain no type family applications
@@ -1733,7 +1737,7 @@ checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
 --         type T a = Int
 --         type instance F (T a) = a
 -- c) For associated types, are consistently instantiated
-checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats
+checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats pp_hs_pats
   = do { mapM_ checkValidTypePat user_ty_pats
 
        ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes user_ty_pats)
@@ -1741,7 +1745,7 @@ checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats
        ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs user_ty_pats)
 
          -- Check that type patterns match the class instance head
-       ; checkConsistentFamInst mb_clsinfo fam_tc tvs (user_ty_pats `chkAppend` extra_ty_pats) }
+       ; checkConsistentFamInst mb_clsinfo fam_tc (user_ty_pats `chkAppend` extra_ty_pats) pp_hs_pats }
 
 checkValidTypePat :: Type -> TcM ()
 -- Used for type patterns in class instances,
diff --git a/testsuite/tests/indexed-types/should_compile/T14045.hs b/testsuite/tests/indexed-types/should_compile/T14045.hs
new file mode 100644 (file)
index 0000000..951388b
--- /dev/null
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, GADTs #-}
+
+module T14045 where
+
+import Data.Kind
+
+data family Sing (a :: k)
+data instance Sing :: Bool -> Type where
+  SFalse :: Sing False
+  STrue  :: Sing True
index 84e2398..359e7d5 100644 (file)
@@ -266,3 +266,4 @@ test('T13398b', normal, compile, [''])
 test('T13662', normal, compile, [''])
 test('T13705', normal, compile, [''])
 test('T12369', normal, compile, [''])
+test('T14045', normal, compile, [''])
index b0c91af..8637eaa 100644 (file)
@@ -1,4 +1,5 @@
 
 SimpleFail1a.hs:4:1: error:
-    • Number of parameters must match family declaration; expected 2
+    • Expecting one more argument to ‘T1 Int’
+      Expected a type, but ‘T1 Int’ has kind ‘* -> *’
     • In the data instance declaration for ‘T1’
index 43c72cf..32303ec 100644 (file)
@@ -1,4 +1,4 @@
 
 SimpleFail1b.hs:4:1: error:
-    • Number of parameters must match family declaration; expected 2
+    • Expected kind ‘* -> *’, but ‘T1 Int Bool’ has kind ‘*’
     • In the data instance declaration for ‘T1’
index a9262eb..9bd571e 100644 (file)
@@ -2,6 +2,6 @@
 SimpleFail2a.hs:11:3: error:
     • Type indexes must match class instance head
       Expected: Sd Int
-      Actual:   Sd a
+        Actual: Sd a :: *
     • In the data instance declaration for ‘Sd’
       In the instance declaration for ‘C Int’
diff --git a/testsuite/tests/indexed-types/should_fail/T14045a.hs b/testsuite/tests/indexed-types/should_fail/T14045a.hs
new file mode 100644 (file)
index 0000000..fc545a8
--- /dev/null
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, GADTs, FlexibleInstances #-}
+
+module T14045a where
+
+import Data.Kind
+
+class C (a :: k) where
+  data S (a :: k)
+
+instance C (z :: Bool) where
+  data S :: Bool -> Type where
+    SF :: S False
+    ST :: S True
diff --git a/testsuite/tests/indexed-types/should_fail/T14045a.stderr b/testsuite/tests/indexed-types/should_fail/T14045a.stderr
new file mode 100644 (file)
index 0000000..0306bd2
--- /dev/null
@@ -0,0 +1,7 @@
+
+T14045a.hs:11:3: error:
+    • Type indexes must match class instance head
+      Expected: S z
+        Actual: S :: Bool -> Type
+    • In the data instance declaration for ‘S’
+      In the instance declaration for ‘C (z :: Bool)’
index c1d308f..c3a2f16 100644 (file)
@@ -137,3 +137,4 @@ test('T13674', normal, compile_fail, [''])
 test('T13784', normal, compile_fail, [''])
 test('T13877', normal, compile_fail, [''])
 test('T14033', normal, compile_fail, [''])
+test('T14045a', normal, compile_fail, [''])