Commit 8136a5cb authored by Simon Peyton Jones's avatar Simon Peyton Jones

Tighten checking for associated type instances

This patch finishes off Trac #11450.  Following debate on that ticket,
the patch tightens up the rules for what the instances of an
associated type can look like.  Now they must match the instance
header exactly. Eg

   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)

Previously we allowed multiple instance equations and now, in effect,
we don't since they would all overlap.  If you want multiple cases,
use an auxiliary type family.

This is consistent with the treatment of generic-default instances,
and the user manual always said "WARNING: this facility (multiple
instance equations may be withdrawn in the future".

I also improved error messages, and did other minor refactoring.
parent 17eb2419
......@@ -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.
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......@@ -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
......
......@@ -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