diff options
24 files changed, 446 insertions, 320 deletions
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs index ea7d036601..af60b7cd6c 100644 --- a/compiler/rename/RnSource.hs +++ b/compiler/rename/RnSource.hs @@ -709,7 +709,10 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds -- to remove the context). rnFamInstDecl :: HsDocContext - -> Maybe (Name, [Name]) + -> Maybe (Name, [Name]) -- Nothing => not associated + -- Just (cls,tvs) => associated, + -- and gives class and tyvars of the + -- parent instance delc -> Located RdrName -> HsTyPats RdrName -> rhs @@ -743,10 +746,17 @@ rnFamInstDecl doc mb_cls tycon (HsIB { hsib_body = pats }) payload rnPayload freeKiTyVarsAllVars pat_kity_vars_with_dups ; tv_nms_dups <- mapM (lookupOccRn . unLoc) $ [ tv | (tv:_:_) <- groups ] - -- Add to the used variables any variables that - -- appear *more than once* on the LHS - -- e.g. F a Int a = Bool - ; let tv_nms_used = extendNameSetList rhs_fvs tv_nms_dups + -- Add to the used variables + -- a) any variables that appear *more than once* on the LHS + -- e.g. F a Int a = Bool + -- b) for associated instances, the variables + -- of the instance decl. See + -- Note [Unused type variables in family instances] + ; let tv_nms_used = extendNameSetList rhs_fvs $ + inst_tvs ++ tv_nms_dups + inst_tvs = case mb_cls of + Nothing -> [] + Just (_, inst_tvs) -> inst_tvs ; warnUnusedTypePatterns var_names tv_nms_used -- See Note [Renaming associated types] @@ -757,8 +767,8 @@ rnFamInstDecl doc mb_cls tycon (HsIB { hsib_body = pats }) payload rnPayload is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs && not (cls_tkv `elemNameSet` var_name_set) - ; unless (null bad_tvs) (badAssocRhs bad_tvs) + ; return ((pats', payload'), rhs_fvs `plusFV` pat_fvs) } ; let anon_wcs = concatMap collectAnonWildCards pats' @@ -872,15 +882,25 @@ fresh meta-variables whereas the former generate fresh skolems. Note [Unused type variables in family instances] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When the flag -fwarn-unused-type-patterns is on, the compiler reports warnings -about unused type variables. (rnFamInstDecl) A type variable is considered -used - * when it is either occurs on the RHS of the family instance, or +When the flag -fwarn-unused-type-patterns is on, the compiler reports +warnings about unused type variables in type-family instances. A +tpye variable is considered used (i.e. cannot be turned into a wildcard) +when + + * it occurs on the RHS of the family instance e.g. type instance F a b = a -- a is used on the RHS * it occurs multiple times in the patterns on the LHS e.g. type instance F a a = Int -- a appears more than once on LHS + * it is one of the instance-decl variables, for associated types + e.g. instance C (a,b) where + type T (a,b) = a + Here the type pattern in the type instance must be the same as that + for the class instance, so + type T (a,_) = a + would be rejected. So we should not complain about an unused variable b + As usual, the warnings are not reported for for type variables with names beginning with an underscore. diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index d88686f0ce..4d20a4a306 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -19,7 +19,7 @@ import DynFlags import TcRnMonad import FamInst import TcErrors( reportAllUnsolved ) -import TcValidity( validDerivPred ) +import TcValidity( validDerivPred, allDistinctTyVars ) import TcClassDcl( tcATDefault, tcMkDeclCtxt ) import TcEnv import TcGenDeriv -- Deriv stuff @@ -639,11 +639,6 @@ deriveTyData tvs tc tc_args deriv_pred (tc_args_to_keep, args_to_drop) = splitAt n_args_to_keep tc_args inst_ty_kind = typeKind (mkTyConApp tc tc_args_to_keep) - -- Use exactTyCoVarsOfTypes, not tyCoVarsOfTypes, so that we - -- don't mistakenly grab a type variable mentioned in a type - -- synonym that drops it. - -- See Note [Eta-reducing type synonyms]. - dropped_tvs = exactTyCoVarsOfTypes args_to_drop -- Match up the kinds, and apply the resulting kind substitution -- to the types. See Note [Unify kinds in deriving] @@ -672,8 +667,7 @@ deriveTyData tvs tc tc_args deriv_pred ; traceTc "derivTyData2" (vcat [ ppr tkvs ]) - ; checkTc (allDistinctTyVars args_to_drop && -- (a) and (b) - not (any (`elemVarSet` dropped_tvs) tkvs)) -- (c) + ; checkTc (allDistinctTyVars (mkVarSet tkvs) args_to_drop) -- (a, b, c) (derivingEtaErr cls final_cls_tys (mkTyConApp tc final_tc_args)) -- Check that -- (a) The args to drop are all type variables; eg reject: @@ -822,6 +816,12 @@ where this was first noticed). For this reason, we call exactTyCoVarsOfTypes on the eta-reduced types so that we only consider the type variables that remain after expanding through type synonyms. + + -- Use exactTyCoVarsOfTypes, not tyCoVarsOfTypes, so that we + -- don't mistakenly grab a type variable mentioned in a type + -- synonym that drops it. + -- See Note [Eta-reducing type synonyms]. + dropped_tvs = exactTyCoVarsOfTypes args_to_drop -} mkEqnHelp :: Maybe OverlapMode diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index 1e34fc683c..bd26e6e620 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -531,7 +531,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds ; (tyvars, theta, clas, inst_tys) <- tcHsClsInstType InstDeclCtxt poly_ty ; let mini_env = mkVarEnv (classTyVars clas `zip` inst_tys) mini_subst = mkTvSubst (mkInScopeSet (mkVarSet tyvars)) mini_env - mb_info = Just (clas, mini_env) + mb_info = Just (clas, tyvars, mini_env) -- Next, process any associated types. ; traceTc "tcLocalInstDecl" (ppr poly_ty) @@ -582,7 +582,7 @@ lot of kinding and type checking code with ordinary algebraic data types (and GADTs). -} -tcFamInstDeclCombined :: Maybe ClsInfo +tcFamInstDeclCombined :: Maybe ClsInstInfo -> Located Name -> TcM TyCon tcFamInstDeclCombined mb_clsinfo fam_tc_lname = do { -- Type family instances require -XTypeFamilies @@ -602,7 +602,7 @@ tcFamInstDeclCombined mb_clsinfo fam_tc_lname ; return fam_tc } -tcTyFamInstDecl :: Maybe ClsInfo +tcTyFamInstDecl :: Maybe ClsInstInfo -> LTyFamInstDecl Name -> TcM FamInst -- "type instance" tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn })) @@ -627,7 +627,7 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn })) ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch ; newFamInst SynFamilyInst axiom } -tcDataFamInstDecl :: Maybe ClsInfo +tcDataFamInstDecl :: Maybe ClsInstInfo -> LDataFamInstDecl Name -> TcM (FamInst, Maybe DerivInfo) -- "newtype instance" and "data instance" tcDataFamInstDecl mb_clsinfo diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 13259664fe..4d664f4c95 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -1081,7 +1081,7 @@ kcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) tc_fam_ty_pats fam_tc_shape Nothing -- not an associated type pats (discardResult . (tcCheckLHsType hs_ty)) } -tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInfo -> LTyFamInstEqn Name -> TcM CoAxBranch +tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInstInfo -> LTyFamInstEqn Name -> TcM CoAxBranch -- Needs to be here, not in TcInstDcls, because closed families -- (typechecked here) have TyFamInstEqns tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) mb_clsinfo @@ -1171,7 +1171,7 @@ famTyConShape fam_tc , tyConResKind fam_tc ) tc_fam_ty_pats :: FamTyConShape - -> Maybe ClsInfo + -> Maybe ClsInstInfo -> HsTyPats Name -- Patterns -> (TcKind -> TcM ()) -- Kind checker for RHS -- result is ignored @@ -1194,7 +1194,7 @@ tc_fam_ty_pats (name, _, binders, res_kind) mb_clsinfo -- See Note [Quantifying over family patterns] (_, (insted_res_kind, typats)) <- tcImplicitTKBndrs tv_names $ do { (insting_subst, _leftover_binders, args, leftovers, n) - <- tcInferArgs name binders (snd <$> mb_clsinfo) arg_pats + <- tcInferArgs name binders (thdOf3 <$> mb_clsinfo) arg_pats ; case leftovers of hs_ty:_ -> addErrTc $ too_many_args hs_ty n _ -> return () @@ -1214,7 +1214,7 @@ tc_fam_ty_pats (name, _, binders, res_kind) mb_clsinfo -- See Note [tc_fam_ty_pats vs tcFamTyPats] tcFamTyPats :: FamTyConShape - -> Maybe ClsInfo + -> Maybe ClsInstInfo -> HsTyPats Name -- patterns -> (TcKind -> TcM ()) -- kind-checker for RHS -> ( [TyVar] -- Kind and type variables @@ -2352,6 +2352,8 @@ checkValidClass cls cls_arity = length $ filterOutInvisibleTyVars (classTyCon cls) tyvars -- Ignore invisible variables cls_tv_set = mkVarSet tyvars + mini_env = zipVarEnv tyvars (mkTyVarTys tyvars) + mb_cls = Just (cls, tyvars, mini_env) check_op constrained_class_methods (sel_id, dm) = setSrcSpan (getSrcSpan sel_id) $ @@ -2394,11 +2396,10 @@ checkValidClass cls -- Check that any default declarations for associated types are valid ; whenIsJust m_dflt_rhs $ \ (rhs, loc) -> - checkValidTyFamEqn (Just (cls, mini_env)) fam_tc + checkValidTyFamEqn mb_cls fam_tc fam_tvs [] (mkTyVarTys fam_tvs) rhs loc } where fam_tvs = tyConTyVars fam_tc - mini_env = zipVarEnv tyvars (mkTyVarTys tyvars) check_dm :: UserTypeCtxt -> DefMethInfo -> TcM () -- Check validity of the /top-level/ generic-default type diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 1d5799cd5d..e710c6e61a 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -11,14 +11,17 @@ module TcValidity ( checkValidTheta, checkValidFamPats, checkValidInstance, validDerivPred, checkInstTermination, - ClsInfo, checkValidCoAxiom, checkValidCoAxBranch, + ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch, checkValidTyFamEqn, arityErr, badATErr, - checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds + checkValidTelescope, checkZonkValidTelescope, checkValidInferredKinds, + allDistinctTyVars ) where #include "HsVersions.h" +import Maybes + -- friends: import TcUnify ( tcSubType_NC ) import TcSimplify ( simplifyAmbiguityCheck ) @@ -28,7 +31,6 @@ import TcMType import PrelNames import Type import Coercion -import Unify( tcMatchTyX ) import Kind import CoAxiom import Class @@ -45,6 +47,7 @@ import FamInst ( makeInjectivityErrors ) import Name import VarEnv import VarSet +import Var ( mkTyVar ) import ErrUtils import DynFlags import Util @@ -53,10 +56,10 @@ import SrcLoc import Outputable import BasicTypes import Module +import Unique ( mkAlphaTyVarUnique ) import qualified GHC.LanguageExtensions as LangExt import Control.Monad -import Data.Maybe import Data.List ( (\\) ) {- @@ -1316,14 +1319,58 @@ for (T ty Int) elsewhere, because it's an *associated* type. Note [Checking consistent instantiation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See Trac #11450 for background discussion on this check. + class C a b where type T a x b +With this class decl, if we have an instance decl + instance C ty1 ty2 where ... +then the type instance must look like + type T ty1 v ty2 = ... +with exactly 'ty1' for 'a', 'ty2' for 'b', and a variable for 'x'. +For example: + instance C [p] Int - type T [p] y Int = (p,y,y) -- Induces the family instance TyCon - -- type TR p y = (p,y,y) + type T [p] y Int = (p,y,y) + +Note that -So we +* We used to allow completely different bound variables in the + associated type instance; e.g. + instance C [p] Int + type T [q] y Int = ... + But from GHC 8.2 onwards, we don't. It's much simpler this way. + See Trac #11450. + +* When the class variable isn't used on the RHS of the type instance, + it's tempting to allow wildcards, thus + instance C [p] Int + type T [_] y Int = (y,y) + But it's awkward to do the test, and it doesn't work if the + variable is repeated: + instance C (p,p) Int + type T (_,_) y Int = (y,y) + Even though 'p' is not used on the RHS, we still need to use 'p' + on the LHS to establish the repeated pattern. So to keep it simple + we just require equality. + +* We also check that any non-class-tyvars are instantiated with + distinct tyvars. That rules out + instance C [p] Int where + type T [p] Bool Int = p -- Note Bool + type T [p] Char Int = p -- Note Char + + and + instance C [p] Int where + type T [p] p Int = p -- Note repeated 'p' on LHS + It's consistent to do this because we don't allow this kind of + instantiation for the class-tyvar arguments of the family. + + Overall, we can have exactly one type instance for each + associated type. If you wantmore, use an auxiliary family. + +Implementation * Form the mini-envt from the class type variables a,b to the instance decl types [p],Int: [a->[p], b->Int] @@ -1333,30 +1380,8 @@ So we * Apply the mini-evnt to them, and check that the result is consistent with the instance types [p] y Int -We do *not* assume (at this point) the the bound variables of -the associated type instance decl are the same as for the parent -instance decl. So, for example, - - instance C [p] Int - type T [q] y Int = ... - -would work equally well. Reason: making the *kind* variables line -up is much harder. Example (Trac #7282): - class Foo (xs :: [k]) where - type Bar xs :: * - - instance Foo '[] where - type Bar '[] = Int -Here the instance decl really looks like - instance Foo k ('[] k) where - type Bar k ('[] k) = Int -but the k's are not scoped, and hence won't match Uniques. - -So instead we just match structure, with tcMatchTyX, and check -that distinct type variables match 1-1 with distinct type variables. - -HOWEVER, we *still* make the instance type variables scope over the -type instances, to pick up non-obvious kinds. Eg +We make all the instance type variables scope over the +type instances, of course, which picks up non-obvious kinds. Eg class Foo (a :: k) where type F a instance Foo (b :: k -> k) where @@ -1367,13 +1392,28 @@ But if the 'b' didn't scope, we would make F's instance too poly-kinded. -} --- | Extra information needed when type-checking associated types. The 'Class' is --- the enclosing class, and the @VarEnv Type@ maps class variables to their --- instance types. -type ClsInfo = (Class, VarEnv Type) +-- | Extra information about the parent instance declaration, needed +-- when type-checking associated types. The 'Class' is the enclosing +-- class, the [TyVar] are the type variable of the instance decl, +-- and and the @VarEnv Type@ maps class variables to their instance +-- types. +type ClsInstInfo = (Class, [TyVar], VarEnv Type) + +type AssocInstArgShape = (Maybe Type, Type) + -- AssocInstArgShape is used only for associated family instances + -- (mb_exp, actual) + -- mb_exp = Just ty => this arg corresponds to a class variable + -- = Nothing => it doesn't correspond to a class variable + -- e.g. class C b where + -- type F a b c + -- instance C [x] where + -- type F p [x] q + -- We get [AssocInstArgShape] = [ (Nothing, p) + -- , (Just [x], [x]) + -- , (Nothing, q)] checkConsistentFamInst - :: Maybe ClsInfo + :: Maybe ClsInstInfo -> TyCon -- ^ Family tycon -> [TyVar] -- ^ Type variables of the family instance -> [Type] -- ^ Type patterns from instance @@ -1381,84 +1421,72 @@ checkConsistentFamInst -- See Note [Checking consistent instantiation] checkConsistentFamInst Nothing _ _ _ = return () -checkConsistentFamInst (Just (clas, mini_env)) fam_tc at_tvs at_tys +checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc _at_tvs at_tys = do { -- Check that the associated type indeed comes from this class checkTc (Just clas == tyConAssoc_maybe fam_tc) (badATErr (className clas) (tyConName fam_tc)) - -- See Note [Checking consistent instantiation] - -- Check right to left, so that we spot type variable - -- inconsistencies before (more confusing) kind variables - ; checkTc (check_args emptyTCvSubst (fam_tc_tvs `zip` at_tys)) - (wrongATArgErr fam_tc expected_args at_tys) } - where - fam_tc_tvs = tyConTyVars fam_tc - expected_args = zipWith pick fam_tc_tvs at_tys - pick fam_tc_tv at_ty = case lookupVarEnv mini_env fam_tc_tv of - Just inst_ty -> inst_ty - Nothing -> at_ty - - check_args :: TCvSubst -> [(TyVar,Type)] -> Bool - check_args subst ((fam_tc_tv, at_ty) : rest) - | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv - = case tcMatchTyX subst at_ty inst_ty of - Just subst -> check_args subst rest - Nothing -> False + -- Check type args first (more comprehensible) + ; checkTc (all check_arg type_shapes) pp_wrong_at_arg + ; checkTc (check_poly_args type_shapes) pp_wrong_at_tyvars - | otherwise - = check_args subst rest - - check_args subst [] - = check_tvs subst [] at_tvs - - check_tvs :: TCvSubst -> [TyVar] -> [TyVar] -> Bool - check_tvs _ _ [] = True -- OK!! - check_tvs subst acc (tv:tvs) - | Just ty <- lookupTyVar subst tv - = case tcGetTyVar_maybe ty of - Nothing -> False - Just tv' | tv' `elem` acc -> False - | otherwise -> check_tvs subst (tv' : acc) tvs - | otherwise - = check_tvs subst acc tvs + -- And now kind args + ; checkTc (all check_arg kind_shapes) + (pp_wrong_at_arg $$ ppSuggestExplicitKinds) + ; checkTc (check_poly_args kind_shapes) + (pp_wrong_at_tyvars $$ ppSuggestExplicitKinds) -{- - check_arg :: (TyVar, Type) -> TCvSubst -> TcM TCvSubst - check_arg (fam_tc_tv, at_ty) subst - | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv - = case tcMatchTyX subst at_ty inst_ty of - Just subst -> return subst - Nothing -> failWithTc $ wrongATArgErr at_ty inst_ty - -- No need to instantiate here, because the axiom - -- uses the same type variables as the assocated class - | otherwise - = return subst -- Allow non-type-variable instantiation - -- See Note [Associated type instances] - - check_distinct :: TCvSubst -> TcM () - -- True if all the variables mapped the substitution - -- map to *distinct* type *variables* - check_distinct subst = go [] at_tvs - where - go _ [] = return () - go acc (tv:tvs) = case lookupTyVar subst tv of - Nothing -> go acc tvs - Just ty | Just tv' <- tcGetTyVar_maybe ty - , tv' `notElem` acc - -> go (tv' : acc) tvs - _other -> addErrTc (dupTyVar tv) --} + ; traceTc "cfi" (vcat [ ppr inst_tvs + , ppr arg_shapes + , ppr mini_env ]) } + where + arg_shapes :: [AssocInstArgShape] + arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty) + | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ] + + (kind_shapes, type_shapes) = partitionInvisibles fam_tc snd arg_shapes + + check_arg :: AssocInstArgShape -> Bool + check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty + check_arg (Nothing, _ ) = True -- Arg position does not correspond + -- to a class variable + check_poly_args :: [(Maybe Type,Type)] -> Bool + check_poly_args arg_shapes + = allDistinctTyVars (mkVarSet inst_tvs) + [ at_ty | (Nothing, at_ty) <- arg_shapes ] + + pp_wrong_at_arg + = vcat [ text "Type indexes must match class instance head" + , pp_exp_act ] + + pp_wrong_at_tyvars + = vcat [ text "Polymorphic type indexes of associated type" <+> quotes (ppr fam_tc) + , nest 2 $ vcat [ text "(i.e. ones independent of the class type variables)" + , text "must be distinct type variables" ] + , pp_exp_act ] + + pp_exp_act + = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args) + , text " Actual:" <+> ppr (mkTyConApp fam_tc at_tys) + , sdocWithDynFlags $ \dflags -> + ppWhen (has_poly_args dflags) $ + vcat [ text "where the `<tv>' arguments are type variables," + , text "distinct from each other and from the instance variables" ] ] + + expected_args = [ exp_ty `orElse` mk_tv at_ty | (exp_ty, at_ty) <- arg_shapes ] + mk_tv at_ty = mkTyVarTy (mkTyVar tv_name (typeKind at_ty)) + tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan + + has_poly_args dflags = any (isNothing . fst) shapes + where + shapes | gopt Opt_PrintExplicitKinds dflags = arg_shapes + | otherwise = type_shapes badATErr :: Name -> Name -> SDoc badATErr clas op = hsep [text "Class", quotes (ppr clas), text "does not have an associated type", quotes (ppr op)] -wrongATArgErr :: TyCon -> [Type] -> [Type] -> SDoc -wrongATArgErr fam_tc expected_args actual_args - = vcat [ text "Type indexes must match class instance head" - , text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args) - , text "Actual: " <+> ppr (mkTyConApp fam_tc actual_args) ] {- ************************************************************************ @@ -1523,7 +1551,7 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches }) -- Check that a "type instance" is well-formed (which includes decidability -- unless -XUndecidableInstances is given). -- -checkValidCoAxBranch :: Maybe ClsInfo +checkValidCoAxBranch :: Maybe ClsInstInfo -> TyCon -> CoAxBranch -> TcM () checkValidCoAxBranch mb_clsinfo fam_tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs @@ -1534,7 +1562,7 @@ checkValidCoAxBranch mb_clsinfo fam_tc -- | Do validity checks on a type family equation, including consistency -- with any enclosing class instance head, termination, and lack of -- polytypes. -checkValidTyFamEqn :: Maybe ClsInfo +checkValidTyFamEqn :: Maybe ClsInstInfo -> TyCon -- ^ of the type family -> [TyVar] -- ^ bound tyvars in the equation -> [CoVar] -- ^ bound covars in the equation @@ -1583,7 +1611,7 @@ checkFamInstRhs lhsTys famInsts what = text "type family application" <+> quotes (pprType (TyConApp tc tys)) bad_tvs = fvTypes tys \\ fvs -checkValidFamPats :: Maybe ClsInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM () +checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM () -- Patterns in a 'type instance' or 'data instance' decl should -- a) contain no type family applications -- (vanilla synonyms are fine, though) @@ -1887,3 +1915,16 @@ isTerminatingClass cls -- | Tidy before printing a type ppr_tidy :: TidyEnv -> Type -> SDoc ppr_tidy env ty = pprType (tidyType env ty) + +allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool +-- (allDistinctTyVars tvs tys) returns True if tys are +-- a) all tyvars +-- b) all distinct +-- c) disjoint from tvs +allDistinctTyVars _ [] = True +allDistinctTyVars tkvs (ty : tys) + = case getTyVar_maybe ty of + Nothing -> False + Just tv | tv `elemVarSet` tkvs -> False + | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys + diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 7ad201360c..9559123dd7 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -95,7 +95,6 @@ module Type ( funTyCon, -- ** Predicates on types - allDistinctTyVars, isTyVarTy, isFunTy, isDictTy, isPredTy, isVoidTy, isCoercionTy, isCoercionTy_maybe, isCoercionType, isForAllTy, isPiTy, @@ -121,7 +120,6 @@ module Type ( tyCoVarsOfTypeDSet, coVarsOfType, coVarsOfTypes, closeOverKinds, - splitDepVarsOfType, splitDepVarsOfTypes, splitVisVarsOfType, splitVisVarsOfTypes, expandTypeSynonyms, typeSize, @@ -585,16 +583,6 @@ repGetTyVar_maybe :: Type -> Maybe TyVar repGetTyVar_maybe (TyVarTy tv) = Just tv repGetTyVar_maybe _ = Nothing -allDistinctTyVars :: [KindOrType] -> Bool -allDistinctTyVars tkvs = go emptyVarSet tkvs - where - go _ [] = True - go so_far (ty : tys) - = case getTyVar_maybe ty of - Nothing -> False - Just tv | tv `elemVarSet` so_far -> False - | otherwise -> go (so_far `extendVarSet` tv) tys - {- --------------------------------------------------------------------- AppTy diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 4d238a5b70..b88cf44860 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -6466,33 +6466,56 @@ keyword in the family instance: :: type Elem [e] = e ... -Note the following points: +The data or type family instance for an assocated type must follow +the following two rules: - The type indexes corresponding to class parameters must have - precisely the same shape the type given in the instance head. To have - the same "shape" means that the two types are identical modulo - renaming of type variables. For example: :: + precisely the same as type given in the instance head. + For example: :: + + class Collects ce where + type Elem ce :: * instance Eq (Elem [e]) => Collects [e] where -- Choose one of the following alternatives: type Elem [e] = e -- OK - type Elem [x] = x -- OK - type Elem x = x -- BAD; shape of 'x' is different to '[e]' - type Elem [Maybe x] = x -- BAD: shape of '[Maybe x]' is different to '[e]' + type Elem [x] = x -- BAD; '[x]' is differnet to '[e]' from head + type Elem x = x -- BAD; 'x' is different to '[e]' + type Elem [Maybe x] = x -- BAD: '[Maybe x]' is different to '[e]' + +- The type indexes of the type family that do *not* correspond to + class parameters must be distinct type variables, not mentioned + in the instance head. For example: :: + + class C b x where + type F a b c :: * + + instance C [v] [w] where + -- Choose one of the following alternatives: + type C a [v] c = a->c -- OK; a,c are tyvars + type C x [v] y = y->x -- OK; x,y are tyvars + type C x [v] x = x -- BAD: x is repeated + type C x [v] w = x -- BAD: w is mentioned in instance head -- An instances for an associated family can only appear as part of an +The effect of these two rules is that the type-family instance +completely covers the cases covered by the instance head. + +- An instance for an associated family can only appear as part of an instance declarations of the class in which the family was declared, just as with the equations of the methods of a class. +- The variables on the right hand side of the type family equation + must, as usual, be bound on the left hand side. + - The instance for an associated type can be omitted in class instances. In that case, unless there is a default instance (see :ref:`assoc-decl-defs`), the corresponding instance type is not inhabited; i.e., only diverging expressions, such as ``undefined``, can assume the type. -- Although it is unusual, there (currently) can be *multiple* instances - for an associated family in a single instance declaration. For - example, this is legitimate: :: +- A historical note. In the past (but no longer), GHC allowed you to + write *multiple* type or data family instances for a single + asssociated type. For example: :: instance GMapKey Flob where data GMap Flob [v] = G1 v @@ -6501,10 +6524,23 @@ Note the following points: Here we give two data instance declarations, one in which the last parameter is ``[v]``, and one for which it is ``Int``. Since you - cannot give any *subsequent* instances for ``(GMap Flob ...)``, this - facility is most useful when the free indexed parameter is of a kind - with a finite number of alternatives (unlike ``*``). WARNING: this - facility may be withdrawn in the future. + cannot give any *subsequent* instances for ``(GMap Flob ...)``, + this facility was not very useful, except perhaps when the free + indexed parameter has a fixed number of alternatives + (e.g. ``Bool`). But in that case it is better to define an auxiliary + closed type function like this: :: + + class C a where + type F a (b :: Bool) :: * + + instance C Int where + type F Int b = FInt b + + type family FInt a b where + FInt True = Char + FInt False = Bool + + Here the auxiliary type function is ``FInt``. .. _assoc-decl-defs: diff --git a/testsuite/tests/ghci/scripts/T4175.hs b/testsuite/tests/ghci/scripts/T4175.hs index 0fc53e76e9..0b7b554062 100644 --- a/testsuite/tests/ghci/scripts/T4175.hs +++ b/testsuite/tests/ghci/scripts/T4175.hs @@ -16,10 +16,10 @@ class C a where type D a b instance C Int where - type D Int () = String + type D Int b = String instance C () where - type D () () = Bool + type D () a = Bool type family E a where E () = Bool diff --git a/testsuite/tests/ghci/scripts/T4175.stdout b/testsuite/tests/ghci/scripts/T4175.stdout index e1ef925bea..d319bd630e 100644 --- a/testsuite/tests/ghci/scripts/T4175.stdout +++ b/testsuite/tests/ghci/scripts/T4175.stdout @@ -1,57 +1,56 @@ -type family A a b :: * -- Defined at T4175.hs:7:1 -type instance A (B a) b = () -- Defined at T4175.hs:10:15 -type instance A (Maybe a) a = a -- Defined at T4175.hs:9:15 -type instance A Int Int = () -- Defined at T4175.hs:8:15 -data family B a -- Defined at T4175.hs:12:1 -instance G B -- Defined at T4175.hs:34:10 -data instance B () = MkB -- Defined at T4175.hs:13:15 -type instance A (B a) b = () -- Defined at T4175.hs:10:15 -class C a where - type family D a b :: * - -- Defined at T4175.hs:16:5 -type instance D () () = Bool -- Defined at T4175.hs:22:10 -type instance D Int () = String -- Defined at T4175.hs:19:10 -type family E a :: * - where - E () = Bool - E Int = String - -- Defined at T4175.hs:24:1 -data () = () -- Defined in ‘GHC.Tuple’ -instance C () -- Defined at T4175.hs:21:10 -instance Bounded () -- Defined in ‘GHC.Enum’ -instance Enum () -- Defined in ‘GHC.Enum’ -instance Eq () -- Defined in ‘GHC.Classes’ -instance Ord () -- Defined in ‘GHC.Classes’ -instance Read () -- Defined in ‘GHC.Read’ -instance Show () -- Defined in ‘GHC.Show’ -instance Monoid () -- Defined in ‘GHC.Base’ -type instance D () () = Bool -- Defined at T4175.hs:22:10 -type instance D Int () = String -- Defined at T4175.hs:19:10 -data instance B () = MkB -- Defined at T4175.hs:13:15 -data Maybe a = Nothing | Just a -- Defined in ‘GHC.Base’ -instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’ -instance Monad Maybe -- Defined in ‘GHC.Base’ -instance Functor Maybe -- Defined in ‘GHC.Base’ -instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Base’ -instance Read a => Read (Maybe a) -- Defined in ‘GHC.Read’ -instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’ -instance Applicative Maybe -- Defined in ‘GHC.Base’ -instance Foldable Maybe -- Defined in ‘Data.Foldable’ -instance Traversable Maybe -- Defined in ‘Data.Traversable’ -instance Monoid a => Monoid (Maybe a) -- Defined in ‘GHC.Base’ -type instance A (Maybe a) a = a -- Defined at T4175.hs:9:15 -data Int = I# Int# -- Defined in ‘GHC.Types’ -instance C Int -- Defined at T4175.hs:18:10 -instance Bounded Int -- Defined in ‘GHC.Enum’ -instance Enum Int -- Defined in ‘GHC.Enum’ -instance Eq Int -- Defined in ‘GHC.Classes’ -instance Integral Int -- Defined in ‘GHC.Real’ -instance Num Int -- Defined in ‘GHC.Num’ -instance Ord Int -- Defined in ‘GHC.Classes’ -instance Read Int -- Defined in ‘GHC.Read’ -instance Real Int -- Defined in ‘GHC.Real’ -instance Show Int -- Defined in ‘GHC.Show’ -type instance D Int () = String -- Defined at T4175.hs:19:10 -type instance A Int Int = () -- Defined at T4175.hs:8:15 -class Z a -- Defined at T4175.hs:28:1 -instance F (Z a) -- Defined at T4175.hs:31:10 +type family A a b :: * -- Defined at T4175.hs:7:1
+type instance A (B a) b = () -- Defined at T4175.hs:10:15
+type instance A (Maybe a) a = a -- Defined at T4175.hs:9:15
+type instance A Int Int = () -- Defined at T4175.hs:8:15
+data family B a -- Defined at T4175.hs:12:1
+instance G B -- Defined at T4175.hs:34:10
+data instance B () = MkB -- Defined at T4175.hs:13:15
+type instance A (B a) b = () -- Defined at T4175.hs:10:15
+class C a where
+ type family D a b :: *
+ -- Defined at T4175.hs:16:5
+type instance D () a = Bool -- Defined at T4175.hs:22:10
+type instance D Int b = String -- Defined at T4175.hs:19:10
+type family E a :: *
+ where
+ E () = Bool
+ E Int = String
+ -- Defined at T4175.hs:24:1
+data () = () -- Defined in ‘GHC.Tuple’
+instance C () -- Defined at T4175.hs:21:10
+instance Bounded () -- Defined in ‘GHC.Enum’
+instance Enum () -- Defined in ‘GHC.Enum’
+instance Eq () -- Defined in ‘GHC.Classes’
+instance Ord () -- Defined in ‘GHC.Classes’
+instance Read () -- Defined in ‘GHC.Read’
+instance Show () -- Defined in ‘GHC.Show’
+instance Monoid () -- Defined in ‘GHC.Base’
+type instance D () a = Bool -- Defined at T4175.hs:22:10
+data instance B () = MkB -- Defined at T4175.hs:13:15
+data Maybe a = Nothing | Just a -- Defined in ‘GHC.Base’
+instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’
+instance Monad Maybe -- Defined in ‘GHC.Base’
+instance Functor Maybe -- Defined in ‘GHC.Base’
+instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Base’
+instance Read a => Read (Maybe a) -- Defined in ‘GHC.Read’
+instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
+instance Applicative Maybe -- Defined in ‘GHC.Base’
+instance Foldable Maybe -- Defined in ‘Data.Foldable’
+instance Traversable Maybe -- Defined in ‘Data.Traversable’
+instance Monoid a => Monoid (Maybe a) -- Defined in ‘GHC.Base’
+type instance A (Maybe a) a = a -- Defined at T4175.hs:9:15
+data Int = I# Int# -- Defined in ‘GHC.Types’
+instance C Int -- Defined at T4175.hs:18:10
+instance Bounded Int -- Defined in ‘GHC.Enum’
+instance Enum Int -- Defined in ‘GHC.Enum’
+instance Eq Int -- Defined in ‘GHC.Classes’
+instance Integral Int -- Defined in ‘GHC.Real’
+instance Num Int -- Defined in ‘GHC.Num’
+instance Ord Int -- Defined in ‘GHC.Classes’
+instance Read Int -- Defined in ‘GHC.Read’
+instance Real Int -- Defined in ‘GHC.Real’
+instance Show Int -- Defined in ‘GHC.Show’
+type instance D Int b = String -- Defined at T4175.hs:19:10
+type instance A Int Int = () -- Defined at T4175.hs:8:15
+class Z a -- Defined at T4175.hs:28:1
+instance F (Z a) -- Defined at T4175.hs:31:10
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr index c81c5218f8..5964262843 100644 --- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr +++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr @@ -38,11 +38,14 @@ L a = MaybeSyn a -- Defined at <interactive>:49:15 <interactive>:55:41: error: - Type family equation violates injectivity annotation. - Kind variable ‘k’ cannot be inferred from the right-hand side. - (enabling -fprint-explicit-kinds might help) - In the type family equation: - PolyKindVarsF '[] = '[] -- Defined at <interactive>:55:41 + • Polymorphic type indexes of associated type ‘PolyKindVarsF’ + (i.e. ones independent of the class type variables) + must be distinct type variables + Expected: PolyKindVarsF '[] + Actual: PolyKindVarsF '[] + Use -fprint-explicit-kinds to see the kind arguments + • In the type instance declaration for ‘PolyKindVarsF’ + In the instance declaration for ‘PolyKindVarsC '[]’ <interactive>:60:15: error: Type family equation violates injectivity annotation. diff --git a/testsuite/tests/indexed-types/should_compile/T10931.hs b/testsuite/tests/indexed-types/should_compile/T10931.hs index 44e5865177..2c0ea204d3 100644 --- a/testsuite/tests/indexed-types/should_compile/T10931.hs +++ b/testsuite/tests/indexed-types/should_compile/T10931.hs @@ -20,6 +20,6 @@ class ( m ~ Outer m (Inner m) ) => BugC (m :: * -> *) where instance BugC (IdT m) where type Inner (IdT m) = m - type Outer (IdT _) = IdT + type Outer (IdT m) = IdT bug f = IdC f diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs index 4bd7bde8df..57a9595254 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs @@ -8,6 +8,7 @@ class C8 a where instance C8 Int where data S8 Int a = S8Int a --- Extra argument is not a variable; this is fine +-- Extra argument is not a variable; +-- this is now not allowed instance C8 Bool where data S8 Bool Char = S8Bool diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr new file mode 100644 index 0000000000..9b99cd1322 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr @@ -0,0 +1,11 @@ + +SimpleFail10.hs:14:3: error: + • Polymorphic type indexes of associated type ‘S8’ + (i.e. ones independent of the class type variables) + must be distinct type variables + Expected: S8 Bool <tv> + Actual: S8 Bool Char + where the `<tv>' arguments are type variables, + distinct from each other and from the instance variables + • In the data instance declaration for ‘S8’ + In the instance declaration for ‘C8 Bool’ diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs index 927c60caf0..9c1c4a82d2 100644 --- a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs @@ -8,8 +8,7 @@ class C7 a b where instance C7 Char (a, Bool) where data S7 (a, Bool) = S7_1 --- Used to fail, but now passes: --- type indexes don't match the instance types by name --- but do by structure +-- Fails because the arg to S7 should be the +-- same as that to C7 instance C7 Char (a, Int) where data S7 (b, Int) = S7_2 diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr new file mode 100644 index 0000000000..b0c421fce8 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr @@ -0,0 +1,7 @@ + +SimpleFail9.hs:14:3: error: + • Type indexes must match class instance head + Expected: S7 (a, Int) + Actual: S7 (b, Int) + • In the data instance declaration for ‘S7’ + In the instance declaration for ‘C7 Char (a, Int)’ diff --git a/testsuite/tests/indexed-types/should_fail/T11450.hs b/testsuite/tests/indexed-types/should_fail/T11450.hs new file mode 100644 index 0000000000..59ef495c53 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T11450.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE TypeFamilies #-} + +module T11450 where + +class C x where + type T x + +instance C (Either a b) where + type T (Either b a) = b -> a diff --git a/testsuite/tests/indexed-types/should_fail/T11450.stderr b/testsuite/tests/indexed-types/should_fail/T11450.stderr new file mode 100644 index 0000000000..a6fe961fcf --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T11450.stderr @@ -0,0 +1,7 @@ + +T11450.hs:9:8: error: + • Type indexes must match class instance head + Expected: T (Either a b) + Actual: T (Either b a) + • In the type instance declaration for ‘T’ + In the instance declaration for ‘C (Either a b)’ diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index c6f29a492f..dfc0326154 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -11,8 +11,8 @@ test('SimpleFail5b', normal, compile_fail, ['']) test('SimpleFail6', normal, compile_fail, ['']) test('SimpleFail7', normal, compile_fail, ['']) test('SimpleFail8', normal, compile_fail, ['']) -test('SimpleFail9', normal, compile, ['']) -test('SimpleFail10', normal, compile, ['']) +test('SimpleFail9', normal, compile_fail, ['']) +test('SimpleFail10', normal, compile_fail, ['']) test('SimpleFail11a', normal, compile_fail, ['']) test('SimpleFail11b', normal, compile_fail, ['']) test('SimpleFail11c', normal, compile_fail, ['']) @@ -139,3 +139,4 @@ test('T10817', normal, compile_fail, ['']) test('T10899', normal, compile_fail, ['']) test('T11136', normal, compile_fail, ['']) test('T7788', normal, compile_fail, ['']) +test('T11450', normal, compile_fail, ['']) diff --git a/testsuite/tests/polykinds/T10570.stderr b/testsuite/tests/polykinds/T10570.stderr index f40ed10ce4..3c91db5cfb 100644 --- a/testsuite/tests/polykinds/T10570.stderr +++ b/testsuite/tests/polykinds/T10570.stderr @@ -1,9 +1,9 @@ T10570.hs:10:10: error: - Illegal instance declaration for ‘ConsByIdx2 Int a Proxy cls’ - The coverage condition fails in class ‘ConsByIdx2’ - for functional dependency: ‘x -> m’ - Reason: lhs type ‘Int’ does not determine rhs type ‘Proxy’ - Un-determined variable: k - (Use -fprint-explicit-kinds to see the kind variables in the types) - In the instance declaration for ‘ConsByIdx2 Int a Proxy cls’ + • Illegal instance declaration for ‘ConsByIdx2 Int a Proxy cls’ + The coverage condition fails in class ‘ConsByIdx2’ + for functional dependency: ‘x -> m’ + Reason: lhs type ‘Int’ does not determine rhs type ‘Proxy’ + Un-determined variable: k + Use -fprint-explicit-kinds to see the kind arguments + • In the instance declaration for ‘ConsByIdx2 Int a Proxy cls’ diff --git a/testsuite/tests/th/T9692.hs b/testsuite/tests/th/T9692.hs index 770290d7db..3f67b0dee9 100644 --- a/testsuite/tests/th/T9692.hs +++ b/testsuite/tests/th/T9692.hs @@ -8,7 +8,7 @@ import Language.Haskell.TH.Ppr import System.IO class C a where - data F a (b :: k) :: * + data F a b :: * instance C Int where data F Int x = FInt x diff --git a/testsuite/tests/th/T9692.stderr b/testsuite/tests/th/T9692.stderr index ffa55365d4..f99d12bd74 100644 --- a/testsuite/tests/th/T9692.stderr +++ b/testsuite/tests/th/T9692.stderr @@ -1,2 +1,2 @@ -data family T9692.F (a_0 :: k_1) (b_2 :: k_3) :: * -data instance T9692.F GHC.Types.Int (x_4 :: *) = T9692.FInt x_4 +data family T9692.F (a_0 :: k_1) (b_2 :: *) :: * +data instance T9692.F GHC.Types.Int x_3 = T9692.FInt x_3 diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.hs b/testsuite/tests/typecheck/should_fail/T6018fail.hs index 44f5024f41..bb3c93c67b 100644 --- a/testsuite/tests/typecheck/should_fail/T6018fail.hs +++ b/testsuite/tests/typecheck/should_fail/T6018fail.hs @@ -50,8 +50,8 @@ type MaybeSyn a = Id a type family L a = r | r -> a type instance L a = MaybeSyn a --- These should fail because given the RHS kind there is no way to determine LHS --- kind +-- These should fail because given the RHS kind +-- there is no way to determine LHS kind class PolyKindVarsC a where type PolyKindVarsF a = (r :: k) | r -> a diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr index 49e89afe54..95b9d1bb3e 100644 --- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr +++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr @@ -58,11 +58,14 @@ T6018fail.hs:51:15: error: L a = MaybeSyn a -- Defined at T6018fail.hs:51:15 T6018fail.hs:59:10: error: - Type family equation violates injectivity annotation. - Kind variable ‘k’ cannot be inferred from the right-hand side. - (enabling -fprint-explicit-kinds might help) - In the type family equation: - PolyKindVarsF '[] = '[] -- Defined at T6018fail.hs:59:10 + • Polymorphic type indexes of associated type ‘PolyKindVarsF’ + (i.e. ones independent of the class type variables) + must be distinct type variables + Expected: PolyKindVarsF '[] + Actual: PolyKindVarsF '[] + Use -fprint-explicit-kinds to see the kind arguments + • In the type instance declaration for ‘PolyKindVarsF’ + In the instance declaration for ‘PolyKindVarsC '[]’ T6018fail.hs:62:15: error: Type family equation violates injectivity annotation. diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr index c151553a3a..6cc0c3700e 100644 --- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr +++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr @@ -1,96 +1,96 @@ T6018failclosed.hs:11:5: error: - Type family equation violates injectivity annotation. - RHS of injective type family equation cannot be a type family: - IdProxyClosed a = IdClosed a -- Defined at T6018failclosed.hs:11:5 - In the equations for closed type family ‘IdProxyClosed’ - In the type family declaration for ‘IdProxyClosed’ + • Type family equation violates injectivity annotation. + RHS of injective type family equation cannot be a type family: + IdProxyClosed a = IdClosed a -- Defined at T6018failclosed.hs:11:5 + • In the equations for closed type family ‘IdProxyClosed’ + In the type family declaration for ‘IdProxyClosed’ T6018failclosed.hs:19:5: error: - Type family equation violates injectivity annotation. - RHS of injective type family equation is a bare type variable - but these LHS type and kind patterns are not bare variables: ‘'Z’ - PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5 - In the equations for closed type family ‘PClosed’ - In the type family declaration for ‘PClosed’ + • Type family equation violates injectivity annotation. + RHS of injective type family equation is a bare type variable + but these LHS type and kind patterns are not bare variables: ‘'Z’ + PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5 + • In the equations for closed type family ‘PClosed’ + In the type family declaration for ‘PClosed’ T6018failclosed.hs:19:5: error: - Type family equations violate injectivity annotation: - PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5 - PClosed ('S n) m = 'S (PClosed n m) - -- Defined at T6018failclosed.hs:20:5 - In the equations for closed type family ‘PClosed’ - In the type family declaration for ‘PClosed’ + • Type family equations violate injectivity annotation: + PClosed 'Z m = m -- Defined at T6018failclosed.hs:19:5 + PClosed ('S n) m = 'S (PClosed n m) + -- Defined at T6018failclosed.hs:20:5 + • In the equations for closed type family ‘PClosed’ + In the type family declaration for ‘PClosed’ T6018failclosed.hs:25:5: error: - Type family equation violates injectivity annotation. - Type and kind variables ‘k’, ‘b’ - cannot be inferred from the right-hand side. - (enabling -fprint-explicit-kinds might help) - In the type family equation: - forall k k1 (b :: k) (c :: k1). - JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5 - In the equations for closed type family ‘JClosed’ - In the type family declaration for ‘JClosed’ + • Type family equation violates injectivity annotation. + Type and kind variables ‘k’, ‘b’ + cannot be inferred from the right-hand side. + Use -fprint-explicit-kinds to see the kind arguments + In the type family equation: + forall k k1 (b :: k) (c :: k1). + JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5 + • In the equations for closed type family ‘JClosed’ + In the type family declaration for ‘JClosed’ T6018failclosed.hs:30:5: error: - Type family equation violates injectivity annotation. - Type variable ‘n’ cannot be inferred from the right-hand side. - In the type family equation: - KClosed ('S n) m = 'S m -- Defined at T6018failclosed.hs:30:5 - In the equations for closed type family ‘KClosed’ - In the type family declaration for ‘KClosed’ + • Type family equation violates injectivity annotation. + Type variable ‘n’ cannot be inferred from the right-hand side. + In the type family equation: + KClosed ('S n) m = 'S m -- Defined at T6018failclosed.hs:30:5 + • In the equations for closed type family ‘KClosed’ + In the type family declaration for ‘KClosed’ T6018failclosed.hs:35:5: error: - Type family equation violates injectivity annotation. - RHS of injective type family equation cannot be a type family: - forall k (a :: k). - LClosed a = MaybeSynClosed a -- Defined at T6018failclosed.hs:35:5 - In the equations for closed type family ‘LClosed’ - In the type family declaration for ‘LClosed’ + • Type family equation violates injectivity annotation. + RHS of injective type family equation cannot be a type family: + forall k (a :: k). + LClosed a = MaybeSynClosed a -- Defined at T6018failclosed.hs:35:5 + • In the equations for closed type family ‘LClosed’ + In the type family declaration for ‘LClosed’ T6018failclosed.hs:39:5: error: - Type family equations violate injectivity annotation: - FClosed Char Bool Int = Int -- Defined at T6018failclosed.hs:39:5 - FClosed Bool Int Char = Int -- Defined at T6018failclosed.hs:40:5 - In the equations for closed type family ‘FClosed’ - In the type family declaration for ‘FClosed’ + • Type family equations violate injectivity annotation: + FClosed Char Bool Int = Int -- Defined at T6018failclosed.hs:39:5 + FClosed Bool Int Char = Int -- Defined at T6018failclosed.hs:40:5 + • In the equations for closed type family ‘FClosed’ + In the type family declaration for ‘FClosed’ T6018failclosed.hs:43:5: error: - Type family equations violate injectivity annotation: - IClosed Int Char Bool = Bool -- Defined at T6018failclosed.hs:43:5 - IClosed Int Int Int = Bool -- Defined at T6018failclosed.hs:44:5 - In the equations for closed type family ‘IClosed’ - In the type family declaration for ‘IClosed’ + • Type family equations violate injectivity annotation: + IClosed Int Char Bool = Bool -- Defined at T6018failclosed.hs:43:5 + IClosed Int Int Int = Bool -- Defined at T6018failclosed.hs:44:5 + • In the equations for closed type family ‘IClosed’ + In the type family declaration for ‘IClosed’ T6018failclosed.hs:49:3: error: - Type family equations violate injectivity annotation: - E2 'True = 'False -- Defined at T6018failclosed.hs:49:3 - E2 a = 'False -- Defined at T6018failclosed.hs:50:3 - In the equations for closed type family ‘E2’ - In the type family declaration for ‘E2’ + • Type family equations violate injectivity annotation: + E2 'True = 'False -- Defined at T6018failclosed.hs:49:3 + E2 a = 'False -- Defined at T6018failclosed.hs:50:3 + • In the equations for closed type family ‘E2’ + In the type family declaration for ‘E2’ T6018failclosed.hs:50:3: error: - Type family equation violates injectivity annotation. - Type variable ‘a’ cannot be inferred from the right-hand side. - In the type family equation: - E2 a = 'False -- Defined at T6018failclosed.hs:50:3 - In the equations for closed type family ‘E2’ - In the type family declaration for ‘E2’ + • Type family equation violates injectivity annotation. + Type variable ‘a’ cannot be inferred from the right-hand side. + In the type family equation: + E2 a = 'False -- Defined at T6018failclosed.hs:50:3 + • In the equations for closed type family ‘E2’ + In the type family declaration for ‘E2’ T6018failclosed.hs:61:3: error: - Type family equations violate injectivity annotation: - F a IO = IO a -- Defined at T6018failclosed.hs:61:3 - F Char b = b Int -- Defined at T6018failclosed.hs:62:3 - In the equations for closed type family ‘F’ - In the type family declaration for ‘F’ + • Type family equations violate injectivity annotation: + F a IO = IO a -- Defined at T6018failclosed.hs:61:3 + F Char b = b Int -- Defined at T6018failclosed.hs:62:3 + • In the equations for closed type family ‘F’ + In the type family declaration for ‘F’ T6018failclosed.hs:66:5: error: - Type family equation violates injectivity annotation. - Kind variable ‘k’ cannot be inferred from the right-hand side. - (enabling -fprint-explicit-kinds might help) - In the type family equation: - forall k (a :: k) (b :: k). - Gc a b = Int -- Defined at T6018failclosed.hs:66:5 - In the equations for closed type family ‘Gc’ - In the type family declaration for ‘Gc’ + • Type family equation violates injectivity annotation. + Kind variable ‘k’ cannot be inferred from the right-hand side. + Use -fprint-explicit-kinds to see the kind arguments + In the type family equation: + forall k (a :: k) (b :: k). + Gc a b = Int -- Defined at T6018failclosed.hs:66:5 + • In the equations for closed type family ‘Gc’ + In the type family declaration for ‘Gc’ |