Commit bcbfdd03 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Yet more refactoring in overlapping type-family instances

This patch mainly introduces TcValidity.checkConsistendFamInst,
and uses it when typechecking type-family instances, *including*
default instances.

I find I can't remember why I began this particular saga, but
it's a modest improvement I think.
parent 59438868
......@@ -20,9 +20,9 @@ module TcInstDcls ( tcInstDecls1, tcInstDecls2 ) where
import HsSyn
import TcBinds
import TcTyClsDecls( tcAddImplicits, tcAddTyFamInstCtxt, tcAddDataFamInstCtxt,
tcAddFamInstCtxt, tcSynFamInstDecl,
tcSynFamInstDecl,
wrongKindOfFamily, tcFamTyPats, kcDataDefn, dataDeclChecks,
tcConDecls, checkValidTyCon, badATErr, wrongATArgErr )
tcConDecls, checkValidTyCon, tcAddFamInstCtxt )
import TcClassDcl( tcClassDecl2,
HsSigFun, lookupHsSig, mkHsSigFun, emptyHsSigs,
findMethodBind, instantiateMethod, tcInstanceMethodBody )
......@@ -41,7 +41,6 @@ import TcDeriv
import TcEnv
import TcHsType
import TcUnify
import Unify ( tcMatchTyX )
import MkCore ( nO_METHOD_BINDING_ERROR_ID )
import CoreSyn ( DFunArg(..) )
import Type
......@@ -640,19 +639,15 @@ tcTyFamInstDecl mb_clsinfo fam_tc (L loc decl@(TyFamInstDecl { tfid_group = grou
check_valid_branch :: [CoAxBranch] -- previous
-> CoAxBranch -- current
-> TcM [CoAxBranch] -- current : previous
check_valid_branch prev_branches
cur_branch@(CoAxBranch { cab_tvs = t_tvs, cab_lhs = t_typats
, cab_rhs = t_rhs, cab_loc = loc })
= setSrcSpan loc $
check_valid_branch prev_branches cur_branch
= tcAddFamInstCtxt (ptext (sLit "type")) (tyConName fam_tc) $
do { -- Check the well-formedness of the instance
checkValidTyFamInst fam_tc t_tvs t_typats t_rhs
-- Check that type patterns match the class instance head
; checkConsistentFamInst mb_clsinfo (ptext (sLit "type")) fam_tc t_tvs t_typats
checkValidTyFamInst mb_clsinfo fam_tc cur_branch
-- Check whether the branch is dominated by earlier
-- ones and hence is inaccessible
; when (t_typats `isDominatedBy` prev_branches) $
; when (cur_branch `isDominatedBy` prev_branches) $
setSrcSpan (coAxBranchSpan cur_branch) $
addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch
; return $ cur_branch : prev_branches }
......@@ -667,6 +662,7 @@ tcDataFamInstDecl mb_clsinfo fam_tc
, dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = ctxt, dd_cons = cons } }))
= setSrcSpan loc $
tcAddFamInstCtxt (ppr new_or_data) (tyConName fam_tc) $
do { -- Check that the family declaration is for the right kind
checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
......@@ -680,7 +676,7 @@ tcDataFamInstDecl mb_clsinfo fam_tc
-- foralls earlier)
checkValidFamPats fam_tc tvs' pats'
-- Check that type patterns match class instance head, if any
; checkConsistentFamInst mb_clsinfo (ppr new_or_data) fam_tc tvs' pats'
; checkConsistentFamInst mb_clsinfo fam_tc tvs' pats'
-- Result kind must be '*' (otherwise, we have too few patterns)
; checkTc (isLiftedTypeKind res_kind) $ tooFewParmsErr (tyConArity fam_tc)
......@@ -722,129 +718,6 @@ tcDataFamInstDecl mb_clsinfo fam_tc
\end{code}
Note [Associated type instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We allow this:
class C a where
type T x a
instance C Int where
type T (S y) Int = y
type T Z Int = Char
Note that
a) The variable 'x' is not bound by the class decl
b) 'x' is instantiated to a non-type-variable in the instance
c) There are several type instance decls for T in the instance
All this is fine. Of course, you can't give any *more* instances
for (T ty Int) elsewhere, becuase it's an *associated* type.
Note [Checking consistent instantiation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
class C a b where
type T a x b
instance C [p] Int
type T [p] y Int = (p,y,y) -- Induces the family instance TyCon
-- type TR p y = (p,y,y)
So we
* Form the mini-envt from the class type variables a,b
to the instance decl types [p],Int: [a->[p], b->Int]
* Look at the tyvars a,x,b of the type family constructor T
(it shares tyvars with the class C)
* 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 assoicated 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 variales 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
class Foo (a :: k) where
type F a
instance Foo (b :: k -> k) where
type F b = Int
Here the instance is kind-indexed and really looks like
type F (k->k) (b::k->k) = Int
But if the 'b' didn't scope, we would make F's instance too
poly-kinded.
\begin{code}
checkConsistentFamInst
:: Maybe ( Class
, VarEnv Type ) -- ^ Class of associated type
-- and instantiation of class TyVars
-> SDoc -- ^ "flavor" of the instance
-> TyCon -- ^ Family tycon
-> [TyVar] -- ^ Type variables of the family instance
-> [Type] -- ^ Type patterns from instance
-> TcM ()
-- See Note [Checking consistent instantiation]
checkConsistentFamInst Nothing _ _ _ _ = return ()
checkConsistentFamInst (Just (clas, mini_env)) flav fam_tc at_tvs at_tys
= tcAddFamInstCtxt flav (tyConName fam_tc) $
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] in TcTyClsDecls
-- Check right to left, so that we spot type variable
-- inconsistencies before (more confusing) kind variables
; discardResult $ foldrM check_arg emptyTvSubst $
tyConTyVars fam_tc `zip` at_tys }
where
at_tv_set = mkVarSet at_tvs
check_arg :: (TyVar, Type) -> TvSubst -> TcM TvSubst
check_arg (fam_tc_tv, at_ty) subst
| Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
= case tcMatchTyX at_tv_set subst at_ty inst_ty of
Just subst | all_distinct subst -> return subst
_ -> failWithTc $ wrongATArgErr at_ty inst_ty
-- No need to instantiate here, becuase the axiom
-- uses the same type variables as the assocated class
| otherwise
= return subst -- Allow non-type-variable instantiation
-- See Note [Associated type instances]
all_distinct :: TvSubst -> Bool
-- True if all the variables mapped the substitution
-- map to *distinct* type *variables*
all_distinct subst = go [] at_tvs
where
go _ [] = True
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 -> False
\end{code}
%************************************************************************
%* *
Type-checking instance declarations, pass 2
......
......@@ -21,8 +21,8 @@ module TcTyClsDecls (
-- data/type family instance declarations
kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
tcSynFamInstDecl, tcFamTyPats,
tcAddFamInstCtxt, tcAddTyFamInstCtxt, tcAddDataFamInstCtxt,
wrongKindOfFamily, badATErr, wrongATArgErr
tcAddTyFamInstCtxt, tcAddDataFamInstCtxt, tcAddFamInstCtxt,
wrongKindOfFamily,
) where
#include "HsVersions.h"
......@@ -54,6 +54,7 @@ import Id
import MkCore ( rEC_SEL_ERROR_ID )
import IdInfo
import Var
import VarEnv
import VarSet
import Module
import Name
......@@ -1467,36 +1468,10 @@ checkValidClass cls
-- type variable. What a mess!
check_at_defs (fam_tc, defs)
= do { mapM_ (\(CoAxBranch { cab_tvs = tvs, cab_lhs = pats, cab_rhs = rhs })
-> checkValidTyFamInst fam_tc tvs pats rhs) defs
; tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $
mapM_ (check_loc_at_def fam_tc) defs }
-- Check that the index of the type instance is the same as on
-- its parent class. Eg
-- class C a b where
-- type F b x a ::*
-- instnace C Int Bool where
-- type F Bool Char Int = Int
-- type F Bool Bool Int = Bool
-- Here the first and third args should match
-- the (C Int Bool) header
-- This is not to do with soundness; it's just checking that the
-- type instance arg is the sam
check_loc_at_def fam_tc (CoAxBranch { cab_lhs = pats, cab_loc = loc })
-- Set the location for each of the default declarations
= setSrcSpan loc $ zipWithM_ check_arg (tyConTyVars fam_tc) pats
-- We only want to check this on the *class* TyVars,
-- not the *family* TyVars (there may be more of these)
-- Nor do we want to check kind vars, for which we don't enforce
-- the "same name as parent" rule as we do for type variables
-- c.f. Trac #7073
check_arg fam_tc_tv at_ty
= checkTc ( isKindVar fam_tc_tv
|| not (fam_tc_tv `elem` tyvars)
|| mkTyVarTy fam_tc_tv `eqType` at_ty)
(wrongATArgErr at_ty (mkTyVarTy fam_tc_tv))
= tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $
mapM_ (checkValidTyFamInst mb_clsinfo fam_tc) defs
mb_clsinfo = Just (cls, mkVarEnv [ (tv, mkTyVarTy tv) | tv <- tyvars ])
checkFamFlag :: Name -> TcM ()
-- Check that we don't use families without -XTypeFamilies
......@@ -1733,14 +1708,6 @@ tcAddDefaultAssocDeclCtxt name thing_inside
ctxt = hsep [ptext (sLit "In the type synonym instance default declaration for"),
quotes (ppr name)]
tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
tcAddFamInstCtxt flavour tycon thing_inside
= addErrCtxt ctxt thing_inside
where
ctxt = hsep [ptext (sLit "In the") <+> flavour
<+> ptext (sLit "declaration for"),
quotes (ppr tycon)]
tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a
tcAddTyFamInstCtxt decl
| [_] <- tfid_eqns decl
......@@ -1753,6 +1720,14 @@ tcAddDataFamInstCtxt decl
= tcAddFamInstCtxt ((pprDataFamInstFlavour decl) <+> (ptext (sLit "instance")))
(unLoc (dfid_tycon decl))
tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
tcAddFamInstCtxt flavour tycon thing_inside
= addErrCtxt ctxt thing_inside
where
ctxt = hsep [ptext (sLit "In the") <+> flavour
<+> ptext (sLit "declaration for"),
quotes (ppr tycon)]
resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
resultTypeMisMatch field_name con1 con2
= vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
......@@ -1817,11 +1792,6 @@ badGadtKindCon data_con
<+> ptext (sLit "cannot be GADT-like in its *kind* arguments"))
2 (ppr data_con <+> dcolon <+> ppr (dataConUserType data_con))
badATErr :: Name -> Name -> SDoc
badATErr clas op
= hsep [ptext (sLit "Class"), quotes (ppr clas),
ptext (sLit "does not have an associated type"), quotes (ppr op)]
badGadtDecl :: Name -> SDoc
badGadtDecl tc_name
= vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
......@@ -1873,13 +1843,6 @@ emptyConDeclsErr tycon
= sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
nest 2 $ ptext (sLit "(-XEmptyDataDecls permits this)")]
wrongATArgErr :: Type -> Type -> SDoc
wrongATArgErr ty instTy =
sep [ ptext (sLit "Type indexes must match class instance head")
, ptext (sLit "Found") <+> quotes (ppr ty)
<+> ptext (sLit "but expected") <+> quotes (ppr instTy)
]
wrongNumberOfParmsErr :: Arity -> SDoc
wrongNumberOfParmsErr exp_arity
= ptext (sLit "Number of parameters must match family declaration; expected")
......
......@@ -10,7 +10,8 @@ module TcValidity (
checkValidTheta, checkValidFamPats,
checkValidInstHead, checkValidInstance, validDerivPred,
checkInstTermination, checkValidTyFamInst, checkTyFamFreeness,
arityErr
checkConsistentFamInst,
arityErr, badATErr
) where
#include "HsVersions.h"
......@@ -22,7 +23,9 @@ import TypeRep
import TcType
import TcMType
import Type
import Unify( tcMatchTyX )
import Kind
import CoAxiom
import Class
import TyCon
......@@ -31,6 +34,7 @@ import HsSyn -- HsType
import TcRnMonad -- TcType, amongst others
import FunDeps
import Name
import VarEnv
import VarSet
import ErrUtils
import PrelNames
......@@ -906,6 +910,140 @@ undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
\end{code}
Note [Associated type instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We allow this:
class C a where
type T x a
instance C Int where
type T (S y) Int = y
type T Z Int = Char
Note that
a) The variable 'x' is not bound by the class decl
b) 'x' is instantiated to a non-type-variable in the instance
c) There are several type instance decls for T in the instance
All this is fine. Of course, you can't give any *more* instances
for (T ty Int) elsewhere, becuase it's an *associated* type.
Note [Checking consistent instantiation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
class C a b where
type T a x b
instance C [p] Int
type T [p] y Int = (p,y,y) -- Induces the family instance TyCon
-- type TR p y = (p,y,y)
So we
* Form the mini-envt from the class type variables a,b
to the instance decl types [p],Int: [a->[p], b->Int]
* Look at the tyvars a,x,b of the type family constructor T
(it shares tyvars with the class C)
* 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 assoicated 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 variales 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
class Foo (a :: k) where
type F a
instance Foo (b :: k -> k) where
type F b = Int
Here the instance is kind-indexed and really looks like
type F (k->k) (b::k->k) = Int
But if the 'b' didn't scope, we would make F's instance too
poly-kinded.
\begin{code}
checkConsistentFamInst
:: Maybe ( Class
, VarEnv Type ) -- ^ Class of associated type
-- and instantiation of class TyVars
-> TyCon -- ^ Family tycon
-> [TyVar] -- ^ Type variables of the family instance
-> [Type] -- ^ Type patterns from instance
-> TcM ()
-- See Note [Checking consistent instantiation]
checkConsistentFamInst Nothing _ _ _ = return ()
checkConsistentFamInst (Just (clas, 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] in TcTyClsDecls
-- Check right to left, so that we spot type variable
-- inconsistencies before (more confusing) kind variables
; discardResult $ foldrM check_arg emptyTvSubst $
tyConTyVars fam_tc `zip` at_tys }
where
at_tv_set = mkVarSet at_tvs
check_arg :: (TyVar, Type) -> TvSubst -> TcM TvSubst
check_arg (fam_tc_tv, at_ty) subst
| Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
= case tcMatchTyX at_tv_set subst at_ty inst_ty of
Just subst | all_distinct subst -> return subst
_ -> failWithTc $ wrongATArgErr at_ty inst_ty
-- No need to instantiate here, becuase the axiom
-- uses the same type variables as the assocated class
| otherwise
= return subst -- Allow non-type-variable instantiation
-- See Note [Associated type instances]
all_distinct :: TvSubst -> Bool
-- True if all the variables mapped the substitution
-- map to *distinct* type *variables*
all_distinct subst = go [] at_tvs
where
go _ [] = True
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 -> False
badATErr :: Name -> Name -> SDoc
badATErr clas op
= hsep [ptext (sLit "Class"), quotes (ppr clas),
ptext (sLit "does not have an associated type"), quotes (ppr op)]
wrongATArgErr :: Type -> Type -> SDoc
wrongATArgErr ty instTy =
sep [ ptext (sLit "Type indexes must match class instance head")
, ptext (sLit "Found") <+> quotes (ppr ty)
<+> ptext (sLit "but expected") <+> quotes (ppr instTy)
]
\end{code}
%************************************************************************
%* *
Checking type instance well-formedness and termination
......@@ -916,18 +1054,24 @@ undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
-- Check that a "type instance" is well-formed (which includes decidability
-- unless -XUndecidableInstances is given).
--
checkValidTyFamInst :: TyCon -> [TyVar] -> [Type] -> Type -> TcM ()
checkValidTyFamInst fam_tc tvs typats rhs
= do { checkValidFamPats fam_tc tvs typats
checkValidTyFamInst :: Maybe ( Class, VarEnv Type )
-> TyCon -> CoAxBranch -> TcM ()
checkValidTyFamInst mb_clsinfo fam_tc
(CoAxBranch { cab_tvs = tvs, cab_lhs = typats
, cab_rhs = rhs, cab_loc = loc })
= setSrcSpan loc $
do { checkValidFamPats fam_tc tvs typats
-- The right-hand side is a tau type
; checkValidMonoType rhs
-- we have a decidable instance unless otherwise permitted
-- We have a decidable instance unless otherwise permitted
; undecidable_ok <- xoptM Opt_UndecidableInstances
; unless undecidable_ok $
mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs))
}
-- Check that type patterns match the class instance head
; checkConsistentFamInst mb_clsinfo fam_tc tvs typats }
-- Make sure that each type family application is
-- (1) strictly smaller than the lhs,
......
......@@ -758,10 +758,11 @@ The "extra" type argument [Char] just stays on the end.
-- It is currently (Oct 2012) used only for generating errors for
-- inaccessible branches. If these errors go unreported, no harm done.
-- This is defined here to avoid a dependency from CoAxiom to Unify
isDominatedBy :: [Type] -> [CoAxBranch] -> Bool
isDominatedBy lhs branches
isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
isDominatedBy branch branches
= or $ map match branches
where
lhs = coAxBranchLHS branch
match (CoAxBranch { cab_tvs = tvs, cab_lhs = tys })
= isJust $ tcMatchTys (mkVarSet tvs) tys lhs
\end{code}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment