import HsSyn
import TypeRep
import CoreUtils( mkPiTypes )
-import TcErrors ( unifyCtxt )
+import TcErrors ( unifyCtxt )
import TcMType
import TcIface
import TcRnMonad
import Name
import ErrUtils
import BasicTypes
-
import Maybes ( allMaybes )
import Util
import Outputable
matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
-> Arity
-> TcRhoType
- -> TcM (CoercionI, [TcSigmaType], TcRhoType)
+ -> TcM (Coercion, [TcSigmaType], TcRhoType)
-- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r)
-- then co : ty ~ (t1 -> ... -> tn -> ty_r)
-- then co : ty ~ t1 -> .. -> tn -> ty_r
go n_req ty
- | n_req == 0 = return (IdCo ty, [], ty)
+ | n_req == 0 = return (mkReflCo ty, [], ty)
go n_req ty
| Just ty' <- tcView ty = go n_req ty'
go n_req (FunTy arg_ty res_ty)
| not (isPredTy arg_ty)
= do { (coi, tys, ty_r) <- go (n_req-1) res_ty
- ; return (mkFunTyCoI (IdCo arg_ty) coi, arg_ty:tys, ty_r) }
+ ; return (mkFunCo (mkReflCo arg_ty) coi, arg_ty:tys, ty_r) }
go _ (TyConApp tc _) -- A common case
| not (isSynFamilyTyCon tc)
\begin{code}
----------------------
-matchExpectedListTy :: TcRhoType -> TcM (CoercionI, TcRhoType)
+matchExpectedListTy :: TcRhoType -> TcM (Coercion, TcRhoType)
-- Special case for lists
matchExpectedListTy exp_ty
= do { (coi, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty
; return (coi, elt_ty) }
----------------------
-matchExpectedPArrTy :: TcRhoType -> TcM (CoercionI, TcRhoType)
+matchExpectedPArrTy :: TcRhoType -> TcM (Coercion, TcRhoType)
-- Special case for parrs
matchExpectedPArrTy exp_ty
= do { (coi, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty
----------------------
matchExpectedTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
-> TcRhoType -- orig_ty
- -> TcM (CoercionI, -- T a b c ~ orig_ty
+ -> TcM (Coercion, -- T a b c ~ orig_ty
[TcSigmaType]) -- Element types, a b c
-- It's used for wired-in tycons, so we call checkWiredInTyCon
= do { checkWiredInTyCon tc
; go (tyConArity tc) orig_ty [] }
where
- go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (CoercionI, [TcSigmaType])
+ go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (Coercion, [TcSigmaType])
-- If go n ty tys = (co, [t1..tn] ++ tys)
-- then co : T t1..tn ~ ty
go n_req ty@(TyConApp tycon args) tys
| tc == tycon
= ASSERT( n_req == length args) -- ty::*
- return (IdCo ty, args ++ tys)
+ return (mkReflCo ty, args ++ tys)
go n_req (AppTy fun arg) tys
| n_req > 0
= do { (coi, args) <- go (n_req - 1) fun (arg : tys)
- ; return (mkAppTyCoI coi (IdCo arg), args) }
+ ; return (mkAppCo coi (mkReflCo arg), args) }
go n_req ty tys = defer n_req ty tys
----------------------
matchExpectedAppTy :: TcRhoType -- orig_ty
- -> TcM (CoercionI, -- m a ~ orig_ty
+ -> TcM (Coercion, -- m a ~ orig_ty
(TcSigmaType, TcSigmaType)) -- Returns m, a
-- If the incoming type is a mutable type variable of kind k, then
-- matchExpectedAppTy returns a new type variable (m: * -> k); note the *.
| Just ty' <- tcView ty = go ty'
| Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
- = return (IdCo orig_ty, (fun_ty, arg_ty))
+ = return (mkReflCo orig_ty, (fun_ty, arg_ty))
go (TyVarTy tv)
| ASSERT( isTcTyVar tv) isMetaTyVar tv
<- tcGen ctxt ty_expected $ \ _ sk_rho -> do
{ (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
; coi <- unifyType in_rho sk_rho
- ; return (coiToHsWrapper coi <.> in_wrap) }
+ ; return (coToHsWrapper coi <.> in_wrap) }
; return (sk_wrap <.> inst_wrap) }
| otherwise -- Urgh! It seems deeply weird to have equality
-- when actual is not a polytype, and it makes a big
-- difference e.g. tcfail104
= do { coi <- unifyType ty_actual ty_expected
- ; return (coiToHsWrapper coi) }
+ ; return (coToHsWrapper coi) }
tcInfer :: (TcType -> TcM a) -> TcM (a, TcType)
tcInfer tc_infer = do { ty <- newFlexiTyVarTy openTypeKind
tcWrapResult expr actual_ty res_ty
= do { coi <- unifyType actual_ty res_ty
-- Both types are deeply skolemised
- ; return (mkHsWrapCoI coi expr) }
+ ; return (mkHsWrapCo coi expr) }
-----------------------------------
wrapFunResCoercion
\begin{code}
---------------
-unifyType :: TcTauType -> TcTauType -> TcM CoercionI
+unifyType :: TcTauType -> TcTauType -> TcM Coercion
-- Actual and expected types
-- Returns a coercion : ty1 ~ ty2
unifyType ty1 ty2 = uType [] ty1 ty2
---------------
-unifyPred :: PredType -> PredType -> TcM CoercionI
+unifyPred :: PredType -> PredType -> TcM Coercion
-- Actual and expected types
unifyPred p1 p2 = uPred [UnifyOrigin (mkPredTy p1) (mkPredTy p2)] p1 p2
---------------
-unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
+unifyTheta :: TcThetaType -> TcThetaType -> TcM [Coercion]
-- Actual and expected types
unifyTheta theta1 theta2
= do { checkTc (equalLength theta1 theta2)
:: [EqOrigin]
-> TcType -- ty1 is the *actual* type
-> TcType -- ty2 is the *expected* type
- -> TcM CoercionI
+ -> TcM Coercion
--------------
-- It is always safe to defer unification to the main constraint solver
; doc <- mkErrInfo emptyTidyEnv ctxt
; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin, doc])
- ; return $ ACo $ mkTyVarTy co_var }
+ ; return $ mkCoVarCo co_var }
uType_defer [] _ _
= panic "uType_defer"
[ sep [ ppr orig_ty1, text "~", ppr orig_ty2]
, ppr origin]
; coi <- go orig_ty1 orig_ty2
- ; case coi of
- ACo co -> traceTc "u_tys yields coercion:" (ppr co)
- IdCo _ -> traceTc "u_tys yields no coercion" empty
+ ; if isReflCo coi
+ then traceTc "u_tys yields no coercion" empty
+ else traceTc "u_tys yields coercion:" (ppr coi)
; return coi }
where
bale_out :: [EqOrigin] -> TcM a
bale_out origin = failWithMisMatch origin
- go :: TcType -> TcType -> TcM CoercionI
+ go :: TcType -> TcType -> TcM Coercion
-- The arguments to 'go' are always semantically identical
-- to orig_ty{1,2} except for looking through type synonyms
| Just ty1' <- tcView ty1 = go ty1' ty2
| Just ty2' <- tcView ty2 = go ty1 ty2'
-
-- Predicates
go (PredTy p1) (PredTy p2) = uPred origin p1 p2
- -- Coercion functions: (t1a ~ t1b) => t1c ~ (t2a ~ t2b) => t2c
- go ty1 ty2
- | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1,
- Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2
- = do { co1 <- uType origin t1a t2a
- ; co2 <- uType origin t1b t2b
- ; co3 <- uType origin t1c t2c
- ; return $ mkCoPredCoI co1 co2 co3 }
-
-- Functions (or predicate functions) just check the two parts
go (FunTy fun1 arg1) (FunTy fun2 arg2)
= do { coi_l <- uType origin fun1 fun2
; coi_r <- uType origin arg1 arg2
- ; return $ mkFunTyCoI coi_l coi_r }
+ ; return $ mkFunCo coi_l coi_r }
-- Always defer if a type synonym family (type function)
-- is involved. (Data families behave rigidly.)
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2 -- See Note [TyCon app]
= do { cois <- uList origin uType tys1 tys2
- ; return $ mkTyConAppCoI tc1 cois }
+ ; return $ mkTyConAppCo tc1 cois }
-- See Note [Care with type applications]
go (AppTy s1 t1) ty2
| Just (s2,t2) <- tcSplitAppTy_maybe ty2
= do { coi_s <- uType_np origin s1 s2 -- See Note [Unifying AppTy]
; coi_t <- uType origin t1 t2
- ; return $ mkAppTyCoI coi_s coi_t }
+ ; return $ mkAppCo coi_s coi_t }
go ty1 (AppTy s2 t2)
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
= do { coi_s <- uType_np origin s1 s2
; coi_t <- uType origin t1 t2
- ; return $ mkAppTyCoI coi_s coi_t }
+ ; return $ mkAppCo coi_s coi_t }
go ty1 ty2
| tcIsForAllTy ty1 || tcIsForAllTy ty2
-- Anything else fails
go _ _ = bale_out origin
-unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM CoercionI
+unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM Coercion
unifySigmaTy origin ty1 ty2
= do { let (tvs1, body1) = tcSplitForAllTys ty1
(tvs2, body2) = tcSplitForAllTys ty2
-- Get location from monad, not from tvs1
; let tys = mkTyVarTys skol_tvs
in_scope = mkInScopeSet (mkVarSet skol_tvs)
- phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
- phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
--- untch = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+ phi1 = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1
+ phi2 = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2
; ((coi, _untch), lie) <- captureConstraints $
captureUntouchables $
(failWithMisMatch origin) -- ToDo: give details from bad_lie
; emitConstraints lie
- ; return (foldr mkForAllTyCoI coi skol_tvs) }
+ ; return (foldr mkForAllCo coi skol_tvs) }
----------
-uPred :: [EqOrigin] -> PredType -> PredType -> TcM CoercionI
+uPred :: [EqOrigin] -> PredType -> PredType -> TcM Coercion
uPred origin (IParam n1 t1) (IParam n2 t2)
| n1 == n2
= do { coi <- uType origin t1 t2
- ; return $ mkIParamPredCoI n1 coi }
+ ; return $ mkPredCo $ IParam n1 coi }
uPred origin (ClassP c1 tys1) (ClassP c2 tys2)
| c1 == c2
= do { cois <- uList origin uType tys1 tys2
-- Guaranteed equal lengths because the kinds check
- ; return $ mkClassPPredCoI c1 cois }
+ ; return $ mkPredCo $ ClassP c1 cois }
+
uPred origin (EqPred ty1a ty1b) (EqPred ty2a ty2b)
- = do { coia <- uType origin ty1a ty2a
- ; coib <- uType origin ty1b ty2b
- ; return $ mkEqPredCoI coia coib }
+ = do { coa <- uType origin ty1a ty2a
+ ; cob <- uType origin ty1b ty2b
+ ; return $ mkPredCo $ EqPred coa cob }
uPred origin _ _ = failWithMisMatch origin
back into @uTys@ if it turns out that the variable is already bound.
\begin{code}
-uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM CoercionI
+uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM Coercion
uVar origin swapped tv1 ty2
= do { traceTc "uVar" (vcat [ ppr origin
, ppr swapped
-> SwapFlag
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> TcTauType -- Type 2
- -> TcM CoercionI
+ -> TcM Coercion
-- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
-- It might be a skolem, or untouchable, or meta
uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2)
| tv1 == tv2 -- Same type variable => no-op
- = return (IdCo (mkTyVarTy tv1))
+ = return (mkReflCo (mkTyVarTy tv1))
| otherwise -- Distinct type variables
= do { lookup2 <- lookupTcTyVar tv2
-> SwapFlag
-> TcTyVar -> TcTyVarDetails -- Tyvar 1
-> TcTyVar -> TcTyVarDetails -- Tyvar 2
- -> TcM CoercionI
+ -> TcM Coercion
-- Invarant: The type variables are distinct,
-- Neither is filled in yet
details = ASSERT2( isTcTyVar tyvar, ppr tyvar )
tcTyVarDetails tyvar
-updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM CoercionI
+updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM Coercion
updateMeta tv1 ref1 ty2
= do { writeMetaTyVarRef tv1 ref1 ty2
- ; return (IdCo ty2) }
+ ; return (mkReflCo ty2) }
\end{code}
Note [Unifying untouchables]
projects / ghc-hetmet.git / blobdiff