\begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
--- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
-module TcTyFuns(
+module TcTyFuns (
tcNormalizeFamInst,
normaliseGivens, normaliseGivenDicts,
import TcRnMonad
import TcEnv
import Inst
-import FamInstEnv
import TcType
import TcMType
import Coercion
import TypeRep ( Type(..) )
import TyCon
-import Var ( mkCoVar, isTcTyVar )
+import Var ( isTcTyVar )
import Type
-import HscTypes ( ExternalPackageState(..) )
import Bag
import Outputable
import SrcLoc ( Located(..) )
| not (isOpenSynTyCon tycon) -- unfold *only* _synonym_ family instances
= return Nothing
| otherwise
- = do { maybeFamInst <- tcLookupFamInst tycon tys
+ = do { -- we only use the indexing arguments for matching,
+ -- not the additional ones
+ ; maybeFamInst <- tcLookupFamInst tycon idxTys
; case maybeFamInst of
Nothing -> return Nothing
- Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc rep_tys,
- mkTyConApp coe_tc rep_tys)
+ Just (rep_tc, rep_tys) -> return $ Just (mkTyConApp rep_tc tys',
+ mkTyConApp coe_tc tys')
where
+ tys' = rep_tys ++ restTys
coe_tc = expectJust "TcTyFun.tcUnfoldSynFamInst"
(tyConFamilyCoercion_maybe rep_tc)
}
+ where
+ n = tyConArity tycon
+ (idxTys, restTys) = splitAt n tys
tcUnfoldSynFamInst _other = return Nothing
\end{code}
then co : ty ~ ty'
\begin{code}
-tcNormalizeFamInst :: Type -> TcM (CoercionI, Type)
+tcNormalizeFamInst :: TcType -> TcM (CoercionI, TcType)
tcNormalizeFamInst = tcGenericNormalizeFamInst tcUnfoldSynFamInst
tcNormalizeFamInstPred :: TcPredType -> TcM (CoercionI, TcPredType)
tcNormalizeFamInstPred = tcGenericNormalizeFamInstPred tcUnfoldSynFamInst
\end{code}
+Normalise a type relative to the rewrite rule implied by one EqInst.
+
+\begin{code}
+tcEqInstNormalizeFamInst :: Inst -> TcType -> TcM (CoercionI, Type)
+tcEqInstNormalizeFamInst inst = ASSERT( isEqInst inst )
+ tcGenericNormalizeFamInst matchInst
+ where
+ pat = eqInstLeftTy inst
+ rhs = eqInstRightTy inst
+ co = eitherEqInst inst TyVarTy id
+ --
+ matchInst ty | pat `tcEqType` ty = return $ Just (rhs, co)
+ | otherwise = return $ Nothing
+\end{code}
+
Generic normalisation of 'Type's and 'PredType's; ie, walk the type term and
apply the normalisation function gives as the first argument to every TyConApp
and every TyVarTy subterm.
good error messages, callers should discard ty' in favour of ty in this case.
\begin{code}
-tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType,Coercion)))
+tcGenericNormalizeFamInst :: (TcType -> TcM (Maybe (TcType, Coercion)))
-- what to do with type functions and tyvars
-> TcType -- old type
- -> TcM (CoercionI, Type) -- (coercion, new type)
+ -> TcM (CoercionI, TcType) -- (coercion, new type)
tcGenericNormalizeFamInst fun ty
| Just ty' <- tcView ty = tcGenericNormalizeFamInst fun ty'
-tcGenericNormalizeFamInst fun ty@(TyConApp tyCon tys)
+tcGenericNormalizeFamInst fun (TyConApp tyCon tys)
= do { (cois, ntys) <- mapAndUnzipM (tcGenericNormalizeFamInst fun) tys
; let tycon_coi = mkTyConAppCoI tyCon ntys cois
; maybe_ty_co <- fun (TyConApp tyCon ntys) -- use normalised args!
-- we do not do anything
Nothing -> return (tycon_coi, TyConApp tyCon ntys)
}
-tcGenericNormalizeFamInst fun ty@(AppTy ty1 ty2)
+tcGenericNormalizeFamInst fun (AppTy ty1 ty2)
= do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
; return (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
}
-tcGenericNormalizeFamInst fun ty@(FunTy ty1 ty2)
+tcGenericNormalizeFamInst fun (FunTy ty1 ty2)
= do { (coi1,nty1) <- tcGenericNormalizeFamInst fun ty1
; (coi2,nty2) <- tcGenericNormalizeFamInst fun ty2
; return (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
}
-tcGenericNormalizeFamInst fun ty@(ForAllTy tyvar ty1)
+tcGenericNormalizeFamInst fun (ForAllTy tyvar ty1)
= do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
; return (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
}
-tcGenericNormalizeFamInst fun ty@(NoteTy note ty1)
+tcGenericNormalizeFamInst fun (NoteTy note ty1)
= do { (coi,nty1) <- tcGenericNormalizeFamInst fun ty1
; return (mkNoteTyCoI note coi,NoteTy note nty1)
}
; traceTc (text "normaliseGivens ->" <+> ppr result)
; return (result, deSkolem)
}
+\end{code}
--- An explanation of what this does would be helpful! -=chak
+
+This is an (attempt at, yet unproven, an) *unflattened* version of
+the SubstL-Ev completion rule.
+
+The above rule is essential to catch non-terminating
+rules that cannot be oriented properly, like
+
+ F a ~ [G (F a)]
+ or even
+ a ~ [G a]
+
+The left-to-right orientiation is not suitable because it does not
+terminate.
+The right-to-left orientation is not suitable because it
+does not have a type-function on the left. This is undesirable because
+it would hide information. E.g. assume
+ instance C [x]
+then rewriting C [G (F a)] to C (F a) is bad because we cannot now
+see that the C [x] instance applies.
+
+The rule also caters for badly-oriented rules of the form:
+ F a ~ G (F a)
+for which other solutions are possible, but this one will do too.
+
+It's behavior is:
+ co : ty1 ~ ty2{F ty1}
+ >-->
+ co : ty1 ~ ty2{b}
+ sym (F co) : F ty2{b} ~ b
+ where b is a fresh skolem variable
+
+We also return an action (b := ty1) which is used to eliminate b
+after the dust of normalisation with the completed rewrite system
+has settled.
+
+A subtle point of this transformation is that both coercions in the results
+are strictly speaking incorrect. However, they are correct again after the
+action {B := ty1} has removed the skolem again. This happens immediately
+after constraint entailment has been checked; ie, code outside of the
+simplification and entailment checking framework will never see these
+temporarily incorrect coercions.
+
+NB: We perform this transformation for multiple occurences of ty1 under one
+ or multiple family applications on the left-hand side at once (ie, the
+ rule doesn't need to be applied multiple times at a single inst). As a
+ result we can get two or more insts back.
+
+\begin{code}
skolemOccurs :: PrecondRule
-skolemOccurs [] = return ([], return ())
-skolemOccurs (inst@(EqInst {}):insts)
- = do { (insts',actions) <- skolemOccurs insts
- -- check whether the current inst co :: ty1 ~ ty2 suffers
- -- from the occurs check issue: F ty1 \in ty2
- ; let occurs = go False ty2
- ; if occurs
- then
- -- if it does generate two new coercions:
- do { skolem_var <- newMetaTyVar TauTv (typeKind ty1)
- ; let skolem_ty = TyVarTy skolem_var
- -- ty1 :: ty1 ~ b
- ; inst1 <- mkEqInst (EqPred ty1 skolem_ty) (mkGivenCo ty1)
- -- sym co :: ty2 ~ b
- ; inst2 <- mkEqInst (EqPred ty2 skolem_ty) (mkGivenCo $ fromACo $ mkSymCoI $ ACo $ fromGivenCo co)
- -- to replace the old one
- -- the corresponding action is
- -- b := ty1
- ; let action = writeMetaTyVar skolem_var ty1
- ; return (inst1:inst2:insts', action >> actions)
- }
- else
- return (inst:insts', actions)
- }
- where
- ty1 = eqInstLeftTy inst
- ty2 = eqInstRightTy inst
- co = eqInstCoercion inst
- check :: Bool -> TcType -> Bool
- check flag ty
- = if flag && ty1 `tcEqType` ty
- then True
- else go flag ty
-
- go flag (TyConApp con tys) = or $ map (check (isOpenSynTyCon con || flag)) tys
- go flag (FunTy arg res) = or $ map (check flag) [arg,res]
- go flag (AppTy fun arg) = or $ map (check flag) [fun,arg]
- go flag ty = False
+skolemOccurs insts
+ = do { (instss, undoSkolems) <- mapAndUnzipM oneSkolemOccurs insts
+ ; return (concat instss, sequence_ undoSkolems)
+ }
+ where
+ oneSkolemOccurs inst
+ | null tysToLiftOut
+ = return ([inst], return ())
+ | otherwise
+ = do { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
+ ; let skTvs_tysTLO = zip skTvs tysToLiftOut
+ insertSkolems = return . replace skTvs_tysTLO
+ ; (_, ty2') <- tcGenericNormalizeFamInst insertSkolems ty2
+ ; inst' <- mkEqInst (EqPred ty1 ty2') co
+ ; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst') skTvs_tysTLO
+ ; return (inst':insts, sequence_ undoSk)
+ }
+ where
+ ty1 = eqInstLeftTy inst
+ ty2 = eqInstRightTy inst
+ co = eqInstCoercion inst
+
+ -- all subtypes that are (1) type family instances and (2) contain the
+ -- lhs type as part of the type arguments of the type family constructor
+ tysToLiftOut = ASSERT( isEqInst inst )
+ [mkTyConApp tc tys | (tc, tys) <- tyFamInsts ty2
+ , any (ty1 `tcPartOfType`) tys]
+
+ replace :: [(TcTyVar, Type)] -> Type -> Maybe (Type, Coercion)
+ replace [] _ = Nothing
+ replace ((skTv, tyTLO):rest) ty
+ | tyTLO `tcEqType` ty = Just (mkTyVarTy skTv, undefined)
+ | otherwise = replace rest ty
+
+ -- create the EqInst for the equality determining the skolem and a
+ -- TcM action undoing the skolem introduction
+ mkSkolemInst inst' (skTv, tyTLO)
+ = do { (co, tyLiftedOut) <- tcEqInstNormalizeFamInst inst' tyTLO
+ ; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
+ (mkGivenCo $ mkSymCoercion (fromACo co))
+ ; return (inst, writeMetaTyVar skTv tyTLO)
+ }
\end{code}
completeRewrite dePrecond (Just (precondName, precond)) insts
= do { (insts', dePrecond') <- precond insts
; traceTc $ text precondName <+> ppr insts'
- ; tryRules dePrecond rules insts'
+ ; tryRules (dePrecond >> dePrecond') rules insts'
}
completeRewrite dePrecond Nothing insts
= tryRules dePrecond rules insts
-- >-->
-- g1 := t
--
-trivialInsts ::
- [Inst] -> -- equations
- TcM ([Inst],Bool) -- remaining equations, any changes?
+trivialInsts :: RewriteRule
trivialInsts []
= return ([],False)
trivialInsts (i@(EqInst {}):is)
where
ty1 = eqInstLeftTy i
ty2 = eqInstRightTy i
+trivialInsts _ = panic "TcTyFuns.trivialInsts: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-swapInsts :: [Inst] -> TcM ([Inst],Bool)
+swapInsts :: RewriteRule
-- All the inputs and outputs are equalities
swapInsts insts
= do { (insts', changeds) <- mapAndUnzipM swapInst insts
}
-- (Swap)
- -- g1 : c ~ Fd
+ -- g1 : c ~ F d
-- >-->
- -- g2 : Fd ~ c
+ -- g2 : F d ~ c
-- g1 := sym g2
+ -- where c isn't a function call
+ -- and
--
- -- This is not all, is it? Td ~ c is also rewritten to c ~ Td!
+ -- g1 : c ~ a
+ -- >-->
+ -- g2 : a ~ c
+ -- g1 := sym g2
+ -- where c isn't a function call or other variable
+swapInst :: Inst -> TcM (Inst, Bool)
swapInst i@(EqInst {})
= go ty1 ty2
where
; new_inst <- mkEqInst (EqPred ty2 ty1) wg_co
; return (new_inst,True)
}
+swapInst _ = panic "TcTyFuns.swapInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-decompInsts :: [Inst] -> TcM ([Inst],Bool)
+decompInsts :: RewriteRule
decompInsts insts = do { (insts,bs) <- mapAndUnzipM decompInst insts
; return (concat insts,or bs)
}
; failWithTcM (env2, hang msg 2 extra)
}
where
- n = tyConArity con1
- (idxTys1, tys1') = splitAt n tys1
- (idxTys2, tys2') = splitAt n tys2
- identicalHead = not (isOpenSynTyCon con1) ||
- idxTys1 `tcEqTypes` idxTys2
+ n = tyConArity con1
+ (idxTys1, _) = splitAt n tys1
+ (idxTys2, _) = splitAt n tys2
+ identicalHead = not (isOpenSynTyCon con1) ||
+ idxTys1 `tcEqTypes` idxTys2
go _ _ = return ([i], False)
+decompInst _ = panic "TcTyFuns.decompInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-topInsts :: [Inst] -> TcM ([Inst],Bool)
+topInsts :: RewriteRule
topInsts insts
= do { (insts,bs) <- mapAndUnzipM topInst insts
; return (insts,or bs)
where
ty1 = eqInstLeftTy i
ty2 = eqInstRightTy i
+topInst _ = panic "TcTyFuns.topInsts: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-substInsts :: [Inst] -> TcM ([Inst],Bool)
+substInsts :: RewriteRule
substInsts insts = substInstsWorker insts []
+substInstsWorker :: [Inst] -> [Inst] -> TcM ([Inst],Bool)
substInstsWorker [] acc
= return (acc,False)
substInstsWorker (i:is) acc
then return ((i:is'),True)
else substInstsWorker is (i:acc)
}
+ | (TyVarTy _) <- tci_left i
+ = do { (is',change) <- substInst i (acc ++ is)
+ ; if change
+ then return ((i:is'),True)
+ else substInstsWorker is (i:acc)
+ }
| otherwise
= substInstsWorker is (i:acc)
-- >-->
-- g2 : s1{t} ~ s2{t}
-- g1 := s1{g} * g2 * sym s2{g} <=> g2 := sym s1{g} * g1 * s2{g}
-substInst inst []
- = return ([],False)
-substInst inst@(EqInst {tci_left = pattern, tci_right = target}) (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
+substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
+substInst _inst [] = return ([],False)
+substInst inst (i@(EqInst {tci_left = ty1, tci_right = ty2}):is)
= do { (is',changed) <- substInst inst is
- ; (coi1,ty1') <- tcGenericNormalizeFamInst fun ty1
- ; (coi2,ty2') <- tcGenericNormalizeFamInst fun ty2
+ ; (coi1,ty1') <- normalise ty1
+ ; (coi2,ty2') <- normalise ty2
; case (coi1,coi2) of
(IdCo,IdCo) ->
return (i:is',changed)
; return (new_inst:is',True)
}
}
- where fun ty = return $ if tcEqType pattern ty then Just (target,coercion) else Nothing
+ where
+ normalise = tcEqInstNormalizeFamInst inst
+substInst _ _ = panic "TcTyFuns.substInst: not EqInst"
- coercion = eitherEqInst inst TyVarTy id
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-unifyInsts
- :: [Inst] -- wanted equations
- -> TcM ([Inst],Bool)
+unifyInsts :: RewriteRule
unifyInsts insts
= do { (insts',changeds) <- mapAndUnzipM unifyInst insts
; return (concat insts',or changeds)
-- g := t
--
-- TOMDO: you should only do this for certain `meta' type variables
+unifyInst :: Inst -> TcM ([Inst], Bool)
unifyInst i@(EqInst {tci_left = ty1, tci_right = ty2})
| TyVarTy tv1 <- ty1, isMetaTyVar tv1 = go ty2 tv1
| TyVarTy tv2 <- ty2, isMetaTyVar tv2 = go ty1 tv2
; writeMetaTyVar cotv ty -- g := t
; return ([],True)
}
+unifyInst _ = panic "TcTyFuns.unifyInst: not EqInst"
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-occursCheckInsts :: [Inst] -> TcM ()
+occursCheckInsts :: CheckRule
occursCheckInsts insts = mappM_ occursCheckInst insts
-- fail
--
occursCheckInst :: Inst -> TcM ()
-occursCheckInst i@(EqInst {tci_left = ty1, tci_right = ty2})
+occursCheckInst (EqInst {tci_left = ty1, tci_right = ty2})
= go ty2
where
check ty = if ty `tcEqType` ty1
; failWithTcM (env2, hang msg 2 extra)
}
where msg = ptext SLIT("Occurs check: cannot construct the infinite type")
+occursCheckInst _ = panic "TcTyFuns.occursCheckInst: not eqInst"
\end{code}
Normalises a set of dictionaries relative to a set of given equalities (which
}
where
normaliseOneInst isWanted fun
- dict@(Dict {tci_name = name,
- tci_pred = pred,
+ dict@(Dict {tci_pred = pred,
tci_loc = loc})
= do { traceTc (text "genericNormaliseInst 1")
; (coi, pred') <- fun pred
}
-- TOMDO: treat other insts appropriately
- normaliseOneInst isWanted fun inst
+ normaliseOneInst _isWanted _fun inst
= do { inst' <- zonkInst inst
; return (inst', emptyBag)
}
+addBind :: Bag (LHsBind TcId) -> Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
addBind binds inst rhs = binds `unionBags` mkBind inst rhs
+mkBind :: Inst -> LHsExpr TcId -> Bag (LHsBind TcId)
mkBind inst rhs = unitBag (L (instSpan inst)
(VarBind (instToId inst) rhs))
\end{code}
projects / ghc-hetmet.git / blobdiff