Commit 5765248b authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
Browse files

Refactor invariants for FamInsts.

This commit mirrors work done in the commit for ClsInsts, 5efe9b...

Specifically:
- All FamInsts have *fresh* type variables. So, no more freshness work
in addLocalFamInst

Also:
- Some pretty-printing code around FamInsts was cleaned up a bit
This caused location information to be added to CoAxioms and index
information to be added to FamInstBranches.
parent 9d9d09de
......@@ -559,7 +559,8 @@ tc_iface_decl _ _ (IfaceAxiom {ifName = ax_occ, ifTyCon = tc, ifAxBranches = bra
= bindIfaceTyVars tv_bndrs $ \ tvs -> do
{ tc_lhs <- mapM tcIfaceType lhs
; tc_rhs <- tcIfaceType rhs
; let branch = CoAxBranch { cab_tvs = tvs
; let branch = CoAxBranch { cab_loc = noSrcSpan
, cab_tvs = tvs
, cab_lhs = tc_lhs
, cab_rhs = tc_rhs }
; return branch }
......
......@@ -11,7 +11,10 @@ The @FamInst@ type: family instance heads
module FamInst (
checkFamInstConsistency, tcExtendLocalFamInstEnv,
tcLookupFamInst, tcLookupDataFamInst,
tcGetFamInstEnvs
tcGetFamInstEnvs,
freshenFamInstEqn, freshenFamInstEqnLoc,
mkFreshenedSynInst, mkFreshenedSynInstLoc
) where
import HscTypes
......@@ -22,6 +25,7 @@ import TcRnMonad
import TyCon
import CoAxiom
import DynFlags
import SrcLoc
import Module
import Outputable
import UniqFM
......@@ -30,6 +34,7 @@ import Util
import Maybes
import TcMType
import Type
import Name
import Control.Monad
import Data.Map (Map)
import qualified Data.Map as Map
......@@ -264,32 +269,20 @@ addLocalFamInst (home_fie, my_fis) fam_inst
-- my_fies is just the ones from this module
= do { traceTc "addLocalFamInst" (ppr fam_inst)
-- We wish to extend the instance envt with completely
-- fresh template variables. Otherwise, there may be
-- problems when we try to unify the template variables
-- with type family applications.
-- See also addLocalInst in Inst.lhs
; (axBranches', fiBranches')
<- zipWithAndUnzipM mk_skolem_tyvars (fromBranchList $ coAxiomBranches axiom)
(fromBranchList fiBranches)
; let axiom' = axiom { co_ax_branches = toBranchList axBranches' }
fam_inst' = fam_inst { fi_axiom = axiom'
, fi_branches = toBranchList fiBranches' }
; isGHCi <- getIsGHCi
-- In GHCi, we *override* any identical instances
-- that are also defined in the interactive context
; let (home_fie', my_fis')
| isGHCi = ( deleteFromFamInstEnv home_fie fam_inst'
, filterOut (identicalFamInst fam_inst') my_fis)
| isGHCi = ( deleteFromFamInstEnv home_fie fam_inst
, filterOut (identicalFamInst fam_inst) my_fis)
| otherwise = (home_fie, my_fis)
-- Load imported instances, so that we report
-- overlaps correctly
; eps <- getEps
; let inst_envs = (eps_fam_inst_env eps, home_fie')
fam_inst' = toBranchedFamInst fam_inst
home_fie'' = extendFamInstEnv home_fie fam_inst'
-- Check for conflicting instance decls
......@@ -299,44 +292,6 @@ addLocalFamInst (home_fie, my_fis) fam_inst
else
return (home_fie, my_fis) }
where
axiom = famInstAxiom fam_inst
fiBranches = famInstBranches fam_inst
zipWithAndUnzipM :: Monad m
=> (a -> b -> m (c, d))
-> [a]
-> [b]
-> m ([c], [d])
zipWithAndUnzipM f as bs
= do { cds <- zipWithM f as bs
; return $ unzip cds }
mk_skolem_tyvars :: CoAxBranch -> FamInstBranch
-> TcM (CoAxBranch, FamInstBranch)
mk_skolem_tyvars axb fib
= do { (subst, skol_tvs) <- tcInstSkolTyVars (coAxBranchTyVars axb)
; let axb' = coAxBranchSubst axb skol_tvs subst
fib' = famInstBranchSubst fib skol_tvs subst
; return (axb', fib') }
-- substitute the tyvars for a new set of tyvars
coAxBranchSubst :: CoAxBranch -> [TyVar] -> TvSubst -> CoAxBranch
coAxBranchSubst (CoAxBranch { cab_lhs = lhs
, cab_rhs = rhs }) new_tvs subst
= CoAxBranch { cab_tvs = new_tvs
, cab_lhs = substTys subst lhs
, cab_rhs = substTy subst rhs }
-- substitute the current set of tyvars for another
famInstBranchSubst :: FamInstBranch -> [TyVar] -> TvSubst -> FamInstBranch
famInstBranchSubst fib@(FamInstBranch { fib_lhs = lhs
, fib_rhs = rhs }) new_tvs subst
= fib { fib_tvs = new_tvs
, fib_lhs = substTys subst lhs
, fib_rhs = substTy subst rhs }
\end{code}
%************************************************************************
......@@ -368,7 +323,7 @@ conflictInstErr fam_inst branch conflictingMatch
[(fam_inst, branch),
(confInst, famInstNthBranch confInst confIndex)]
| otherwise
= pprPanic "conflictInstErr" (pprFamInstBranch (famInstTyCon fam_inst) branch)
= pprPanic "conflictInstErr" (pprFamInstBranch (famInstAxiom fam_inst) branch)
addFamInstsErr :: SDoc -> [(FamInst Branched, FamInstBranch)] -> TcRn ()
addFamInstsErr herald insts
......@@ -393,3 +348,53 @@ tcGetFamInstEnvs
= do { eps <- getEps; env <- getGblEnv
; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }
\end{code}
%************************************************************************
%* *
Freshening type variables
%* *
%************************************************************************
\begin{code}
-- All type variables in a FamInst/CoAxiom must be fresh. This function
-- creates the fresh variables and applies the necessary substitution
-- It is defined here to avoid a dependency from FamInstEnv on the monad
-- code.
freshenFamInstEqn :: [TyVar] -- original, possibly stale, tyvars
-> [Type] -- LHS patterns
-> Type -- RHS
-> TcM ([TyVar], [Type], Type)
freshenFamInstEqn tvs lhs rhs
= do { loc <- getSrcSpanM
; freshenFamInstEqnLoc loc tvs lhs rhs }
-- freshenFamInstEqn needs to be called outside the TcM monad:
freshenFamInstEqnLoc :: SrcSpan
-> [TyVar] -> [Type] -> Type
-> TcRnIf gbl lcl ([TyVar], [Type], Type)
freshenFamInstEqnLoc loc tvs lhs rhs
= do { (subst, tvs') <- tcInstSkolTyVarsLoc loc tvs
; let lhs' = substTys subst lhs
rhs' = substTy subst rhs
; return (tvs', lhs', rhs') }
-- Makes an unbranched synonym FamInst, with freshened tyvars
mkFreshenedSynInst :: Name -- Unique name for the coercion tycon
-> [TyVar] -- possibly stale tyvars of the coercion
-> TyCon -- Family tycon
-> [Type] -- LHS patterns
-> Type -- RHS
-> TcM (FamInst Unbranched)
mkFreshenedSynInst name tvs fam_tc inst_tys rep_ty
= do { loc <- getSrcSpanM
; mkFreshenedSynInstLoc loc name tvs fam_tc inst_tys rep_ty }
mkFreshenedSynInstLoc :: SrcSpan
-> Name -> [TyVar] -> TyCon -> [Type] -> Type
-> TcRnIf gbl lcl (FamInst Unbranched)
mkFreshenedSynInstLoc loc name tvs fam_tc inst_tys rep_ty
= do { (tvs', inst_tys', rep_ty') <- freshenFamInstEqnLoc loc tvs inst_tys rep_ty
; return $ mkSingleSynFamInst name tvs' fam_tc inst_tys' rep_ty' }
\end{code}
\ No newline at end of file
......@@ -28,7 +28,8 @@ import TcGenDeriv
import DataCon
import TyCon
import CoAxiom
import FamInstEnv ( FamInst, mkSingleSynFamInst )
import FamInstEnv ( FamInst )
import FamInst
import Module ( Module, moduleName, moduleNameString )
import IfaceEnv ( newGlobalBinder )
import Name hiding ( varName )
......@@ -448,7 +449,7 @@ tc_mkRepFamInsts gk tycon metaDts mod =
in newGlobalBinder mod (mkGen (nameOccName (tyConName tycon)))
(nameSrcSpan (tyConName tycon))
; return $ mkSingleSynFamInst rep_name tyvars rep appT repTy
; mkFreshenedSynInst rep_name tyvars rep appT repTy
}
--------------------------------------------------------------------------------
......
......@@ -472,14 +472,14 @@ tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
= setSrcSpan loc $
tcAddTyFamInstCtxt decl $
do { fam_tc <- tcFamInstDeclCombined TopLevel (tyFamInstDeclLName decl)
; fam_inst <- tcTyFamInstDecl fam_tc (L loc decl)
; fam_inst <- tcTyFamInstDecl Nothing fam_tc (L loc decl)
; return ([], [fam_inst]) }
tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
= setSrcSpan loc $
tcAddDataFamInstCtxt decl $
do { fam_tc <- tcFamInstDeclCombined TopLevel (dfid_tycon decl)
; fam_inst <- tcDataFamInstDecl fam_tc decl
; fam_inst <- tcDataFamInstDecl Nothing fam_tc (L loc decl)
; return ([], [toBranchedFamInst fam_inst]) }
tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
......@@ -504,12 +504,9 @@ tcClsInstDecl (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
-- Next, process any associated types.
; traceTc "tcLocalInstDecl" (ppr poly_ty)
; tyfam_insts0 <- tcExtendTyVarEnv tyvars $
mapAndRecoverM tcAssocTyDecl ats
mapAndRecoverM (tcAssocTyDecl clas mini_env) ats
; datafam_insts <- tcExtendTyVarEnv tyvars $
mapAndRecoverM tcAssocDataDecl adts
-- discard the [()]
; _ <- mapAndRecoverM (tcAssocFamInst clas mini_env) (tyfam_insts0 ++ datafam_insts)
mapAndRecoverM (tcAssocDataDecl clas mini_env) adts
-- Check for missing associated types and build them
-- from their defaults (if available)
......@@ -540,7 +537,7 @@ tcClsInstDecl (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
tvs' = varSetElems tv_set'
; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' )
return (mkSingleSynFamInst rep_tc_name tvs' fam_tc pat_tys' rhs') }
mkFreshenedSynInst rep_tc_name tvs' fam_tc pat_tys' rhs' }
; tyfam_insts1 <- mapM mk_deflt_at_instances (classATItems clas)
......@@ -571,6 +568,29 @@ class instance heads, but can contain data constructors and hence they share a
lot of kinding and type checking code with ordinary algebraic data types (and
GADTs).
Note [Associated type consistency check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
According to the invariant stated in FamInstEnv, all FamInsts are created
with *fresh* variables. This is all well and good for matching instances --
when we don't want a spurious variable collision -- but bad for type checking
the instance declarations. Consider this example:
class Cls a where
type Typ a
instance Cls (Maybe b) where
type Typ (Maybe b) = Int
When we're checking the class instance, we build the mini_env [a |-> Maybe b].
Then, we wish to check that the pattern used in the type instance matches.
If we build the FamInst for the associated type instance before doing this
check, the check always fails. This is because the FamInst will be built with
a *fresh* b, which won't be the same as the old, stale b.
Bottom line: we must perform this check before creating the FamInst, even
though it's a little awkward to do so. (The FamInst packages everything
nicely, and we have to push around all pieces independently.)
\begin{code}
tcFamInstDeclCombined :: TopLevelFlag -> Located Name -> TcM TyCon
tcFamInstDeclCombined top_lvl fam_tc_lname
......@@ -590,9 +610,10 @@ tcFamInstDeclCombined top_lvl fam_tc_lname
; return fam_tc }
tcTyFamInstDecl :: TyCon -> LTyFamInstDecl Name -> TcM (FamInst Branched)
tcTyFamInstDecl :: Maybe (Class, VarEnv Type) -- the class & mini_env if applicable
-> TyCon -> LTyFamInstDecl Name -> TcM (FamInst Branched)
-- "type instance"
tcTyFamInstDecl fam_tc (L loc decl@(TyFamInstDecl { tfid_group = group }))
tcTyFamInstDecl mb_clsinfo fam_tc (L loc decl@(TyFamInstDecl { tfid_group = group }))
= do { -- (0) Check it's an open type family
checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
......@@ -603,7 +624,7 @@ tcTyFamInstDecl fam_tc (L loc decl@(TyFamInstDecl { tfid_group = group }))
; quads <- tcSynFamInstDecl fam_tc decl
-- (2) create the branches
; fam_inst_branches <- mapM check_valid_mk_branch quads
; co_ax_branches <- mapM check_valid_mk_branch quads
-- (3) construct coercion tycon
; rep_tc_name <- newFamInstAxiomName loc
......@@ -611,40 +632,49 @@ tcTyFamInstDecl fam_tc (L loc decl@(TyFamInstDecl { tfid_group = group }))
(get_typats quads)
-- (4) check to see if earlier equations dominate a later one
; foldlM_ check_inaccessible_branches [] (map fst fam_inst_branches)
; foldlM_ check_inaccessible_branches [] co_ax_branches
-- now, build the FamInstGroup
; return $ mkSynFamInst rep_tc_name fam_tc group fam_inst_branches }
-- now, build the FamInst
; return $ mkSynFamInst rep_tc_name fam_tc group co_ax_branches }
where
check_valid_mk_branch :: ([TyVar], [Type], Type, SrcSpan)
-> TcM (FamInstBranch, CoAxBranch)
-> TcM CoAxBranch
check_valid_mk_branch (t_tvs, t_typats, t_rhs, loc)
= setSrcSpan loc $
do { -- check the well-formedness of the instance
checkValidTyFamInst fam_tc t_tvs t_typats t_rhs
; return $ mkSynFamInstBranch loc t_tvs t_typats t_rhs }
-- check that type patterns match the class instance head
; tcAssocFamInst mb_clsinfo loc (ptext (sLit "type")) fam_tc t_typats
-- make fresh tyvars for axiom
; (t_tvs', t_typats', t_rhs')
<- freshenFamInstEqn t_tvs t_typats t_rhs
; return $ mkCoAxBranch loc t_tvs' t_typats' t_rhs' }
check_inaccessible_branches :: [FamInstBranch] -- previous
-> FamInstBranch -- current
-> TcM [FamInstBranch] -- current : previous
check_inaccessible_branches :: [CoAxBranch] -- previous
-> CoAxBranch -- current
-> TcM [CoAxBranch] -- current : previous
check_inaccessible_branches prev_branches
cur_branch@(FamInstBranch { fib_lhs = tys })
= setSrcSpan (famInstBranchSpan cur_branch) $
cur_branch@(CoAxBranch { cab_lhs = tys })
= setSrcSpan (coAxBranchSpan cur_branch) $
do { when (tys `isDominatedBy` prev_branches) $
addErrTc $ inaccessibleFamInstBranch fam_tc cur_branch
addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch
; return $ cur_branch : prev_branches }
get_typats = map (\(_, tys, _, _) -> tys)
tcDataFamInstDecl :: TyCon -> DataFamInstDecl Name -> TcM (FamInst Unbranched)
tcDataFamInstDecl :: Maybe (Class, VarEnv Type)
-> TyCon -> LDataFamInstDecl Name -> TcM (FamInst Unbranched)
-- "newtype instance" and "data instance"
tcDataFamInstDecl fam_tc
(DataFamInstDecl { dfid_pats = pats
, dfid_tycon = fam_tc_name
, dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = ctxt, dd_cons = cons } })
tcDataFamInstDecl mb_clsinfo fam_tc
(L loc (DataFamInstDecl
{ dfid_pats = pats
, dfid_tycon = fam_tc_name
, dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = ctxt, dd_cons = cons } }))
= 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)
......@@ -663,6 +693,8 @@ tcDataFamInstDecl fam_tc
; stupid_theta <- tcHsContext ctxt
; h98_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta cons
-- Check that type patterns match class instance head, if any
; tcAssocFamInst mb_clsinfo loc (ppr new_or_data) fam_tc pats'
-- Construct representation tycon
; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
......@@ -676,9 +708,12 @@ tcDataFamInstDecl fam_tc
DataType -> return (mkDataTyConRhs data_cons)
NewType -> ASSERT( not (null data_cons) )
mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
; let fam_inst = mkDataFamInst axiom_name tvs' fam_tc pats' rep_tc
parent = FamInstTyCon (famInstAxiom fam_inst) fam_tc pats'
rep_tc = buildAlgTyCon rep_tc_name tvs' cType stupid_theta tc_rhs
-- freshen tyvars
; (subst, tvs'') <- tcInstSkolTyVars tvs'
; let pats'' = substTys subst pats'
fam_inst = mkDataFamInst axiom_name tvs'' fam_tc pats'' rep_tc
parent = FamInstTyCon (famInstAxiom fam_inst) fam_tc pats''
rep_tc = buildAlgTyCon rep_tc_name tvs'' cType stupid_theta tc_rhs
Recursive h98_syntax parent
-- We always assume that indexed types are recursive. Why?
-- (1) Due to their open nature, we can never be sure that a
......@@ -693,19 +728,22 @@ tcDataFamInstDecl fam_tc
----------------
tcAssocFamInst :: Class -- ^ Class of associated type
-> VarEnv Type -- ^ Instantiation of class TyVars
-> FamInst Unbranched -- ^ RHS
-- See Note [Associated type consistency check]
tcAssocFamInst :: Maybe (Class
, VarEnv Type) -- ^ Class of associated type
-- and instantiation of class TyVars
-> SrcSpan -- ^ Of the family instance
-> SDoc -- ^ "flavor" of the instance
-> TyCon -- ^ Family tycon
-> [Type] -- ^ Type patterns from instance
-> TcM ()
tcAssocFamInst clas mini_env fam_inst
= setSrcSpan (getSrcSpan fam_inst) $
tcAddFamInstCtxt (pprFamFlavor (fi_flavor fam_inst)) (fi_fam fam_inst) $
do { let branch = famInstSingleBranch fam_inst
fam_tc = famInstTyCon fam_inst
at_tys = famInstBranchLHS branch
tcAssocFamInst Nothing _ _ _ _ = return ()
tcAssocFamInst (Just (clas, mini_env)) loc flav fam_tc at_tys
= setSrcSpan loc $
tcAddFamInstCtxt flav (tyConName fam_tc) $
do {
-- Check that the associated type comes from this class
; checkTc (Just clas == tyConAssoc_maybe fam_tc)
checkTc (Just clas == tyConAssoc_maybe fam_tc)
(badATErr (className clas) (tyConName fam_tc))
-- See Note [Checking consistent instantiation] in TcTyClsDecls
......@@ -721,22 +759,26 @@ tcAssocFamInst clas mini_env fam_inst
= return () -- Allow non-type-variable instantiation
-- See Note [Associated type instances]
tcAssocTyDecl :: LTyFamInstDecl Name
tcAssocTyDecl :: Class -- Class of associated type
-> VarEnv Type -- Instantiation of class TyVars
-> LTyFamInstDecl Name
-> TcM (FamInst Unbranched)
tcAssocTyDecl ldecl@(L loc decl)
tcAssocTyDecl clas mini_env ldecl@(L loc decl)
= setSrcSpan loc $
tcAddTyFamInstCtxt decl $
do { fam_tc <- tcFamInstDeclCombined NotTopLevel (tyFamInstDeclLName decl)
; fam_inst <- tcTyFamInstDecl fam_tc ldecl
; fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) fam_tc ldecl
; return $ toUnbranchedFamInst fam_inst }
tcAssocDataDecl :: LDataFamInstDecl Name -- ^ RHS
tcAssocDataDecl :: Class -- ^ Class of associated type
-> VarEnv Type -- ^ Instantiation of class TyVars
-> LDataFamInstDecl Name -- ^ RHS
-> TcM (FamInst Unbranched)
tcAssocDataDecl (L loc decl)
tcAssocDataDecl clas mini_env ldecl@(L loc decl)
= setSrcSpan loc $
tcAddDataFamInstCtxt decl $
do { fam_tc <- tcFamInstDeclCombined NotTopLevel (dfid_tycon decl)
; tcDataFamInstDecl fam_tc decl }
; tcDataFamInstDecl (Just (clas, mini_env)) fam_tc ldecl }
\end{code}
......@@ -1524,10 +1566,10 @@ badFamInstDecl tc_name
quotes (ppr tc_name)
, nest 2 (parens $ ptext (sLit "Use -XTypeFamilies to allow indexed type families")) ]
inaccessibleFamInstBranch :: TyCon -> FamInstBranch -> SDoc
inaccessibleFamInstBranch tc fi
inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
inaccessibleCoAxBranch tc fi
= ptext (sLit "Inaccessible family instance equation:") $$
(pprFamInstBranch tc fi)
(pprCoAxBranch tc fi)
notOpenFamily :: TyCon -> SDoc
notOpenFamily tc
......
......@@ -43,7 +43,7 @@ module TcMType (
-- Instantiation
tcInstTyVars, tcInstSigTyVars, newSigTyVar,
tcInstType,
tcInstSkolTyVars, tcInstSuperSkolTyVars,
tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVars,
tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX,
tcInstSkolTyVar, tcInstSkolType,
tcSkolDFunType, tcSuperSkolTyVars,
......@@ -221,15 +221,15 @@ tcSuperSkolTyVar subst tv
kind = substTy subst (tyVarKind tv)
new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
tcInstSkolTyVar :: Bool -> TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
tcInstSkolTyVar :: SrcSpan -> Bool -> TvSubst -> TyVar
-> TcRnIf gbl lcl (TvSubst, TcTyVar)
-- Instantiate the tyvar, using
-- * the occ-name and kind of the supplied tyvar,
-- * the unique from the monad,
-- * the location either from the tyvar (skol_info = SigSkol)
-- or from the monad (otherwise)
tcInstSkolTyVar overlappable subst tyvar
tcInstSkolTyVar loc overlappable subst tyvar
= do { uniq <- newUnique
; loc <- getSrcSpanM
; let new_name = mkInternalName uniq occ loc
new_tv = mkTcTyVar new_name kind (SkolemTv overlappable)
; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
......@@ -239,6 +239,10 @@ tcInstSkolTyVar overlappable subst tyvar
kind = substTy subst (tyVarKind tyvar)
-- Wrappers
-- we need to be able to do this from outside the TcM monad:
tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
tcInstSkolTyVarsLoc loc = mapAccumLM (tcInstSkolTyVar loc False) (mkTopTvSubst [])
tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVarsX (mkTopTvSubst [])
......@@ -253,7 +257,9 @@ tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
tcInstSkolTyVars' isSuperSkol = mapAccumLM (tcInstSkolTyVar isSuperSkol)
tcInstSkolTyVars' isSuperSkol subst tvs
= do { loc <- getSrcSpanM
; mapAccumLM (tcInstSkolTyVar loc isSuperSkol) subst tvs }
tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type with fresh skolem constants
......
......@@ -16,14 +16,14 @@ module CoAxiom (
brListLength, brListNth, brListMap, brListFoldr,
brListZipWith,
CoAxiom(..), CoAxBranch(..),
CoAxiom(..), CoAxBranch(..), mkCoAxBranch,
toBranchedAxiom, toUnbranchedAxiom,
coAxiomName, coAxiomArity, coAxiomBranches,
coAxiomTyCon, isImplicitCoAxiom,
coAxiomNthBranch, coAxiomSingleBranch_maybe,
coAxiomSingleBranch, coAxBranchTyVars, coAxBranchLHS,
coAxBranchRHS
coAxBranchRHS, coAxBranchSpan
) where
import {-# SOURCE #-} TypeRep ( Type )
......@@ -35,18 +35,13 @@ import Var
import Util
import BasicTypes
import Data.Typeable ( Typeable )
import SrcLoc
import qualified Data.Data as Data
#include "HsVersions.h"
\end{code}
%************************************************************************
%* *
Coercion axioms
%* *
%************************************************************************
Note [Coercion axiom branches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In order to allow type family instance groups, an axiom needs to contain an
......@@ -115,6 +110,13 @@ remain compilable with GHC 7.2.1. If you are revising this code and GHC no
longer needs to remain compatible with GHC 7.2.x, then please update this
code to use promoted types.
%************************************************************************
%* *
Branch lists
%* *
%************************************************************************
\begin{code}
-- the phantom type labels
......@@ -177,7 +179,15 @@ brListZipWith f (NextBranch a ta) (NextBranch b tb) = f a b : brListZipWith f ta
instance Outputable a => Outputable (BranchList a br) where
ppr = ppr . fromBranchList
\end{code}
%************************************************************************
%* *
Coercion axioms
%* *
%************************************************************************
\begin{code}
-- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom.
-- If you edit this type, you may need to update the GHC formalism
......@@ -197,7 +207,8 @@ data CoAxiom br
data CoAxBranch
= CoAxBranch
{ cab_tvs :: [TyVar] -- bound type variables
{ cab_loc :: SrcSpan -- location of the defining equation
, cab_tvs :: [TyVar] -- bound type variables
, cab_lhs :: [Type] -- type patterns to match against
, cab_rhs :: Type -- right-hand side of the equality
}
......@@ -248,8 +259,16 @@ coAxBranchLHS = cab_lhs
coAxBranchRHS :: CoAxBranch -> Type
coAxBranchRHS = cab_rhs
coAxBranchSpan :: CoAxBranch -> SrcSpan
coAxBranchSpan = cab_loc
isImplicitCoAxiom :: CoAxiom br -> Bool
isImplicitCoAxiom = co_ax_implicit
-- The tyvars must be *fresh*. This CoAxBranch will be put into a
-- FamInst. See Note [Template tyvars are fresh] in InstEnv
mkCoAxBranch :: SrcSpan -> [TyVar] -> [Type] -> Type -> CoAxBranch
mkCoAxBranch = CoAxBranch
\end{code}
Note [Implicit axioms]
......@@ -289,4 +308,5 @@ instance Typeable br => Data.Data (CoAxiom br) where
toConstr _ = abstractConstr "CoAxiom"
gunfold _ _ = error "gunfold"
dataTypeOf _ = mkNoRepType "CoAxiom"
\end{code}
\ No newline at end of file
\end{code}
......@@ -87,7 +87,7 @@ import Var
import VarEnv
import VarSet
import Maybes ( orElse )
import Name ( Name, NamedThing(..), nameUnique )
import Name ( Name, NamedThing(..), nameUnique, getSrcSpan )
import OccName ( parenSymOcc )
import Util
import BasicTypes
......@@ -705,7 +705,8 @@ mkNewTypeCo name tycon tvs rhs_ty
, co_ax_implicit = True -- See Note [Implicit axioms] in TyCon
, co_ax_tc = tycon
, co_ax_branches = FirstBranch branch }
where branch = CoAxBranch { cab_tvs = tvs
where branch = CoAxBranch { cab_loc = getSrcSpan name
, cab_tvs = tvs
, cab_lhs = mkTyVarTys tvs
, cab_rhs = rhs_ty }
......
......@@ -14,9 +14,9 @@ module FamInstEnv (
famInstBranchLHS, famInstBranches, famInstBranchSpan,
toBranchedFamInst, toUnbranchedFamInst,
famInstTyCon, famInstRepTyCon_maybe, dataFamInstRepTyCon,
pprFamInst, pprFamInsts, pprFamInstBranch, pprFamInstBranches,
pprFamFlavor, pprFamInstBranchHdr,
mkSynFamInst, mkSynFamInstBranch, mkSingleSynFamInst,
pprFamInst, pprFamInsts, pprFamInstBranch,
pprFamFlavor, pprFamInstBranchHdr, pprCoAxBranch,
mkSynFamInst, mkSingleSynFamInst,
mkDataFamInst, mkImportedFamInst,
FamInstEnv, FamInstEnvs,
......@@ -107,8 +107,35 @@ assumes that it is part of a consistent axiom set.
A "group" with fi_group=True can have just one element, however.
Note [Why we need fib_rhs]
~~~~~~~~~~~~~~~~~~~~~~~~~~