Commit 9d643cf6 authored by Joachim Breitner's avatar Joachim Breitner

Roleify TcCoercion

Previously, TcCoercion were only used to represent boxed Nominal
coercions. In order to also talk about boxed Representational coercions
in the type checker, we add Roles to TcCoercion. Again, we closely
mirror Coercion.

The roles are verified by a few assertions, and at the latest after
conversion to Coercion. I have put my trust in the comprehensiveness of
the testsuite here, but any role error after desugaring popping up now
might be caused by this refactoring.
parent f432229b
......@@ -25,11 +25,8 @@ module MkCore (
-- * Floats
FloatBind(..), wrapFloat,
-- * Constructing/deconstructing equality evidence boxes
-- * Constructing equality evidence boxes
mkEqBox,
-- * Constructing Coercible evidence
mkCoercible,
-- * Constructing general big tuples
-- $big_tuples
......@@ -302,17 +299,17 @@ mkStringExprFS str
\begin{code}
-- This take a ~# b (or a ~# R b) and returns a ~ b (or Coercible a b)
mkEqBox :: Coercion -> CoreExpr
mkEqBox co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ ppr (typeKind ty1) $$ ppr (typeKind ty2) )
Var (dataConWorkId eqBoxDataCon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
where Pair ty1 ty2 = coercionKind co
k = typeKind ty1
mkCoercible :: Coercion -> CoreExpr
mkCoercible co = ASSERT2( typeKind ty2 `eqKind` k, ppr co $$ ppr ty1 $$ ppr ty2 $$ ppr (typeKind ty1) $$ ppr (typeKind ty2) )
Var (dataConWorkId coercibleDataCon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
Var (dataConWorkId datacon) `mkTyApps` [k, ty1, ty2] `App` Coercion co
where Pair ty1 ty2 = coercionKind co
k = typeKind ty1
datacon = case coercionRole co of
Nominal -> eqBoxDataCon
Representational -> coercibleDataCon
Phantom -> pprPanic "mkEqBox does not support boxing phantom coercions"
(ppr co)
\end{code}
%************************************************************************
......
......@@ -626,7 +626,7 @@ dsCmd _ids local_vars _stack_ty _res_ty (HsCmdArrForm op _ args) env_ids = do
dsCmd ids local_vars stack_ty res_ty (HsCmdCast coercion cmd) env_ids = do
(core_cmd, env_ids') <- dsCmd ids local_vars stack_ty res_ty cmd env_ids
wrapped_cmd <- dsHsWrapper (WpCast coercion) core_cmd
wrapped_cmd <- dsHsWrapper (mkWpCast coercion) core_cmd
return (wrapped_cmd, env_ids')
dsCmd _ _ _ _ _ c = pprPanic "dsCmd" (ppr c)
......
......@@ -66,7 +66,6 @@ import Maybes
import OrdList
import Bag
import BasicTypes hiding ( TopLevel )
import Pair
import DynFlags
import FastString
import ErrUtils( MsgDoc )
......@@ -707,7 +706,8 @@ dsHsWrapper (WpTyApp ty) e = return $ App e (Type ty)
dsHsWrapper (WpLet ev_binds) e = do bs <- dsTcEvBinds ev_binds
return (mkCoreLets bs e)
dsHsWrapper (WpCompose c1 c2) e = dsHsWrapper c1 =<< dsHsWrapper c2 e
dsHsWrapper (WpCast co) e = dsTcCoercion Representational co (mkCast e)
dsHsWrapper (WpCast co) e = ASSERT (tcCoercionRole co == Representational)
dsTcCoercion co (mkCast e)
dsHsWrapper (WpEvLam ev) e = return $ Lam ev e
dsHsWrapper (WpTyLam tv) e = return $ Lam tv e
dsHsWrapper (WpEvApp evtrm) e = liftM (App e) (dsEvTerm evtrm)
......@@ -741,7 +741,7 @@ dsEvTerm (EvId v) = return (Var v)
dsEvTerm (EvCast tm co)
= do { tm' <- dsEvTerm tm
; dsTcCoercion Representational co $ mkCast tm' }
; dsTcCoercion co $ (mkCast tm' . mkSubCo) }
-- 'v' is always a lifted evidence variable so it is
-- unnecessary to call varToCoreExpr v here.
......@@ -749,7 +749,7 @@ dsEvTerm (EvDFunApp df tys tms) = do { tms' <- mapM dsEvTerm tms
; return (Var df `mkTyApps` tys `mkApps` tms') }
dsEvTerm (EvCoercion (TcCoVarCo v)) = return (Var v) -- See Note [Simple coercions]
dsEvTerm (EvCoercion co) = dsTcCoercion Nominal co mkEqBox
dsEvTerm (EvCoercion co) = dsTcCoercion co mkEqBox
dsEvTerm (EvTupleSel v n)
= do { tm' <- dsEvTerm v
......@@ -788,12 +788,12 @@ dsEvTerm (EvLit l) =
-- Note [Coercible Instances]
dsEvTerm (EvCoercible (EvCoercibleRefl ty)) = do
return $ mkCoercible $ mkReflCo Representational ty
return $ mkEqBox $ mkReflCo Representational ty
dsEvTerm (EvCoercible (EvCoercibleTyCon tyCon evs)) = do
ntEvs <- mapM (mapEvCoercibleArgM dsEvTerm) evs
wrapInEqRCases ntEvs $ \cos -> do
return $ mkCoercible $
return $ mkEqBox $
mkTyConAppCo Representational tyCon cos
dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
......@@ -801,7 +801,7 @@ dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
famenv <- dsGetFamInstEnvs
let Just (_, ntCo) = instNewTyConTF_maybe famenv tyCon tys
wrapInEqRCase ntEv $ \co -> do
return $ mkCoercible $ connect lor co ntCo
return $ mkEqBox $ connect lor co ntCo
where connect CLeft co2 co1 = mkTransCo co1 co2
connect CRight co2 co1 = mkTransCo co2 (mkSymCo co1)
......@@ -829,7 +829,7 @@ wrapInEqRCases (EvCoercibleArgP t1 t2:es) mkBody =
wrapInEqRCases [] mkBody = mkBody []
---------------------------------------
dsTcCoercion :: Role -> TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
-- This is the crucial function that moves
-- from TcCoercions to Coercions; see Note [TcCoercions] in Coercion
-- e.g. dsTcCoercion (trans g1 g2) k
......@@ -837,14 +837,14 @@ dsTcCoercion :: Role -> TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr
-- case g2 of EqBox g2# ->
-- k (trans g1# g2#)
-- thing_inside will get a coercion at the role requested
dsTcCoercion role co thing_inside
dsTcCoercion co thing_inside
= do { us <- newUniqueSupply
; let eqvs_covs :: [(EqVar,CoVar)]
eqvs_covs = zipWith mk_co_var (varSetElems (coVarsOfTcCo co))
(uniqsFromSupply us)
subst = mkCvSubst emptyInScopeSet [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs]
result_expr = thing_inside (ds_tc_coercion subst role co)
result_expr = thing_inside (ds_tc_coercion subst co)
result_ty = exprType result_expr
; return (foldr (wrap_in_case result_ty) result_expr eqvs_covs) }
......@@ -855,46 +855,44 @@ dsTcCoercion role co thing_inside
eq_nm = idName eqv
occ = nameOccName eq_nm
loc = nameSrcSpan eq_nm
ty = mkCoercionType Nominal ty1 ty2
ty = mkCoercionType (getEqPredRole (evVarPred eqv)) ty1 ty2
(ty1, ty2) = getEqPredTys (evVarPred eqv)
wrap_in_case result_ty (eqv, cov) body
= Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)]
wrap_in_case result_ty (eqv, cov) body
= case getEqPredRole (evVarPred eqv) of
Nominal -> Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)]
Representational -> Case (Var eqv) eqv result_ty [(DataAlt coercibleDataCon, [cov], body)]
Phantom -> panic "wrap_in_case/phantom"
ds_tc_coercion :: CvSubst -> Role -> TcCoercion -> Coercion
-- If the incoming TcCoercion if of type (a ~ b),
-- the result is of type (a ~# b)
-- The VarEnv maps EqVars of type (a ~ b) to Coercions of type (a ~# b)
ds_tc_coercion :: CvSubst -> TcCoercion -> Coercion
-- If the incoming TcCoercion if of type (a ~ b) (resp. Coercible a b)
-- the result is of type (a ~# b) (reps. a ~# b)
-- The VarEnv maps EqVars of type (a ~ b) to Coercions of type (a ~# b) (resp. and so on)
-- No need for InScope set etc because the
ds_tc_coercion subst role tc_co
= go role tc_co
ds_tc_coercion subst tc_co
= go tc_co
where
go Phantom co
= mkUnivCo Phantom ty1 ty2
where Pair ty1 ty2 = tcCoercionKind co
go r (TcRefl ty) = Refl r (Coercion.substTy subst ty)
go r (TcTyConAppCo tc cos) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) cos)
go r (TcAppCo co1 co2) = let leftCo = go r co1
go (TcRefl r ty) = Refl r (Coercion.substTy subst ty)
go (TcTyConAppCo r tc cos) = mkTyConAppCo r tc (map go cos)
go (TcAppCo co1 co2) = let leftCo = go co1
rightRole = nextRole leftCo in
mkAppCoFlexible leftCo rightRole (go rightRole co2)
go r (TcForAllCo tv co) = mkForAllCo tv' (ds_tc_coercion subst' r co)
mkAppCoFlexible leftCo rightRole (go co2)
go (TcForAllCo tv co) = mkForAllCo tv' (ds_tc_coercion subst' co)
where
(subst', tv') = Coercion.substTyVarBndr subst tv
go r (TcAxiomInstCo ax ind tys)
= mkAxInstCo r ax ind (map (Coercion.substTy subst) tys)
go r (TcSymCo co) = mkSymCo (go r co)
go r (TcTransCo co1 co2) = mkTransCo (go r co1) (go r co2)
go r (TcNthCo n co) = mkNthCoRole r n (go r co) -- the 2nd r is a harmless lie
go r (TcLRCo lr co) = maybeSubCo r $ mkLRCo lr (go Nominal co)
go r (TcInstCo co ty) = mkInstCo (go r co) ty
go r (TcLetCo bs co) = ds_tc_coercion (ds_co_binds bs) r co
go r (TcCastCo co1 co2) = maybeSubCo r $ mkCoCast (go Nominal co1)
(go Nominal co2)
go r (TcCoVarCo v) = maybeSubCo r $ ds_ev_id subst v
go _ (TcAxiomRuleCo co ts cs) = AxiomRuleCo co
(map (Coercion.substTy subst) ts)
(map (go Nominal) cs)
go (TcAxiomInstCo ax ind cos)
= AxiomInstCo ax ind (map go cos)
go (TcPhantomCo ty1 ty2) = UnivCo Phantom ty1 ty2
go (TcSymCo co) = mkSymCo (go co)
go (TcTransCo co1 co2) = mkTransCo (go co1) (go co2)
go (TcNthCo n co) = mkNthCo n (go co)
go (TcLRCo lr co) = mkLRCo lr (go co)
go (TcInstCo co ty) = mkInstCo (go co) ty
go (TcSubCo co) = mkSubCo (go co)
go (TcLetCo bs co) = ds_tc_coercion (ds_co_binds bs) co
go (TcCastCo co1 co2) = mkCoCast (go co1) (go co2)
go (TcCoVarCo v) = ds_ev_id subst v
go (TcAxiomRuleCo co ts cs) = AxiomRuleCo co (map (Coercion.substTy subst) ts) (map go cs)
......@@ -908,9 +906,9 @@ ds_tc_coercion subst role tc_co
ds_scc _ (CyclicSCC other) = pprPanic "ds_scc:cyclic" (ppr other $$ ppr tc_co)
ds_co_term :: CvSubst -> EvTerm -> Coercion
ds_co_term subst (EvCoercion tc_co) = ds_tc_coercion subst Nominal tc_co
ds_co_term subst (EvCoercion tc_co) = ds_tc_coercion subst tc_co
ds_co_term subst (EvId v) = ds_ev_id subst v
ds_co_term subst (EvCast tm co) = mkCoCast (ds_co_term subst tm) (ds_tc_coercion subst Nominal co)
ds_co_term subst (EvCast tm co) = mkCoCast (ds_co_term subst tm) (ds_tc_coercion subst co)
ds_co_term _ other = pprPanic "ds_co_term" (ppr other $$ ppr tc_co)
ds_ev_id :: CvSubst -> EqVar -> Coercion
......
......@@ -32,6 +32,7 @@ import HsSyn
-- NB: The desugarer, which straddles the source and Core worlds, sometimes
-- needs to see source types
import TcType
import Coercion ( Role(..) )
import TcEvidence
import TcRnMonad
import Type
......@@ -533,11 +534,11 @@ dsExpr expr@(RecordUpd record_expr (HsRecFields { rec_flds = fields })
-- Tediously wrap the application in a cast
-- Note [Update for GADTs]
wrap_co = mkTcTyConAppCo tycon
wrap_co = mkTcTyConAppCo Nominal tycon
[ lookup tv ty | (tv,ty) <- univ_tvs `zip` out_inst_tys ]
lookup univ_tv ty = case lookupVarEnv wrap_subst univ_tv of
Just co' -> co'
Nothing -> mkTcReflCo ty
Nothing -> mkTcReflCo Nominal ty
wrap_subst = mkVarEnv [ (tv, mkTcSymCo (mkTcCoVarCo eq_var))
| ((tv,_),eq_var) <- eq_spec `zip` eqs_vars ]
......@@ -547,7 +548,7 @@ dsExpr expr@(RecordUpd record_expr (HsRecFields { rec_flds = fields })
, pat_args = PrefixCon $ map nlVarPat arg_ids
, pat_ty = in_ty }
; let wrapped_rhs | null eq_spec = rhs
| otherwise = mkLHsWrap (WpCast wrap_co) rhs
| otherwise = mkLHsWrap (mkWpCast (mkTcSubCo wrap_co)) rhs
; return (mkSimpleMatch [pat] wrapped_rhs) }
\end{code}
......
......@@ -996,11 +996,11 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2
---------
eq_co :: TcCoercion -> TcCoercion -> Bool
-- Just some simple cases
eq_co (TcRefl t1) (TcRefl t2) = eqType t1 t2
eq_co (TcCoVarCo v1) (TcCoVarCo v2) = v1==v2
eq_co (TcSymCo co1) (TcSymCo co2) = co1 `eq_co` co2
eq_co (TcTyConAppCo tc1 cos1) (TcTyConAppCo tc2 cos2) = tc1==tc2 && eq_list eq_co cos1 cos2
-- Just some simple cases (should the r1 == r2 rather be an ASSERT?)
eq_co (TcRefl r1 t1) (TcRefl r2 t2) = r1 == r2 && eqType t1 t2
eq_co (TcCoVarCo v1) (TcCoVarCo v2) = v1==v2
eq_co (TcSymCo co1) (TcSymCo co2) = co1 `eq_co` co2
eq_co (TcTyConAppCo r1 tc1 cos1) (TcTyConAppCo r2 tc2 cos2) = r1 == r2 && tc1==tc2 && eq_list eq_co cos1 cos2
eq_co _ _ = False
patGroup :: DynFlags -> Pat Id -> PatGroup
......
......@@ -440,12 +440,10 @@ mkHsWrap co_fn e | isIdHsWrapper co_fn = e
| otherwise = HsWrap co_fn e
mkHsWrapCo :: TcCoercion -> HsExpr id -> HsExpr id
mkHsWrapCo co e | isTcReflCo co = e
| otherwise = mkHsWrap (WpCast co) e
mkHsWrapCo co e = mkHsWrap (coToHsWrapper co) e
mkLHsWrapCo :: TcCoercion -> LHsExpr id -> LHsExpr id
mkLHsWrapCo co (L loc e) | isTcReflCo co = L loc e
| otherwise = L loc (mkHsWrap (WpCast co) e)
mkLHsWrapCo co (L loc e) = L loc (mkHsWrapCo co e)
mkHsCmdCast :: TcCoercion -> HsCmd id -> HsCmd id
mkHsCmdCast co cmd | isTcReflCo co = cmd
......@@ -453,7 +451,7 @@ mkHsCmdCast co cmd | isTcReflCo co = cmd
coToHsWrapper :: TcCoercion -> HsWrapper
coToHsWrapper co | isTcReflCo co = idHsWrapper
| otherwise = WpCast co
| otherwise = mkWpCast (mkTcSubCo co)
mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id
mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
......@@ -461,7 +459,7 @@ mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
mkHsWrapPatCo :: TcCoercion -> Pat id -> Type -> Pat id
mkHsWrapPatCo co pat ty | isTcReflCo co = pat
| otherwise = CoPat (WpCast co) pat ty
| otherwise = CoPat (mkWpCast co) pat ty
mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id
mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr
......
......@@ -48,6 +48,7 @@ import InstEnv
import FunDeps
import TcMType
import Type
import Coercion ( Role(..) )
import TcType
import Class
import Unify
......@@ -222,7 +223,7 @@ instCallConstraints orig preds
; return (mkWpEvApps evs) }
where
go pred
| Just (ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut
| Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut
= do { co <- unifyType ty1 ty2
; return (EvCoercion co) }
| otherwise
......
......@@ -30,6 +30,7 @@ import TcEvidence
import Id( mkLocalId )
import Inst
import Name
import Coercion ( Role(..) )
import TysWiredIn
import VarSet
import TysPrim
......@@ -93,7 +94,7 @@ tcProc pat cmd exp_ty
; let cmd_env = CmdEnv { cmd_arr = arr_ty }
; (pat', cmd') <- tcPat ProcExpr pat arg_ty $
tcCmdTop cmd_env cmd (unitTy, res_ty)
; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcReflCo res_ty))
; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcReflCo Nominal res_ty))
; return (pat', cmd', res_co) }
\end{code}
......@@ -323,11 +324,11 @@ tc_cmd _ cmd _
matchExpectedCmdArgs :: Arity -> TcType -> TcM (TcCoercion, [TcType], TcType)
matchExpectedCmdArgs 0 ty
= return (mkTcReflCo ty, [], ty)
= return (mkTcReflCo Nominal ty, [], ty)
matchExpectedCmdArgs n ty
= do { (co1, [ty1, ty2]) <- matchExpectedTyConApp pairTyCon ty
; (co2, tys, res_ty) <- matchExpectedCmdArgs (n-1) ty2
; return (mkTcTyConAppCo pairTyCon [co1, co2], ty1:tys, res_ty) }
; return (mkTcTyConAppCo Nominal pairTyCon [co1, co2], ty1:tys, res_ty) }
\end{code}
......
......@@ -243,7 +243,7 @@ tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
-- co : t -> IP "x" t
toDict ipClass x ty =
case unwrapNewTyCon_maybe (classTyCon ipClass) of
Just (_,_,ax) -> HsWrap $ WpCast $ mkTcSymCo $ mkTcUnbranchedAxInstCo ax [x,ty]
Just (_,_,ax) -> HsWrap $ mkWpCast $ mkTcSymCo $ mkTcUnbranchedAxInstCo Representational ax [x,ty]
Nothing -> panic "The dictionary for `IP` is not a newtype?"
......
......@@ -235,7 +235,7 @@ canClassNC ev cls tys
canClass ev cls tys
= do { (xis, cos) <- flattenMany FMFullFlatten ev tys
; let co = mkTcTyConAppCo (classTyCon cls) cos
; let co = mkTcTyConAppCo Nominal (classTyCon cls) cos
xi = mkClassPred cls xis
; mb <- rewriteCtFlavor ev xi co
; traceTcS "canClass" (vcat [ ppr ev <+> ppr cls <+> ppr tys
......@@ -491,7 +491,7 @@ flatten f ctxt ty
; if eqType xi ty then return (ty,co) else return (xi,co) }
-- Small tweak for better error messages
flatten _ _ xi@(LitTy {}) = return (xi, mkTcReflCo xi)
flatten _ _ xi@(LitTy {}) = return (xi, mkTcReflCo Nominal xi)
flatten f ctxt (TyVarTy tv)
= flattenTyVar f ctxt tv
......@@ -504,14 +504,14 @@ flatten f ctxt (AppTy ty1 ty2)
flatten f ctxt (FunTy ty1 ty2)
= do { (xi1,co1) <- flatten f ctxt ty1
; (xi2,co2) <- flatten f ctxt ty2
; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) }
; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
flatten f ctxt (TyConApp tc tys)
-- For a normal type constructor or data family application, we just
-- recursively flatten the arguments.
| not (isSynFamilyTyCon tc)
= do { (xis,cos) <- flattenMany f ctxt tys
; return (mkTyConApp tc xis, mkTcTyConAppCo tc cos) }
; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
-- Otherwise, it's a type function application, and we have to
-- flatten it away as well, and generate a new given equality constraint
......@@ -529,7 +529,7 @@ flatten f ctxt (TyConApp tc tys)
; (ret_co, rhs_xi) <-
case f of
FMSubstOnly ->
return (mkTcReflCo fam_ty, fam_ty)
return (mkTcReflCo Nominal fam_ty, fam_ty)
FMFullFlatten ->
do { mb_ct <- lookupFlatEqn tc xi_args
; case mb_ct of
......@@ -561,7 +561,7 @@ flatten f ctxt (TyConApp tc tys)
-- Emit the flat constraints
; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable
-- cf Trac #5655
, mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args) $
, mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo Nominal tc cos_args) $
cos_rest
)
}
......@@ -651,7 +651,7 @@ flattenFinalTyVar f ctxt tv
do { let knd = tyVarKind tv
; (new_knd, _kind_co) <- flatten f ctxt knd
; let ty = mkTyVarTy (setVarType tv new_knd)
; return (ty, mkTcReflCo ty) }
; return (ty, mkTcReflCo Nominal ty) }
\end{code}
Note [Non-idempotent inert substitution]
......@@ -712,7 +712,7 @@ canEqNC ev ty1 ty2
| tcEqType ty1 ty2 -- Dealing with equality here avoids
-- later spurious occurs checks for a~a
= if isWanted ev then
setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo ty1)) >> return Stop
setEvBind (ctev_evar ev) (EvCoercion (mkTcReflCo Nominal ty1)) >> return Stop
else
return Stop
......@@ -781,7 +781,8 @@ canEqNC ev ty1 ty2
= do { let xevcomp [x,y] = EvCoercion (mkTcAppCo (evTermCoercion x) (evTermCoercion y))
xevcomp _ = error "canEqAppTy: can't happen" -- Can't happen
xevdecomp x = let xco = evTermCoercion x
in [EvCoercion (mkTcLRCo CLeft xco), EvCoercion (mkTcLRCo CRight xco)]
in [ EvCoercion (mkTcLRCo CLeft xco)
, EvCoercion (mkTcLRCo CRight xco)]
; ctevs <- xCtFlavor ev [mkTcEqPred s1 s2, mkTcEqPred t1 t2] (XEvTerm xevcomp xevdecomp)
; canEvVarsCreated ctevs }
......@@ -799,7 +800,7 @@ canDecomposableTyConApp ev tc1 tys1 tc2 tys2
-- Fail straight away for better error messages
= canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
| otherwise
= do { let xcomp xs = EvCoercion (mkTcTyConAppCo tc1 (map evTermCoercion xs))
= do { let xcomp xs = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
xev = XEvTerm xcomp xdecomp
; ctevs <- xCtFlavor ev (zipWith mkTcEqPred tys1 tys2) xev
......@@ -1085,7 +1086,7 @@ canEqLeafFun ev fn tys1 ty2 -- ev :: F tys1 ~ ty2
-- Fancy higher-dimensional coercion between equalities!
-- SPJ asks why? Why not just co : F xis1 ~ F tys1?
; let fam_head = mkTyConApp fn xis1
xco = mkHdEqPred ty2 (mkTcTyConAppCo fn cos1) co2
xco = mkHdEqPred ty2 (mkTcTyConAppCo Nominal fn cos1) co2
-- xco :: (F xis1 ~ xi2) ~ (F tys1 ~ ty2)
; mb <- rewriteCtFlavor ev (mkTcEqPred fam_head xi2) xco
......@@ -1117,7 +1118,8 @@ canEqLeafTyVar ev tv s2 -- ev :: tv ~ s2
(Just tv1, Just tv2) | tv1 == tv2
-> do { when (isWanted ev) $
setEvBind (ctev_evar ev) (mkEvCast (EvCoercion (mkTcReflCo xi1)) co)
ASSERT ( tcCoercionRole co == Nominal )
setEvBind (ctev_evar ev) (mkEvCast (EvCoercion (mkTcReflCo Nominal xi1)) co)
; return Stop }
(Just tv1, _) -> do { dflags <- getDynFlags
......@@ -1188,7 +1190,7 @@ mkHdEqPred :: Type -> TcCoercion -> TcCoercion -> TcCoercion
-- Make a higher-dimensional equality
-- co1 :: s1~t1, co2 :: s2~t2
-- Then (mkHdEqPred t2 co1 co2) :: (s1~s2) ~ (t1~t2)
mkHdEqPred t2 co1 co2 = mkTcTyConAppCo eqTyCon [mkTcReflCo (defaultKind (typeKind t2)), co1, co2]
mkHdEqPred t2 co1 co2 = mkTcTyConAppCo Nominal eqTyCon [mkTcReflCo Nominal (defaultKind (typeKind t2)), co1, co2]
-- Why defaultKind? Same reason as the comment on TcType/mkTcEqPred. I truly hate this (DV)
\end{code}
......
......@@ -7,7 +7,7 @@ module TcEvidence (
-- HsWrapper
HsWrapper(..),
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet,
(<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCast,
idHsWrapper, isIdHsWrapper, pprHsWrapper,
-- Evidence bindings
......@@ -22,20 +22,21 @@ module TcEvidence (
TcCoercion(..), LeftOrRight(..), pickLR,
mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcInstCos, mkTcSubCo,
mkTcAxiomRuleCo,
tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe
isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
tcCoercionRole, eqVarRole
) where
#include "HsVersions.h"
import Var
import Coercion( LeftOrRight(..), pickLR )
import Coercion( LeftOrRight(..), pickLR, nthRole )
import PprCore () -- Instance OutputableBndr TyVar
import TypeRep -- Knows type representation
import TcType
import Type( tyConAppArgN, tyConAppTyCon_maybe, getEqPredTys, coAxNthLHS )
import Type( tyConAppArgN, tyConAppTyCon_maybe, getEqPredTys, getEqPredRole, coAxNthLHS )
import TysPrim( funTyCon )
import TyCon
import CoAxiom
......@@ -68,8 +69,8 @@ boxed type (a ~ b). After we are done with typechecking the
desugarer finds the free variables, unboxes them, and creates a
resulting real Coercion with kosher free variables.
We can use most of the Coercion "smart constructors" to build TcCoercions. However,
mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
We can use most of the Coercion "smart constructors" to build TcCoercions.
However, mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
The data type is similar to Coercion.Coercion, with the following
differences
......@@ -77,42 +78,36 @@ differences
This is what lets us unify two for-all types and generate
equality constraints underneath
* The kind of a TcCoercion is t1 ~ t2
of a Coercion is t1 ~# t2
* The kind of a TcCoercion is t1 ~ t2 (resp. Coercible t1 t2)
of a Coercion is t1 ~# t2 (resp. t1 ~#R t2)
* TcCoercions are essentially all at role Nominal -- the type-checker
reasons only about nominal equality, not representational.
--> Exception: there can be newtype axioms wrapped up in TcCoercions.
These, of course, are only used in casts, so the desugarer
will still produce the right 'Coercion's.
* TcAxiomInstCo takes Types, not Coercions as arguments;
the generality is required only in the Simplifier
* UnsafeCo aren't required
* UnsafeCo aren't required, but we do have TcPhandomCo
* Representation invariants are weaker:
- we are allowed to have type synonyms in TcTyConAppCo
- the first arg of a TcAppCo can be a TcTyConAppCo
- TcSubCo is not applied as deep as done with mkSubCo
Reason: they'll get established when we desugar to Coercion
\begin{code}
data TcCoercion
= TcRefl TcType
| TcTyConAppCo TyCon [TcCoercion]
= TcRefl Role TcType
| TcTyConAppCo Role TyCon [TcCoercion]
| TcAppCo TcCoercion TcCoercion
| TcForAllCo TyVar TcCoercion
| TcInstCo TcCoercion TcType
| TcCoVarCo EqVar -- variable always at role N
| TcAxiomInstCo (CoAxiom Branched) Int [TcType] -- Int specifies branch number
-- See [CoAxiom Index] in Coercion.lhs
-- This is number of types and coercions are expected to macth to CoAxiomRule
| TcCoVarCo EqVar
| TcAxiomInstCo (CoAxiom Branched) Int [TcCoercion] -- Int specifies branch number
-- See [CoAxiom Index] in Coercion.lhs
-- This is number of types and coercions are expected to match to CoAxiomRule
-- (i.e., the CoAxiomRules are always fully saturated)
| TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
| TcPhantomCo TcType TcType
| TcSymCo TcCoercion
| TcTransCo TcCoercion TcCoercion
| TcNthCo Int TcCoercion
| TcLRCo LeftOrRight TcCoercion
| TcSubCo TcCoercion
| TcCastCo TcCoercion TcCoercion -- co1 |> co2
| TcLetCo TcEvBinds TcCoercion
deriving (Data.Data, Data.Typeable)
......@@ -124,8 +119,8 @@ isEqVar v = case tyConAppTyCon_maybe (varType v) of
Nothing -> False
isTcReflCo_maybe :: TcCoercion -> Maybe TcType
isTcReflCo_maybe (TcRefl ty) = Just ty
isTcReflCo_maybe _ = Nothing
isTcReflCo_maybe (TcRefl _ ty) = Just ty
isTcReflCo_maybe _ = Nothing
isTcReflCo :: TcCoercion -> Bool
isTcReflCo (TcRefl {}) = True
......@@ -135,41 +130,71 @@ getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
getTcCoVar_maybe (TcCoVarCo v) = Just v
getTcCoVar_maybe _ = Nothing
mkTcReflCo :: TcType -> TcCoercion
mkTcReflCo :: Role -> TcType -> TcCoercion
mkTcReflCo = TcRefl
mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]
mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2]
mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion
mkTcTyConAppCo tc cos -- No need to expand type synonyms
-- See Note [TcCoercions]
mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
mkTcTyConAppCo role tc cos -- No need to expand type synonyms
-- See Note [TcCoercions]
| Just tys <- traverse isTcReflCo_maybe cos
= TcRefl (mkTyConApp tc tys) -- See Note [Refl invariant]
| otherwise = TcTyConAppCo tc cos
mkTcAxInstCo :: CoAxiom br -> Int -> [TcType] -> TcCoercion
mkTcAxInstCo ax ind tys
| arity == n_tys = TcAxiomInstCo ax_br ind tys
= TcRefl role (mkTyConApp tc tys) -- See Note [Refl invariant]
| otherwise = TcTyConAppCo role tc cos
-- input coercion is Nominal
-- mkSubCo will do some normalisation. We do not do it for TcCoercions, but
-- defer that to desugaring; just to reduce the code duplication a little bit
mkTcSubCo :: TcCoercion -> TcCoercion
mkTcSubCo co = ASSERT2 ( tcCoercionRole co == Nominal, ppr co)
TcSubCo co
maybeTcSubCo2_maybe :: Role -- desired role
-> Role -- current role
-> TcCoercion -> Maybe TcCoercion
maybeTcSubCo2_maybe Representational Nominal = Just . mkTcSubCo
maybeTcSubCo2_maybe Nominal Representational = const Nothing
maybeTcSubCo2_maybe Phantom _ = panic "maybeTcSubCo2_maybe Phantom" -- not supported (not needed at the moment)
maybeTcSubCo2_maybe _ Phantom = const Nothing
maybeTcSubCo2_maybe _ _ = Just
maybeTcSubCo2 :: Role -- desired role
-> Role -- current role
-> TcCoercion -> TcCoercion
maybeTcSubCo2 r1 r2 co
= case maybeTcSubCo2_maybe r1 r2 co of
Just co' -> co'
Nothing -> pprPanic "maybeTcSubCo2" (ppr r1 <+> ppr r2 <+> ppr co)
mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion
mkTcAxInstCo role ax index tys
| ASSERT2 ( not (role == Nominal && ax_role == Representational) , ppr (ax, tys) )
arity == n_tys = maybeTcSubCo2 role ax_role $ TcAxiomInstCo ax_br index rtys
| otherwise = ASSERT( arity < n_tys )
foldl TcAppCo (TcAxiomInstCo ax_br ind (take arity tys))
(map TcRefl (drop arity tys))
maybeTcSubCo2 role ax_role $
foldl TcAppCo (TcAxiomInstCo ax_br index (take arity rtys))
(drop arity rtys)
where
n_tys = length tys
arity = coAxiomArity ax ind
ax_br = toBranchedAxiom ax
n_tys = length tys
ax_br = toBranchedAxiom ax
branch = coAxiomNthBranch ax_br index
arity = length $ coAxBranchTyVars branch
ax_role = coAxiomRole ax
arg_roles = coAxBranchRoles branch
rtys = zipWith mkTcReflCo (arg_roles ++ repeat Nominal) tys
mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
mkTcAxiomRuleCo = TcAxiomRuleCo
mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType] -> TcCoercion
mkTcUnbranchedAxInstCo ax tys
= mkTcAxInstCo ax 0 tys
mkTcUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [TcType] -> TcCoercion
mkTcUnbranchedAxInstCo role ax tys
= mkTcAxInstCo role ax 0 tys
mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
-- No need to deal with TyConApp on the left; see Note [TcCoercions]
mkTcAppCo (TcRefl ty1) (TcRefl ty2) = TcRefl (mkAppTy ty1 ty2)