Commit a6f6169a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Define mkTcNomReflCo = TcRefl Nominal, and use it all over

This patch doesn't include the changes to TcCanonical and TcSMonad,
which are a bigger follow-up patch, so it is tightly coupled to the
follow-up.
parent df2dd64d
......@@ -94,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 Nominal res_ty))
; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcNomReflCo res_ty))
; return (pat', cmd', res_co) }
\end{code}
......@@ -324,7 +324,7 @@ tc_cmd _ cmd _
matchExpectedCmdArgs :: Arity -> TcType -> TcM (TcCoercion, [TcType], TcType)
matchExpectedCmdArgs 0 ty
= return (mkTcReflCo Nominal ty, [], ty)
= return (mkTcNomReflCo ty, [], ty)
matchExpectedCmdArgs n ty
= do { (co1, [ty1, ty2]) <- matchExpectedTyConApp pairTyCon ty
; (co2, tys, res_ty) <- matchExpectedCmdArgs (n-1) ty2
......
......@@ -19,7 +19,8 @@ module TcEvidence (
-- TcCoercion
TcCoercion(..), LeftOrRight(..), pickLR,
mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
mkTcReflCo, mkTcNomReflCo,
mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo,
mkTcAxiomRuleCo,
......@@ -132,6 +133,9 @@ getTcCoVar_maybe _ = Nothing
mkTcReflCo :: Role -> TcType -> TcCoercion
mkTcReflCo = TcRefl
mkTcNomReflCo :: TcType -> TcCoercion
mkTcNomReflCo = TcRefl Nominal
mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2]
......
......@@ -1235,7 +1235,7 @@ tcTagToEnum loc fun_name arg res_ty
-- and returns a coercion between the two
get_rep_ty ty tc tc_args
| not (isFamilyTyCon tc)
= return (mkTcReflCo Nominal ty, tc, tc_args)
= return (mkTcNomReflCo ty, tc, tc_args)
| otherwise
= do { mb_fam <- tcLookupFamInst tc tc_args
; case mb_fam of
......
......@@ -99,7 +99,7 @@ solveInteractGiven loc fsks givens
, ctev_loc = loc }
| ev_id <- givens ]
fsk_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_evtm = EvCoercion (mkTcReflCo Nominal tv_ty)
fsk_bag = listToBag [ mkNonCanonical $ CtGiven { ctev_evtm = EvCoercion (mkTcNomReflCo tv_ty)
, ctev_pred = pred
, ctev_loc = loc }
| tv <- fsks
......@@ -987,7 +987,7 @@ solveWithIdentity wd tv xi
-- cf TcUnify.uUnboundKVar
; setWantedTyBind tv xi'
; let refl_evtm = EvCoercion (mkTcReflCo Nominal xi')
; let refl_evtm = EvCoercion (mkTcNomReflCo xi')
; when (isWanted wd) $
setEvBind (ctev_evar wd) refl_evtm
......@@ -1953,7 +1953,7 @@ getCoercibleInst loc ty1 ty2 = do
return
( Nothing
, Nothing
, mkTcReflCo Nominal ta1 {- == ta2, due to nominalArgsAgree -}
, mkTcNomReflCo ta1 {- == ta2, due to nominalArgsAgree -}
)
Representational -> do
ct_ev <- requestCoercible loc ta1 ta2
......
......@@ -809,7 +809,7 @@ zonkFlats binds_var untch cts
, not (tv `elemVarSet` tyVarsOfType ty_lhs) -- Do not construct an infinite type
= ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
do { writeMetaTyVar tv ty_lhs
; let evterm = EvCoercion (mkTcReflCo Nominal ty_lhs)
; let evterm = EvCoercion (mkTcNomReflCo ty_lhs)
evvar = ctev_evar (cc_ev zct)
; when (isWantedCt orig_ct) $ -- Can be derived (Trac #8129)
addTcEvBind binds_var evvar evterm
......
......@@ -219,11 +219,11 @@ tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty
| otherwise
= do { bndr_id <- newNoSigLetBndr no_gen bndr_name pat_ty
; traceTc "tcPatBndr(no-sig)" (ppr bndr_id $$ ppr (idType bndr_id))
; return (mkTcReflCo Nominal pat_ty, bndr_id) }
; return (mkTcNomReflCo pat_ty, bndr_id) }
tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
= do { bndr <- mkLocalBinder bndr_name pat_ty
; return (mkTcReflCo Nominal pat_ty, bndr) }
; return (mkTcNomReflCo pat_ty, bndr) }
------------
newNoSigLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
......
......@@ -131,7 +131,7 @@ matchExpectedFunTys herald arity orig_ty
-- then co : ty ~ t1 -> .. -> tn -> ty_r
go n_req ty
| n_req == 0 = return (mkTcReflCo Nominal ty, [], ty)
| n_req == 0 = return (mkTcNomReflCo ty, [], ty)
go n_req ty
| Just ty' <- tcView ty = go n_req ty'
......@@ -139,7 +139,7 @@ matchExpectedFunTys herald arity orig_ty
go n_req (FunTy arg_ty res_ty)
| not (isPredTy arg_ty)
= do { (co, tys, ty_r) <- go (n_req-1) res_ty
; return (mkTcFunCo Nominal (mkTcReflCo Nominal arg_ty) co, arg_ty:tys, ty_r) }
; return (mkTcFunCo Nominal (mkTcNomReflCo arg_ty) co, arg_ty:tys, ty_r) }
go n_req ty@(TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
......@@ -222,7 +222,7 @@ matchExpectedTyConApp tc orig_ty
go ty@(TyConApp tycon args)
| tc == tycon -- Common case
= return (mkTcReflCo Nominal ty, args)
= return (mkTcNomReflCo ty, args)
go (TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
......@@ -267,7 +267,7 @@ matchExpectedAppTy orig_ty
| Just ty' <- tcView ty = go ty'
| Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
= return (mkTcReflCo Nominal orig_ty, (fun_ty, arg_ty))
= return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty))
go (TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
......@@ -621,7 +621,7 @@ uType origin orig_ty1 orig_ty2
go (LitTy m) ty@(LitTy n)
| m == n
= return $ mkTcReflCo Nominal ty
= return $ mkTcNomReflCo ty
-- See Note [Care with type applications]
-- Do not decompose FunTy against App;
......@@ -769,7 +769,7 @@ uUnfilledVar :: CtOrigin
uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
| tv1 == tv2 -- Same type variable => no-op
= return (mkTcReflCo Nominal (mkTyVarTy tv1))
= return (mkTcNomReflCo (mkTyVarTy tv1))
| otherwise -- Distinct type variables
= do { lookup2 <- lookupTcTyVar tv2
......@@ -1044,7 +1044,7 @@ lookupTcTyVar tyvar
updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM TcCoercion
updateMeta tv1 ref1 ty2
= do { writeMetaTyVarRef tv1 ref1 ty2
; return (mkTcReflCo Nominal ty2) }
; return (mkTcNomReflCo ty2) }
\end{code}
Note [Unifying untouchables]
......
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