module FamInst (
FamInstEnvs, tcGetFamInstEnvs,
checkFamInstConsistency, tcExtendLocalFamInstEnv,
tcLookupDataFamInst, tcLookupDataFamInst_maybe,
tcInstNewTyCon_maybe, tcTopNormaliseNewTypeTF_maybe,
newFamInst,
makeInjectivityErrors
) where
import HscTypes
import FamInstEnv
import InstEnv( roughMatchTcs )
import Coercion
import TcEvidence
import LoadIface
import TcRnMonad
import SrcLoc
import TyCon
import TcType
import CoAxiom
import DynFlags
import Module
import Outputable
import UniqFM
import Util
import RdrName
import DataCon ( dataConName )
import Maybes
import Type
import TyCoRep
import TcMType
import Name
import Pair
import Panic
import VarSet
import Control.Monad
import Data.Map (Map)
import qualified Data.Map as Map
#if __GLASGOW_HASKELL__ < 709
import Prelude hiding ( and )
import Data.Foldable ( and )
#endif
#include "HsVersions.h"
newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
= ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
ASSERT2( tyCoVarsOfType rhs `subVarSet` tcv_set, text "rhs" <+> pp_ax )
ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
do { (subst, tvs') <- freshenTyVarBndrs tvs
; (subst, cvs') <- freshenCoVarBndrsX subst cvs
; return (FamInst { fi_fam = tyConName fam_tc
, fi_flavor = flavor
, fi_tcs = roughMatchTcs lhs
, fi_tvs = tvs'
, fi_cvs = cvs'
, fi_tys = substTys subst lhs
, fi_rhs = substTy subst rhs
, fi_axiom = axiom }) }
where
lhs_kind = typeKind (mkTyConApp fam_tc lhs)
rhs_kind = typeKind rhs
tcv_set = mkVarSet (tvs ++ cvs)
pp_ax = pprCoAxiom axiom
CoAxBranch { cab_tvs = tvs
, cab_cvs = cvs
, cab_lhs = lhs
, cab_rhs = rhs } = coAxiomSingleBranch axiom
data ModulePair = ModulePair Module Module
canon :: ModulePair -> (Module, Module)
canon (ModulePair m1 m2) | m1 < m2 = (m1, m2)
| otherwise = (m2, m1)
instance Eq ModulePair where
mp1 == mp2 = canon mp1 == canon mp2
instance Ord ModulePair where
mp1 `compare` mp2 = canon mp1 `compare` canon mp2
instance Outputable ModulePair where
ppr (ModulePair m1 m2) = angleBrackets (ppr m1 <> comma <+> ppr m2)
type ModulePairSet = Map ModulePair ()
listToSet :: [ModulePair] -> ModulePairSet
listToSet l = Map.fromList (zip l (repeat ()))
checkFamInstConsistency :: [Module] -> [Module] -> TcM ()
checkFamInstConsistency famInstMods directlyImpMods
= do { dflags <- getDynFlags
; (eps, hpt) <- getEpsAndHpt
; let {
modIface mod =
case lookupIfaceByModule dflags hpt (eps_PIT eps) mod of
Nothing -> panicDoc "FamInst.checkFamInstConsistency"
(ppr mod $$ pprHPT hpt)
Just iface -> iface
; hmiModule = mi_module . hm_iface
; hmiFamInstEnv = extendFamInstEnvList emptyFamInstEnv
. md_fam_insts . hm_details
; hpt_fam_insts = mkModuleEnv [ (hmiModule hmi, hmiFamInstEnv hmi)
| hmi <- eltsUFM hpt]
; groups = map (dep_finsts . mi_deps . modIface)
directlyImpMods
; okPairs = listToSet $ concatMap allPairs groups
; criticalPairs = listToSet $ allPairs famInstMods
; toCheckPairs = Map.keys $ criticalPairs `Map.difference` okPairs
}
; mapM_ (check hpt_fam_insts) toCheckPairs
}
where
allPairs [] = []
allPairs (m:ms) = map (ModulePair m) ms ++ allPairs ms
check hpt_fam_insts (ModulePair m1 m2)
= do { env1 <- getFamInsts hpt_fam_insts m1
; env2 <- getFamInsts hpt_fam_insts m2
; mapM_ (checkForConflicts (emptyFamInstEnv, env2))
(famInstEnvElts env1)
; mapM_ (checkForInjectivityConflicts (emptyFamInstEnv,env2))
(famInstEnvElts env1)
}
getFamInsts :: ModuleEnv FamInstEnv -> Module -> TcM FamInstEnv
getFamInsts hpt_fam_insts mod
| Just env <- lookupModuleEnv hpt_fam_insts mod = return env
| otherwise = do { _ <- initIfaceTcRn (loadSysInterface doc mod)
; eps <- getEps
; return (expectJust "checkFamInstConsistency" $
lookupModuleEnv (eps_mod_fam_inst_env eps) mod) }
where
doc = ppr mod <+> text "is a family-instance module"
tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
tcInstNewTyCon_maybe = instNewTyCon_maybe
tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
-> (TyCon, [TcType], Coercion)
tcLookupDataFamInst fam_inst_envs tc tc_args
| Just (rep_tc, rep_args, co)
<- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
= (rep_tc, rep_args, co)
| otherwise
= (tc, tc_args, mkRepReflCo (mkTyConApp tc tc_args))
tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
-> Maybe (TyCon, [TcType], Coercion)
tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
| isDataFamilyTyCon tc
, match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args
, FamInstMatch { fim_instance = rep_fam@(FamInst { fi_axiom = ax
, fi_cvs = cvs })
, fim_tys = rep_args
, fim_cos = rep_cos } <- match
, let rep_tc = dataFamInstRepTyCon rep_fam
co = mkUnbranchedAxInstCo Representational ax rep_args
(mkCoVarCos cvs)
= ASSERT( null rep_cos )
Just (rep_tc, rep_args, co)
| otherwise
= Nothing
tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
-> GlobalRdrEnv
-> Type
-> Maybe (TcCoercion, Type)
tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
= topNormaliseTypeX_maybe stepper ty
where
stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance
unwrap_newtype_instance rec_nts tc tys
| Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys
= modifyStepResultCo (co `mkTransCo`) $
unwrap_newtype rec_nts tc' tys'
| otherwise = NS_Done
unwrap_newtype rec_nts tc tys
| data_cons_in_scope tc
= unwrapNewTypeStepper rec_nts tc tys
| otherwise
= NS_Done
data_cons_in_scope :: TyCon -> Bool
data_cons_in_scope tc
= isWiredInName (tyConName tc) ||
(not (isAbstractTyCon tc) && all in_scope data_con_names)
where
data_con_names = map dataConName (tyConDataCons tc)
in_scope dc = not $ null $ lookupGRE_Name rdr_env dc
tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
tcExtendLocalFamInstEnv fam_insts thing_inside
= do { env <- getGblEnv
; (inst_env', fam_insts') <- foldlM addLocalFamInst
(tcg_fam_inst_env env, tcg_fam_insts env)
fam_insts
; let env' = env { tcg_fam_insts = fam_insts'
, tcg_fam_inst_env = inst_env' }
; setGblEnv env' thing_inside
}
addLocalFamInst :: (FamInstEnv,[FamInst])
-> FamInst
-> TcM (FamInstEnv, [FamInst])
addLocalFamInst (home_fie, my_fis) fam_inst
= do { traceTc "addLocalFamInst" (ppr fam_inst)
; isGHCi <- getIsGHCi
; mod <- getModule
; traceTc "alfi" (ppr mod $$ ppr isGHCi)
; let home_fie'
| isGHCi = deleteFromFamInstEnv home_fie fam_inst
| otherwise = home_fie
; eps <- getEps
; let inst_envs = (eps_fam_inst_env eps, home_fie')
home_fie'' = extendFamInstEnv home_fie fam_inst
; no_conflict <- checkForConflicts inst_envs fam_inst
; injectivity_ok <- checkForInjectivityConflicts inst_envs fam_inst
; if no_conflict && injectivity_ok then
return (home_fie'', fam_inst : my_fis)
else
return (home_fie, my_fis) }
checkForConflicts :: FamInstEnvs -> FamInst -> TcM Bool
checkForConflicts inst_envs fam_inst
= do { let conflicts = lookupFamInstEnvConflicts inst_envs fam_inst
no_conflicts = null conflicts
; traceTc "checkForConflicts" $
vcat [ ppr (map fim_instance conflicts)
, ppr fam_inst
]
; unless no_conflicts $ conflictInstErr fam_inst conflicts
; return no_conflicts }
checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM Bool
checkForInjectivityConflicts instEnvs famInst
| isTypeFamilyTyCon tycon
, Injective inj <- familyTyConInjectivityInfo tycon = do
{ let axiom = coAxiomSingleBranch fi_ax
conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst
errs = makeInjectivityErrors fi_ax axiom inj conflicts
; mapM_ (\(err, span) -> setSrcSpan span $ addErr err) errs
; return (null errs)
}
| otherwise = return True
where tycon = famInstTyCon famInst
fi_ax = fi_axiom famInst
makeInjectivityErrors
:: CoAxiom br
-> CoAxBranch
-> [Bool]
-> [CoAxBranch]
-> [(SDoc, SrcSpan)]
makeInjectivityErrors fi_ax axiom inj conflicts
= ASSERT2( any id inj, text "No injective type variables" )
let lhs = coAxBranchLHS axiom
rhs = coAxBranchRHS axiom
are_conflicts = not $ null conflicts
unused_inj_tvs = unusedInjTvsInRHS (coAxiomTyCon fi_ax) inj lhs rhs
inj_tvs_unused = not $ and (isEmptyVarSet <$> unused_inj_tvs)
tf_headed = isTFHeaded rhs
bare_variables = bareTvInRHSViolated lhs rhs
wrong_bare_rhs = not $ null bare_variables
err_builder herald eqns
= ( hang herald
2 (vcat (map (pprCoAxBranch fi_ax) eqns))
, coAxBranchSpan (head eqns) )
errorIf p f = if p then [f err_builder axiom] else []
in errorIf are_conflicts (conflictInjInstErr conflicts )
++ errorIf inj_tvs_unused (unusedInjectiveVarsErr unused_inj_tvs)
++ errorIf tf_headed tfHeadedErr
++ errorIf wrong_bare_rhs (bareVariableInRHSErr bare_variables)
unusedInjTvsInRHS :: TyCon -> [Bool] -> [Type] -> Type -> Pair TyVarSet
unusedInjTvsInRHS tycon injList lhs rhs =
(`minusVarSet` injRhsVars) <$> injLHSVars
where
(invis_pairs, vis_pairs)
= partitionInvisibles tycon snd (zipEqual "unusedInjTvsInRHS" injList lhs)
invis_lhs = uncurry filterByList $ unzip invis_pairs
vis_lhs = uncurry filterByList $ unzip vis_pairs
invis_vars = tyCoVarsOfTypes invis_lhs
Pair invis_vars' vis_vars = splitVisVarsOfTypes vis_lhs
injLHSVars
= Pair (invis_vars `minusVarSet` vis_vars `unionVarSet` invis_vars')
vis_vars
injRhsVars = collectInjVars rhs
collectInjVars :: Type -> VarSet
collectInjVars (TyVarTy v)
= unitVarSet v `unionVarSet` collectInjVars (tyVarKind v)
collectInjVars (TyConApp tc tys)
| isTypeFamilyTyCon tc = collectInjTFVars tys
(familyTyConInjectivityInfo tc)
| otherwise = mapUnionVarSet collectInjVars tys
collectInjVars (LitTy {})
= emptyVarSet
collectInjVars (ForAllTy (Anon arg) res)
= collectInjVars arg `unionVarSet` collectInjVars res
collectInjVars (AppTy fun arg)
= collectInjVars fun `unionVarSet` collectInjVars arg
collectInjVars (ForAllTy _ _) =
panic "unusedInjTvsInRHS.collectInjVars"
collectInjVars (CastTy ty _) = collectInjVars ty
collectInjVars (CoercionTy {}) = emptyVarSet
collectInjTFVars :: [Type] -> Injectivity -> VarSet
collectInjTFVars _ NotInjective
= emptyVarSet
collectInjTFVars tys (Injective injList)
= mapUnionVarSet collectInjVars (filterByList injList tys)
isTFHeaded :: Type -> Bool
isTFHeaded ty | Just ty' <- coreView ty
= isTFHeaded ty'
isTFHeaded ty | (TyConApp tc args) <- ty
, isTypeFamilyTyCon tc
= tyConArity tc == length args
isTFHeaded _ = False
bareTvInRHSViolated :: [Type] -> Type -> [Type]
bareTvInRHSViolated pats rhs | isTyVarTy rhs
= filter (not . isTyVarTy) pats
bareTvInRHSViolated _ _ = []
conflictInstErr :: FamInst -> [FamInstMatch] -> TcRn ()
conflictInstErr fam_inst conflictingMatch
| (FamInstMatch { fim_instance = confInst }) : _ <- conflictingMatch
= let (err, span) = makeFamInstsErr
(text "Conflicting family instance declarations:")
[fam_inst, confInst]
in setSrcSpan span $ addErr err
| otherwise
= panic "conflictInstErr"
type InjErrorBuilder = SDoc -> [CoAxBranch] -> (SDoc, SrcSpan)
injectivityErrorHerald :: Bool -> SDoc
injectivityErrorHerald isSingular =
text "Type family equation" <> s isSingular <+> text "violate" <>
s (not isSingular) <+> text "injectivity annotation" <>
if isSingular then dot else colon
where
s False = text "s"
s True = empty
conflictInjInstErr :: [CoAxBranch] -> InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
| confEqn : _ <- conflictingEqns
= errorBuilder (injectivityErrorHerald False) [confEqn, tyfamEqn]
| otherwise
= panic "conflictInjInstErr"
unusedInjectiveVarsErr :: Pair TyVarSet -> InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
= errorBuilder (injectivityErrorHerald True $$ msg)
[tyfamEqn]
where
tvs = varSetElemsWellScoped (invis_vars `unionVarSet` vis_vars)
has_types = not $ isEmptyVarSet vis_vars
has_kinds = not $ isEmptyVarSet invis_vars
doc = sep [ what <+> text "variable" <>
plural tvs <+> pprQuotedList tvs
, text "cannot be inferred from the right-hand side." ]
what = case (has_types, has_kinds) of
(True, True) -> text "Type and kind"
(True, False) -> text "Type"
(False, True) -> text "Kind"
(False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $ ppr tvs
print_kinds_info = sdocWithDynFlags $ \ dflags ->
if has_kinds && not (gopt Opt_PrintExplicitKinds dflags)
then text "(enabling -fprint-explicit-kinds might help)"
else empty
msg = doc $$ print_kinds_info $$
text "In the type family equation:"
tfHeadedErr :: InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
tfHeadedErr errorBuilder famInst
= errorBuilder (injectivityErrorHerald True $$
text "RHS of injective type family equation cannot" <+>
text "be a type family:") [famInst]
bareVariableInRHSErr :: [Type] -> InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
bareVariableInRHSErr tys errorBuilder famInst
= errorBuilder (injectivityErrorHerald True $$
text "RHS of injective type family equation is a bare" <+>
text "type variable" $$
text "but these LHS type and kind patterns are not bare" <+>
text "variables:" <+> pprQuotedList tys) [famInst]
makeFamInstsErr :: SDoc -> [FamInst] -> (SDoc, SrcSpan)
makeFamInstsErr herald insts
= ASSERT( not (null insts) )
( hang herald
2 (vcat [ pprCoAxBranchHdr (famInstAxiom fi) 0
| fi <- sorted ])
, srcSpan )
where
getSpan = getSrcLoc . famInstAxiom
sorted = sortWith getSpan insts
fi1 = head sorted
srcSpan = coAxBranchSpan (coAxiomSingleBranch (famInstAxiom fi1))
tcGetFamInstEnvs :: TcM FamInstEnvs
tcGetFamInstEnvs
= do { eps <- getEps; env <- getGblEnv
; return (eps_fam_inst_env eps, tcg_fam_inst_env env) }