diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2011-12-05 04:46:15 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2011-12-05 04:46:15 +0000 |
| commit | eb21a9793c903dacfd0b86e5ce80178c8ccbd731 (patch) | |
| tree | 8e6ae156b130e56bba9be378156206ef2f88cdbd /compiler | |
| parent | 9a0adc0b01aa62bd605145a555d26645229d5cc1 (diff) | |
| parent | 2e6dcdf711ebd50eef230a878014a5a9abd20e07 (diff) | |
| download | haskell-eb21a9793c903dacfd0b86e5ce80178c8ccbd731.tar.gz | |
Merge branch 'master' of ../HEAD
Diffstat (limited to 'compiler')
48 files changed, 1090 insertions, 774 deletions
diff --git a/compiler/basicTypes/Var.lhs b/compiler/basicTypes/Var.lhs index 8e31fef8ea..d7caf2a521 100644 --- a/compiler/basicTypes/Var.lhs +++ b/compiler/basicTypes/Var.lhs @@ -122,14 +122,13 @@ Note [Evidence: EvIds and CoVars] * An EvId (evidence Id) is a *boxed*, term-level evidence variable (dictionary, implicit parameter, or equality). -* DictId, IpId, and EqVar are synonyms when we know what kind of - evidence we are talking about. For example, an EqVar has type (t1 ~ t2). - * A CoVar (coercion variable) is an *unboxed* term-level evidence variable of type (t1 ~# t2). So it's the unboxed version of an EqVar. -* Only CoVars can occur in Coercions (but NB the LCoercion hack; see - Note [LCoercions] in Coercion). +* Only CoVars can occur in Coercions, EqVars appear in TcCoercions. + +* DictId, IpId, and EqVar are synonyms when we know what kind of + evidence we are talking about. For example, an EqVar has type (t1 ~ t2). Note [Kind and type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/coreSyn/TrieMap.lhs b/compiler/coreSyn/TrieMap.lhs index b7ee95c2af..d8a134ed87 100644 --- a/compiler/coreSyn/TrieMap.lhs +++ b/compiler/coreSyn/TrieMap.lhs @@ -14,7 +14,7 @@ {-# LANGUAGE TypeFamilies #-} module TrieMap( CoreMap, emptyCoreMap, extendCoreMap, lookupCoreMap, foldCoreMap, - TypeMap, + TypeMap, foldTypeMap, CoercionMap, MaybeMap, ListMap, @@ -488,6 +488,12 @@ data TypeMap a , tm_tc_app :: NameEnv (ListMap TypeMap a) , tm_forall :: TypeMap (BndrMap a) } +instance Outputable a => Outputable (TypeMap a) where + ppr m = text "TypeMap elts" <+> ppr (foldTypeMap (:) [] m) + +foldTypeMap :: (a -> b -> b) -> b -> TypeMap a -> b +foldTypeMap k z m = fdT k m z + wrapEmptyTypeMap :: TypeMap a wrapEmptyTypeMap = TM { tm_var = emptyTM , tm_app = EmptyTM diff --git a/compiler/deSugar/Desugar.lhs b/compiler/deSugar/Desugar.lhs index cb23075134..cb482eaf89 100644 --- a/compiler/deSugar/Desugar.lhs +++ b/compiler/deSugar/Desugar.lhs @@ -120,7 +120,7 @@ deSugar hsc_env else return (binds, hpcInfo, emptyModBreaks) initDs hsc_env mod rdr_env type_env $ do - do { ds_ev_binds <- dsEvBinds ev_binds + do { let ds_ev_binds = dsEvBinds ev_binds ; core_prs <- dsTopLHsBinds binds_cvr ; (spec_prs, spec_rules) <- dsImpSpecs imp_specs ; (ds_fords, foreign_prs) <- dsForeigns fords diff --git a/compiler/deSugar/DsArrows.lhs b/compiler/deSugar/DsArrows.lhs index d276baf86d..1748ce7cac 100644 --- a/compiler/deSugar/DsArrows.lhs +++ b/compiler/deSugar/DsArrows.lhs @@ -32,6 +32,7 @@ import TcHsSyn import {-# SOURCE #-} DsExpr ( dsExpr, dsLExpr, dsLocalBinds ) import TcType +import TcEvidence import Type import CoreSyn import CoreFVs diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs index b6a5e3e507..d44943c347 100644 --- a/compiler/deSugar/DsBinds.lhs +++ b/compiler/deSugar/DsBinds.lhs @@ -18,7 +18,7 @@ lower levels it is preserved with @let@/@letrec@s). -- for details module DsBinds ( dsTopLHsBinds, dsLHsBinds, decomposeRuleLhs, dsSpec, - dsHsWrapper, dsTcEvBinds, dsEvBinds, + dsHsWrapper, dsTcEvBinds, dsEvBinds, dsTcCoercion ) where #include "HsVersions.h" @@ -41,6 +41,7 @@ import CoreFVs import Digraph import TyCon ( isTupleTyCon, tyConDataCons_maybe ) +import TcEvidence import TcType import Type import Coercion hiding (substCo) @@ -107,8 +108,7 @@ dsHsBind (FunBind { fun_id = L _ fun, fun_matches = matches , fun_infix = inf }) = do { (args, body) <- matchWrapper (FunRhs (idName fun) inf) matches ; let body' = mkOptTickBox tick body - ; wrap_fn' <- dsHsWrapper co_fn - ; let rhs = wrap_fn' (mkLams args body') + rhs = dsHsWrapper co_fn (mkLams args body') ; {- pprTrace "dsHsBind" (ppr fun <+> ppr (idInlinePragma fun)) $ -} return (unitOL (makeCorePair fun False 0 rhs)) } @@ -131,12 +131,10 @@ dsHsBind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts | ABE { abe_wrap = wrap, abe_poly = global , abe_mono = local, abe_prags = prags } <- export = do { bind_prs <- ds_lhs_binds binds - ; ds_ev_binds <- dsTcEvBinds ev_binds - ; wrap_fn <- dsHsWrapper wrap ; let core_bind = Rec (fromOL bind_prs) - rhs = wrap_fn $ -- Usually the identity + rhs = dsHsWrapper wrap $ -- Usually the identity mkLams tyvars $ mkLams dicts $ - mkCoreLets ds_ev_binds $ + mkCoreLets (dsTcEvBinds ev_binds) $ Let core_bind $ Var local @@ -152,14 +150,13 @@ dsHsBind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts , abs_exports = exports, abs_ev_binds = ev_binds , abs_binds = binds }) = do { bind_prs <- ds_lhs_binds binds - ; ds_ev_binds <- dsTcEvBinds ev_binds ; let core_bind = Rec (fromOL bind_prs) -- Monomorphic recursion possible, hence Rec tup_expr = mkBigCoreVarTup locals tup_ty = exprType tup_expr poly_tup_rhs = mkLams tyvars $ mkLams dicts $ - mkCoreLets ds_ev_binds $ + mkCoreLets (dsTcEvBinds ev_binds) $ Let core_bind $ tup_expr locals = map abe_mono exports @@ -168,9 +165,9 @@ dsHsBind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts ; let mk_bind (ABE { abe_wrap = wrap, abe_poly = global , abe_mono = local, abe_prags = spec_prags }) - = do { wrap_fn <- dsHsWrapper wrap - ; tup_id <- newSysLocalDs tup_ty - ; let rhs = wrap_fn $ mkLams tyvars $ mkLams dicts $ + = do { tup_id <- newSysLocalDs tup_ty + ; let rhs = dsHsWrapper wrap $ + mkLams tyvars $ mkLams dicts $ mkTupleSelector locals local tup_id $ mkVarApps (Var poly_tup_id) (tyvars ++ dicts) rhs_for_spec = Let (NonRec poly_tup_id poly_tup_rhs) rhs @@ -183,104 +180,6 @@ dsHsBind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts ; return ((poly_tup_id, poly_tup_rhs) `consOL` concatOL export_binds_s) } --------------------------------------- -dsTcEvBinds :: TcEvBinds -> DsM [CoreBind] -dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds" -- Zonker has got rid of this -dsTcEvBinds (EvBinds bs) = -- pprTrace "EvBinds bs = " (ppr bs) $ - dsEvBinds bs - -dsEvBinds :: Bag EvBind -> DsM [CoreBind] -dsEvBinds bs = do { let core_binds = map dsEvSCC sccs --- ; pprTrace "dsEvBinds, result = " (vcat (map ppr core_binds)) $ - ; return core_binds } --- ; return (map dsEvGroup sccs) - where - sccs :: [SCC EvBind] - sccs = stronglyConnCompFromEdgedVertices edges - - edges :: [(EvBind, EvVar, [EvVar])] - edges = foldrBag ((:) . mk_node) [] bs - - mk_node :: EvBind -> (EvBind, EvVar, [EvVar]) - mk_node b@(EvBind var term) = (b, var, free_vars_of term) - - free_vars_of :: EvTerm -> [EvVar] - free_vars_of (EvId v) = [v] - free_vars_of (EvCast v co) = v : varSetElems (coVarsOfCo co) - free_vars_of (EvCoercionBox co) = varSetElems (coVarsOfCo co) - free_vars_of (EvDFunApp _ _ vs) = vs - free_vars_of (EvTupleSel v _) = [v] - free_vars_of (EvTupleMk vs) = vs - free_vars_of (EvSuperClass d _) = [d] - -dsEvSCC :: SCC EvBind -> CoreBind - -dsEvSCC (AcyclicSCC (EvBind v r)) - = NonRec v (dsEvTerm r) - -dsEvSCC (CyclicSCC bs) - = Rec (map ds_pair bs) - where - ds_pair (EvBind v r) = (v, dsEvTerm r) - ---------------------------------------- -dsLCoercion :: LCoercion -> (Coercion -> CoreExpr) -> CoreExpr --- This is the crucial function that moves --- from LCoercions to Coercions; see Note [LCoercions] in Coercion --- e.g. dsLCoercion (trans g1 g2) k --- = case g1 of EqBox g1# -> --- case g2 of EqBox g2# -> --- k (trans g1# g2#) -dsLCoercion co k - = foldr wrap_in_case result_expr eqvs_covs - where - result_expr = k (substCo subst co) - result_ty = exprType result_expr - - -- We use the same uniques for the EqVars and the CoVars, and just change - -- the type. So the CoVars shadow the EqVars - -- - -- NB: DON'T try to cheat and not substitute into the LCoercion to change the - -- types of the free variables: -ddump-ds will panic if you do this since it - -- runs Lint before we substitute CoVar occurrences out for their binding sites. - eqvs_covs = [(eqv, eqv `setIdType` mkCoercionType ty1 ty2) - | eqv <- varSetElems (coVarsOfCo co) - , let (ty1, ty2) = getEqPredTys (evVarPred eqv)] - - subst = extendCvSubstList (mkEmptySubst (mkInScopeSet (tyCoVarsOfCo co))) - [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs] - - wrap_in_case (eqv, cov) body - = Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)] - ---------------------------------------- -dsEvTerm :: EvTerm -> CoreExpr -dsEvTerm (EvId v) = Var v - -dsEvTerm (EvCast v co) - = dsLCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is - -- unnecessary to call varToCoreExpr v here. - -dsEvTerm (EvDFunApp df tys vars) = Var df `mkTyApps` tys `mkVarApps` vars -dsEvTerm (EvCoercionBox co) = dsLCoercion co mkEqBox -dsEvTerm (EvTupleSel v n) - = ASSERT( isTupleTyCon tc ) - Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')] - where - (tc, tys) = splitTyConApp (evVarPred v) - Just [dc] = tyConDataCons_maybe tc - v' = v `setVarType` ty_want - xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after - (tys_before, ty_want:tys_after) = splitAt n tys -dsEvTerm (EvTupleMk vs) = Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs - where dc = tupleCon ConstraintTuple (length vs) - tys = map varType vs -dsEvTerm (EvSuperClass d n) - = Var sc_sel_id `mkTyApps` tys `App` Var d - where - sc_sel_id = classSCSelId cls n -- Zero-indexed - (cls, tys) = getClassPredTys (evVarPred d) - ------------------------ makeCorePair :: Id -> Bool -> Arity -> CoreExpr -> (Id, CoreExpr) makeCorePair gbl_id is_default_method dict_arity rhs @@ -500,14 +399,13 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl)) = putSrcSpanDs loc $ do { let poly_name = idName poly_id ; spec_name <- newLocalName poly_name - ; wrap_fn <- dsHsWrapper spec_co - ; let (bndrs, ds_lhs) = collectBinders (wrap_fn (Var poly_id)) + ; let (bndrs, ds_lhs) = collectBinders (dsHsWrapper spec_co (Var poly_id)) spec_ty = mkPiTypes bndrs (exprType ds_lhs) ; case decomposeRuleLhs bndrs ds_lhs of { Left msg -> do { warnDs msg; return Nothing } ; Right (final_bndrs, _fn, args) -> do - { (spec_unf, unf_pairs) <- specUnfolding wrap_fn spec_ty (realIdUnfolding poly_id) + { (spec_unf, unf_pairs) <- specUnfolding spec_co spec_ty (realIdUnfolding poly_id) ; let spec_id = mkLocalId spec_name spec_ty `setInlinePragma` inl_prag @@ -540,7 +438,7 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl)) final_bndrs args (mkVarApps (Var spec_id) bndrs) - spec_rhs = wrap_fn poly_rhs + spec_rhs = dsHsWrapper spec_co poly_rhs spec_pair = makeCorePair spec_id False (dictArity bndrs) spec_rhs ; return (Just (spec_pair `consOL` unf_pairs, rule)) @@ -557,7 +455,7 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl)) | otherwise = pprPanic "dsImpSpecs" (ppr poly_id) -- The type checker has checked that it *has* an unfolding -specUnfolding :: (CoreExpr -> CoreExpr) -> Type +specUnfolding :: HsWrapper -> Type -> Unfolding -> DsM (Unfolding, OrdList (Id,CoreExpr)) {- [Dec 10: TEMPORARILY commented out, until we can straighten out how to generate unfoldings for specialised DFuns @@ -740,25 +638,138 @@ as the old one, but with an Internal name and no IdInfo. %************************************************************************ %* * - Desugaring coercions + Desugaring evidence %* * %************************************************************************ \begin{code} -dsHsWrapper :: HsWrapper -> DsM (CoreExpr -> CoreExpr) -dsHsWrapper WpHole = return (\e -> e) -dsHsWrapper (WpTyApp ty) = return (\e -> App e (Type ty)) -dsHsWrapper (WpLet ev_binds) = do { ds_ev_binds <- dsTcEvBinds ev_binds --- ; pprTrace "Desugared core bindings = " (vcat (map ppr ds_ev_binds)) $ - ; return (mkCoreLets ds_ev_binds) } -dsHsWrapper (WpCompose c1 c2) = do { k1 <- dsHsWrapper c1 - ; k2 <- dsHsWrapper c2 - ; return (k1 . k2) } -dsHsWrapper (WpCast co) - = return (\e -> dsLCoercion co (mkCast e)) -dsHsWrapper (WpEvLam ev) = return (\e -> Lam ev e) -dsHsWrapper (WpTyLam tv) = return (\e -> Lam tv e) -dsHsWrapper (WpEvApp evtrm) - = return (\e -> App e (dsEvTerm evtrm)) +dsHsWrapper :: HsWrapper -> CoreExpr -> CoreExpr +dsHsWrapper WpHole e = e +dsHsWrapper (WpTyApp ty) e = App e (Type ty) +dsHsWrapper (WpLet ev_binds) e = mkCoreLets (dsTcEvBinds ev_binds) e +dsHsWrapper (WpCompose c1 c2) e = dsHsWrapper c1 (dsHsWrapper c2 e) +dsHsWrapper (WpCast co) e = dsTcCoercion co (mkCast e) +dsHsWrapper (WpEvLam ev) e = Lam ev e +dsHsWrapper (WpTyLam tv) e = Lam tv e +dsHsWrapper (WpEvApp evtrm) e = App e (dsEvTerm evtrm) + +-------------------------------------- +dsTcEvBinds :: TcEvBinds -> [CoreBind] +dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds" -- Zonker has got rid of this +dsTcEvBinds (EvBinds bs) = dsEvBinds bs + +dsEvBinds :: Bag EvBind -> [CoreBind] +dsEvBinds bs = map ds_scc (sccEvBinds bs) + where + ds_scc (AcyclicSCC (EvBind v r)) = NonRec v (dsEvTerm r) + ds_scc (CyclicSCC bs) = Rec (map ds_pair bs) + + ds_pair (EvBind v r) = (v, dsEvTerm r) + +sccEvBinds :: Bag EvBind -> [SCC EvBind] +sccEvBinds bs = stronglyConnCompFromEdgedVertices edges + where + edges :: [(EvBind, EvVar, [EvVar])] + edges = foldrBag ((:) . mk_node) [] bs + + mk_node :: EvBind -> (EvBind, EvVar, [EvVar]) + mk_node b@(EvBind var term) = (b, var, evVarsOfTerm term) + + +--------------------------------------- +dsEvTerm :: EvTerm -> CoreExpr +dsEvTerm (EvId v) = Var v + +dsEvTerm (EvCast v co) + = dsTcCoercion co $ mkCast (Var v) -- 'v' is always a lifted evidence variable so it is + -- unnecessary to call varToCoreExpr v here. + +dsEvTerm (EvDFunApp df tys vars) = Var df `mkTyApps` tys `mkVarApps` vars +dsEvTerm (EvCoercion co) = dsTcCoercion co mkEqBox +dsEvTerm (EvTupleSel v n) + = ASSERT( isTupleTyCon tc ) + Case (Var v) (mkWildValBinder (varType v)) (tys !! n) [(DataAlt dc, xs, Var v')] + where + (tc, tys) = splitTyConApp (evVarPred v) + Just [dc] = tyConDataCons_maybe tc + v' = v `setVarType` ty_want + xs = map mkWildValBinder tys_before ++ v' : map mkWildValBinder tys_after + (tys_before, ty_want:tys_after) = splitAt n tys +dsEvTerm (EvTupleMk vs) = Var (dataConWorkId dc) `mkTyApps` tys `mkVarApps` vs + where dc = tupleCon ConstraintTuple (length vs) + tys = map varType vs +dsEvTerm (EvSuperClass d n) + = Var sc_sel_id `mkTyApps` tys `App` Var d + where + sc_sel_id = classSCSelId cls n -- Zero-indexed + (cls, tys) = getClassPredTys (evVarPred d) + +--------------------------------------- +dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> CoreExpr +-- This is the crucial function that moves +-- from LCoercions to Coercions; see Note [TcCoercions] in Coercion +-- e.g. dsTcCoercion (trans g1 g2) k +-- = case g1 of EqBox g1# -> +-- case g2 of EqBox g2# -> +-- k (trans g1# g2#) +dsTcCoercion co thing_inside + = foldr wrap_in_case result_expr eqvs_covs + where + result_expr = thing_inside (ds_tc_coercion subst co) + result_ty = exprType result_expr + + -- We use the same uniques for the EqVars and the CoVars, and just change + -- the type. So the CoVars shadow the EqVars + + eqvs_covs :: [(EqVar,CoVar)] + eqvs_covs = [(eqv, eqv `setIdType` mkCoercionType ty1 ty2) + | eqv <- varSetElems (coVarsOfTcCo co) + , let (ty1, ty2) = getEqPredTys (evVarPred eqv)] + + subst = mkCvSubst emptyInScopeSet [(eqv, mkCoVarCo cov) | (eqv, cov) <- eqvs_covs] + + wrap_in_case (eqv, cov) body + = Case (Var eqv) eqv result_ty [(DataAlt eqBoxDataCon, [cov], body)] + +ds_tc_coercion :: CvSubst -> 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) +-- No need for InScope set etc because the +ds_tc_coercion subst tc_co + = go tc_co + where + go (TcRefl ty) = Refl (Coercion.substTy subst ty) + go (TcTyConAppCo tc cos) = mkTyConAppCo tc (map go cos) + go (TcAppCo co1 co2) = mkAppCo (go co1) (go co2) + go (TcForAllCo tv co) = mkForAllCo tv' (ds_tc_coercion subst' co) + where + (subst', tv') = Coercion.substTyVarBndr subst tv + go (TcAxiomInstCo ax tys) = mkAxInstCo ax (map (Coercion.substTy subst) tys) + go (TcSymCo co) = mkSymCo (go co) + go (TcTransCo co1 co2) = mkTransCo (go co1) (go co2) + go (TcNthCo n co) = mkNthCo n (go co) + go (TcInstCo co ty) = mkInstCo (go co) ty + go (TcLetCo bs co) = ds_tc_coercion (ds_co_binds bs) co + go (TcCoVarCo v) = ds_ev_id subst v + + ds_co_binds :: TcEvBinds -> CvSubst + ds_co_binds (EvBinds bs) = foldl ds_scc subst (sccEvBinds bs) + ds_co_binds eb@(TcEvBinds {}) = pprPanic "ds_co_binds" (ppr eb) + + ds_scc :: CvSubst -> SCC EvBind -> CvSubst + ds_scc subst (AcyclicSCC (EvBind v ev_term)) + = extendCvSubstAndInScope subst v (ds_ev_term subst ev_term) + ds_scc _ (CyclicSCC other) = pprPanic "ds_scc:cyclic" (ppr other $$ ppr tc_co) + + ds_ev_term :: CvSubst -> EvTerm -> Coercion + ds_ev_term subst (EvCoercion tc_co) = ds_tc_coercion subst tc_co + ds_ev_term subst (EvId v) = ds_ev_id subst v + ds_ev_term _ other = pprPanic "ds_ev_term" (ppr other $$ ppr tc_co) + + ds_ev_id :: CvSubst -> EqVar -> Coercion + ds_ev_id subst v + | Just co <- Coercion.lookupCoVar subst v = co + | otherwise = pprPanic "ds_tc_coercion" (ppr v $$ ppr tc_co) \end{code} diff --git a/compiler/deSugar/DsExpr.lhs b/compiler/deSugar/DsExpr.lhs index 95645de5f2..a47e617a7c 100644 --- a/compiler/deSugar/DsExpr.lhs +++ b/compiler/deSugar/DsExpr.lhs @@ -31,8 +31,8 @@ import HsSyn -- NB: The desugarer, which straddles the source and Core worlds, sometimes -- needs to see source types import TcType +import TcEvidence import Type -import Coercion import CoreSyn import CoreUtils import CoreFVs @@ -79,8 +79,7 @@ dsValBinds (ValBindsIn _ _) _ = panic "dsValBinds ValBindsIn" ------------------------- dsIPBinds :: HsIPBinds Id -> CoreExpr -> DsM CoreExpr dsIPBinds (IPBinds ip_binds ev_binds) body - = do { ds_ev_binds <- dsTcEvBinds ev_binds - ; let inner = mkCoreLets ds_ev_binds body + = do { let inner = mkCoreLets (dsTcEvBinds ev_binds) body -- The dict bindings may not be in -- dependency order; hence Rec ; foldrM ds_ip_bind inner ip_binds } @@ -128,12 +127,11 @@ dsStrictBind (AbsBinds { abs_tvs = [], abs_ev_vars = [] , abs_exports = exports , abs_ev_binds = ev_binds , abs_binds = binds }) body - = do { ds_ev_binds <- dsTcEvBinds ev_binds - ; let body1 = foldr bind_export body exports + = do { let body1 = foldr bind_export body exports bind_export export b = bindNonRec (abe_poly export) (Var (abe_mono export)) b ; body2 <- foldlBagM (\body bind -> dsStrictBind (unLoc bind) body) body1 binds - ; return (mkCoreLets ds_ev_binds body2) } + ; return (mkCoreLets (dsTcEvBinds ev_binds) body2) } dsStrictBind (FunBind { fun_id = L _ fun, fun_matches = matches, fun_co_fn = co_fn , fun_tick = tick, fun_infix = inf }) body @@ -217,11 +215,11 @@ dsExpr (HsLit lit) = dsLit lit dsExpr (HsOverLit lit) = dsOverLit lit dsExpr (HsWrap co_fn e) - = do { co_fn' <- dsHsWrapper co_fn - ; e' <- dsExpr e + = do { e' <- dsExpr e + ; let wrapped_e = dsHsWrapper co_fn e' ; warn_id <- woptDs Opt_WarnIdentities - ; when warn_id $ warnAboutIdentities e' co_fn' - ; return (co_fn' e') } + ; when warn_id $ warnAboutIdentities e' wrapped_e + ; return wrapped_e } dsExpr (NegApp expr neg_expr) = App <$> dsExpr neg_expr <*> dsLExpr expr @@ -546,12 +544,12 @@ dsExpr expr@(RecordUpd record_expr (HsRecFields { rec_flds = fields }) -- Tediously wrap the application in a cast -- Note [Update for GADTs] - wrap_co = mkTyConAppCo tycon + wrap_co = mkTcTyConAppCo 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 -> mkReflCo ty - wrap_subst = mkVarEnv [ (tv, mkSymCo (mkEqVarLCo eq_var)) + Nothing -> mkTcReflCo ty + wrap_subst = mkVarEnv [ (tv, mkTcSymCo (mkTcCoVarCo eq_var)) | ((tv,_),eq_var) <- eq_spec `zip` eqs_vars ] pat = noLoc $ ConPatOut { pat_con = noLoc con, pat_tvs = ex_tvs @@ -806,14 +804,15 @@ mk_fail_msg pat = "Pattern match failure in do expression at " ++ %* * %************************************************************************ -Warn about functions that convert between one type and another -when the to- and from- types are the same. Then it's probably -(albeit not definitely) the identity +Warn about functions like toInteger, fromIntegral, that convert +between one type and another when the to- and from- types are the +same. Then it's probably (albeit not definitely) the identity + \begin{code} -warnAboutIdentities :: CoreExpr -> (CoreExpr -> CoreExpr) -> DsM () -warnAboutIdentities (Var v) co_fn +warnAboutIdentities :: CoreExpr -> CoreExpr -> DsM () +warnAboutIdentities (Var v) wrapped_fun | idName v `elem` conversionNames - , let fun_ty = exprType (co_fn (Var v)) + , let fun_ty = exprType wrapped_fun , Just (arg_ty, res_ty) <- splitFunTy_maybe fun_ty , arg_ty `eqType` res_ty -- So we are converting ty -> ty = warnDs (vcat [ ptext (sLit "Call of") <+> ppr v <+> dcolon <+> ppr fun_ty diff --git a/compiler/deSugar/DsListComp.lhs b/compiler/deSugar/DsListComp.lhs index 63d96fd465..4ad8006b39 100644 --- a/compiler/deSugar/DsListComp.lhs +++ b/compiler/deSugar/DsListComp.lhs @@ -19,6 +19,7 @@ import TcHsSyn import CoreSyn import MkCore +import TcEvidence import DsMonad -- the monadery used in the desugarer import DsUtils diff --git a/compiler/deSugar/Match.lhs b/compiler/deSugar/Match.lhs index 236a05bcb5..cd0153e3ac 100644 --- a/compiler/deSugar/Match.lhs +++ b/compiler/deSugar/Match.lhs @@ -22,6 +22,7 @@ import {-#SOURCE#-} DsExpr (dsLExpr) import DynFlags import HsSyn import TcHsSyn +import TcEvidence import Check import CoreSyn import Literal @@ -36,7 +37,6 @@ import DataCon import MatchCon import MatchLit import Type -import Coercion import TysWiredIn import ListSetOps import SrcLoc @@ -356,8 +356,7 @@ matchCoercion (var:vars) ty (eqns@(eqn1:_)) ; var' <- newUniqueId var (hsPatType pat) ; match_result <- match (var':vars) ty $ map (decomposeFirstPat getCoPat) eqns - ; co' <- dsHsWrapper co - ; let rhs' = co' (Var var) + ; let rhs' = dsHsWrapper co (Var var) ; return (mkCoLetMatchResult (NonRec var' rhs') match_result) } matchCoercion _ _ _ = panic "matchCoercion" @@ -919,7 +918,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2 -- equating different ways of writing a coercion) wrap WpHole WpHole = True wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2' - wrap (WpCast co) (WpCast co') = co `coreEqCoercion` co' + wrap (WpCast co) (WpCast co') = co `eq_co` co' wrap (WpEvApp et1) (WpEvApp et2) = et1 `ev_term` et2 wrap (WpTyApp t) (WpTyApp t') = eqType t t' -- Enhancement: could implement equality for more wrappers @@ -928,8 +927,8 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2 --------- ev_term :: EvTerm -> EvTerm -> Bool - ev_term (EvId a) (EvId b) = a==b - ev_term (EvCoercionBox a) (EvCoercionBox b) = coreEqCoercion a b + ev_term (EvId a) (EvId b) = a==b + ev_term (EvCoercion a) (EvCoercion b) = a `eq_co` b ev_term _ _ = False --------- @@ -939,6 +938,15 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2 eq_list _ (_:_) [] = False eq_list eq (x:xs) (y:ys) = eq x y && eq_list eq xs ys + --------- + 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 + eq_co _ _ = False + patGroup :: Pat Id -> PatGroup patGroup (WildPat {}) = PgAny patGroup (BangPat {}) = PgBang diff --git a/compiler/deSugar/MatchCon.lhs b/compiler/deSugar/MatchCon.lhs index 989008a5ca..f3b613fdbb 100644 --- a/compiler/deSugar/MatchCon.lhs +++ b/compiler/deSugar/MatchCon.lhs @@ -131,19 +131,18 @@ matchOneCon vars ty (eqn1 : eqns) -- All eqns for a single constructor match_group :: [Id] -> [(ConArgPats, EquationInfo)] -> DsM MatchResult -- All members of the group have compatible ConArgPats match_group arg_vars arg_eqn_prs - = do { (wraps, eqns') <- mapAndUnzipM shift arg_eqn_prs - ; let group_arg_vars = select_arg_vars arg_vars arg_eqn_prs + = do { let (wraps, eqns') = unzip (map shift arg_eqn_prs) + group_arg_vars = select_arg_vars arg_vars arg_eqn_prs ; match_result <- match (group_arg_vars ++ vars) ty eqns' ; return (adjustMatchResult (foldr1 (.) wraps) match_result) } shift (_, eqn@(EqnInfo { eqn_pats = ConPatOut{ pat_tvs = tvs, pat_dicts = ds, pat_binds = bind, pat_args = args } : pats })) - = do { ds_ev_binds <- dsTcEvBinds bind - ; return (wrapBinds (tvs `zip` tvs1) - . wrapBinds (ds `zip` dicts1) - . mkCoreLets ds_ev_binds, - eqn { eqn_pats = conArgPats arg_tys args ++ pats }) } + = ( wrapBinds (tvs `zip` tvs1) + . wrapBinds (ds `zip` dicts1) + . mkCoreLets (dsTcEvBinds bind) + , eqn { eqn_pats = conArgPats arg_tys args ++ pats }) shift (_, (EqnInfo { eqn_pats = ps })) = pprPanic "matchOneCon/shift" (ppr ps) -- Choose the right arg_vars in the right order for this group diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index a976efafd5..15b9943ecd 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -411,6 +411,7 @@ Library TcTyClsDecls TcTyDecls TcType + TcEvidence TcUnify TcInteract TcCanonical diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs index b6bc0c702b..bb8b337a00 100644 --- a/compiler/hsSyn/HsBinds.lhs +++ b/compiler/hsSyn/HsBinds.lhs @@ -27,7 +27,7 @@ import HsLit import HsTypes import PprCore () import CoreSyn -import Coercion +import TcEvidence import Type import Name import NameSet @@ -35,15 +35,11 @@ import BasicTypes import Outputable import SrcLoc import Util -import VarEnv import Var import Bag -import Unique import FastString -import Data.IORef( IORef ) import Data.Data hiding ( Fixity ) - import Data.List ( intersect ) \end{code} @@ -440,227 +436,6 @@ instance (OutputableBndr id) => Outputable (IPBind id) where %************************************************************************ %* * -\subsection{Coercion functions} -%* * -%************************************************************************ - -\begin{code} -data HsWrapper - = WpHole -- The identity coercion - - | WpCompose HsWrapper HsWrapper - -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]] - -- - -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) - -- But ([] a) `WpCompose` ([] b) = ([] b a) - - | WpCast LCoercion -- A cast: [] `cast` co - -- Guaranteed not the identity coercion - - -- Evidence abstraction and application - -- (both dictionaries and coercions) - | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable - | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint - - -- Kind and Type abstraction and application - | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var) - | WpTyApp KindOrType -- [] t the 't' is a type (not coercion) - - - | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings, - -- so that the identity coercion is always exactly WpHole - deriving (Data, Typeable) - - -data TcEvBinds - = TcEvBinds -- Mutable evidence bindings - EvBindsVar -- Mutable because they are updated "later" - -- when an implication constraint is solved - - | EvBinds -- Immutable after zonking - (Bag EvBind) - - deriving( Typeable ) - -data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique - -- The Unique is only for debug printing - ------------------ -newtype EvBindMap = EvBindMap { ev_bind_varenv :: VarEnv EvBind } -- Map from evidence variables to evidence terms - -emptyEvBindMap :: EvBindMap -emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv } - -extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap -extendEvBinds bs v t - = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) } - -lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind -lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs) - -evBindMapBinds :: EvBindMap -> Bag EvBind -evBindMapBinds bs - = foldVarEnv consBag emptyBag (ev_bind_varenv bs) - ------------------ -instance Data TcEvBinds where - -- Placeholder; we can't travers into TcEvBinds - toConstr _ = abstractConstr "TcEvBinds" - gunfold _ _ = error "gunfold" - dataTypeOf _ = mkNoRepType "TcEvBinds" - --- All evidence is bound by EvBinds; no side effects -data EvBind = EvBind EvVar EvTerm - -data EvTerm - = EvId EvId -- Term-level variable-to-variable bindings - -- (no coercion variables! they come via EvCoercionBox) - - | EvCoercionBox LCoercion -- (Boxed) coercion bindings - - | EvCast EvVar LCoercion -- d |> co - - | EvDFunApp DFunId -- Dictionary instance application - [Type] [EvVar] - - | EvTupleSel EvId Int -- n'th component of the tuple - - | EvTupleMk [EvId] -- tuple built from this stuff - - | EvSuperClass DictId Int -- n'th superclass. Used for both equalities and - -- dictionaries, even though the former have no - -- selector Id. We count up from _0_ - - deriving( Data, Typeable) -\end{code} - -Note [EvBinds/EvTerm] -~~~~~~~~~~~~~~~~~~~~~ -How evidence is created and updated. Bindings for dictionaries, -and coercions and implicit parameters are carried around in TcEvBinds -which during constraint generation and simplification is always of the -form (TcEvBinds ref). After constraint simplification is finished it -will be transformed to t an (EvBinds ev_bag). - -Evidence for coercions *SHOULD* be filled in using the TcEvBinds -However, all EvVars that correspond to *wanted* coercion terms in -an EvBind must be mutable variables so that they can be readily -inlined (by zonking) after constraint simplification is finished. - -Conclusion: a new wanted coercion variable should be made mutable. -[Notice though that evidence variables that bind coercion terms - from super classes will be "given" and hence rigid] - - -\begin{code} -mkEvCast :: EvVar -> LCoercion -> EvTerm -mkEvCast ev lco - | isReflCo lco = EvId ev - | otherwise = EvCast ev lco - -emptyTcEvBinds :: TcEvBinds -emptyTcEvBinds = EvBinds emptyBag - -isEmptyTcEvBinds :: TcEvBinds -> Bool -isEmptyTcEvBinds (EvBinds b) = isEmptyBag b -isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds" - -(<.>) :: HsWrapper -> HsWrapper -> HsWrapper -WpHole <.> c = c -c <.> WpHole = c -c1 <.> c2 = c1 `WpCompose` c2 - -mkWpTyApps :: [Type] -> HsWrapper -mkWpTyApps tys = mk_co_app_fn WpTyApp tys - -mkWpEvApps :: [EvTerm] -> HsWrapper -mkWpEvApps args = mk_co_app_fn WpEvApp args - -mkWpEvVarApps :: [EvVar] -> HsWrapper -mkWpEvVarApps vs = mkWpEvApps (map EvId vs) - -mkWpTyLams :: [TyVar] -> HsWrapper -mkWpTyLams ids = mk_co_lam_fn WpTyLam ids - -mkWpLams :: [Var] -> HsWrapper -mkWpLams ids = mk_co_lam_fn WpEvLam ids - -mkWpLet :: TcEvBinds -> HsWrapper --- This no-op is a quite a common case -mkWpLet (EvBinds b) | isEmptyBag b = WpHole -mkWpLet ev_binds = WpLet ev_binds - -mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper -mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as - -mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper --- For applications, the *first* argument must --- come *last* in the composition sequence -mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as - -idHsWrapper :: HsWrapper -idHsWrapper = WpHole - -isIdHsWrapper :: HsWrapper -> Bool -isIdHsWrapper WpHole = True -isIdHsWrapper _ = False -\end{code} - -Pretty printing - -\begin{code} -instance Outputable HsWrapper where - ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn - -pprHsWrapper :: SDoc -> HsWrapper -> SDoc --- In debug mode, print the wrapper --- otherwise just print what's inside -pprHsWrapper doc wrap - = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc) - where - help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc - -- True <=> appears in function application position - -- False <=> appears as body of let or lambda - help it WpHole = it - help it (WpCompose f1 f2) = help (help it f2) f1 - help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>") - <+> pprParendCo co)] - help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)] - help it (WpTyApp ty) = no_parens $ sep [it True, ptext (sLit "@") <+> pprParendType ty] - help it (WpEvLam id) = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False] - help it (WpTyLam tv) = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False] - help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False] - - pp_bndr v = pprBndr LambdaBind v <> dot - - add_parens, no_parens :: SDoc -> Bool -> SDoc - add_parens d True = parens d - add_parens d False = d - no_parens d _ = d - -instance Outputable TcEvBinds where - ppr (TcEvBinds v) = ppr v - ppr (EvBinds bs) = ptext (sLit "EvBinds") <> braces (ppr bs) - -instance Outputable EvBindsVar where - ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u) - -instance Outputable EvBind where - ppr (EvBind v e) = ppr v <+> equals <+> ppr e - -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing - -instance Outputable EvTerm where - ppr (EvId v) = ppr v - ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendCo co - ppr (EvCoercionBox co) = ptext (sLit "CO") <+> ppr co - ppr (EvTupleSel v n) = ptext (sLit "tupsel") <> parens (ppr (v,n)) - ppr (EvTupleMk vs) = ptext (sLit "tupmk") <+> ppr vs - ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n)) - ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ] -\end{code} - -%************************************************************************ -%* * \subsection{@Sig@: type signatures and value-modifying user pragmas} %* * %************************************************************************ diff --git a/compiler/hsSyn/HsExpr.lhs b/compiler/hsSyn/HsExpr.lhs index af2de9f87b..5a18fc6574 100644 --- a/compiler/hsSyn/HsExpr.lhs +++ b/compiler/hsSyn/HsExpr.lhs @@ -25,6 +25,7 @@ import HsTypes import HsBinds -- others: +import TcEvidence import CoreSyn import Var import Name diff --git a/compiler/hsSyn/HsPat.lhs b/compiler/hsSyn/HsPat.lhs index 236f211d42..3180d24152 100644 --- a/compiler/hsSyn/HsPat.lhs +++ b/compiler/hsSyn/HsPat.lhs @@ -29,6 +29,7 @@ import {-# SOURCE #-} HsExpr (SyntaxExpr, LHsExpr, pprLExpr) import HsBinds import HsLit import HsTypes +import TcEvidence import BasicTypes -- others: import PprCore ( {- instance OutputableBndr TyVar -} ) diff --git a/compiler/hsSyn/HsUtils.lhs b/compiler/hsSyn/HsUtils.lhs index 358f8bbc3e..234791d9fc 100644 --- a/compiler/hsSyn/HsUtils.lhs +++ b/compiler/hsSyn/HsUtils.lhs @@ -82,9 +82,9 @@ import HsPat import HsTypes import HsLit +import TcEvidence import RdrName import Var -import Coercion import TypeRep import DataCon import Name @@ -172,37 +172,6 @@ mkParPat :: LPat name -> LPat name mkParPat lp@(L loc p) | hsPatNeedsParens p = L loc (ParPat lp) | otherwise = lp ---------- HsWrappers: type args, dict args, casts --------- -mkLHsWrap :: HsWrapper -> LHsExpr id -> LHsExpr id -mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e) - -mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id -mkHsWrap co_fn e | isIdHsWrapper co_fn = e - | otherwise = HsWrap co_fn e - -mkHsWrapCo :: LCoercion -> HsExpr id -> HsExpr id -mkHsWrapCo (Refl _) e = e -mkHsWrapCo co e = mkHsWrap (WpCast co) e - -mkLHsWrapCo :: LCoercion -> LHsExpr id -> LHsExpr id -mkLHsWrapCo (Refl _) e = e -mkLHsWrapCo co (L loc e) = L loc (mkHsWrap (WpCast co) e) - -coToHsWrapper :: LCoercion -> HsWrapper -coToHsWrapper (Refl _) = idHsWrapper -coToHsWrapper co = WpCast co - -mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id -mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p - | otherwise = CoPat co_fn p ty - -mkHsWrapPatCo :: LCoercion -> Pat id -> Type -> Pat id -mkHsWrapPatCo (Refl _) pat _ = pat -mkHsWrapPatCo co pat ty = CoPat (WpCast co) pat ty - -mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id -mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr - ------------------------------- -- These are the bits of syntax that contain rebindable names @@ -404,6 +373,39 @@ missingTupArg :: HsTupArg a missingTupArg = Missing placeHolderType \end{code} +\begin{code} +--------- HsWrappers: type args, dict args, casts --------- +mkLHsWrap :: HsWrapper -> LHsExpr id -> LHsExpr id +mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e) + +mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id +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 + +mkLHsWrapCo :: TcCoercion -> LHsExpr id -> LHsExpr id +mkLHsWrapCo co (L loc e) | isTcReflCo co = L loc e + | otherwise = L loc (mkHsWrap (WpCast co) e) + +coToHsWrapper :: TcCoercion -> HsWrapper +coToHsWrapper co | isTcReflCo co = idHsWrapper + | otherwise = WpCast co + +mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id +mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p + | otherwise = CoPat co_fn p ty + +mkHsWrapPatCo :: TcCoercion -> Pat id -> Type -> Pat id +mkHsWrapPatCo co pat ty | isTcReflCo co = pat + | otherwise = CoPat (WpCast co) pat ty + +mkHsDictLet :: TcEvBinds -> LHsExpr Id -> LHsExpr Id +mkHsDictLet ev_binds expr = mkLHsWrap (mkWpLet ev_binds) expr +\end{code} +l %************************************************************************ %* * Bindings; with a location at the top diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs index c731b0aca6..7b82b11119 100644 --- a/compiler/main/GHC.hs +++ b/compiler/main/GHC.hs @@ -262,7 +262,7 @@ import Packages import NameSet import RdrName import qualified HsSyn -- hack as we want to reexport the whole module -import HsSyn hiding ((<.>)) +import HsSyn import Type hiding( typeKind ) import Kind ( synTyConResKind ) import TcType hiding( typeKind ) diff --git a/compiler/main/GhcMake.hs b/compiler/main/GhcMake.hs index abbaa1fb75..3db920553e 100644 --- a/compiler/main/GhcMake.hs +++ b/compiler/main/GhcMake.hs @@ -38,7 +38,7 @@ import Module import HscTypes import ErrUtils import DynFlags -import HsSyn hiding ((<.>)) +import HsSyn import Finder import HeaderInfo import TcIface ( typecheckIface ) diff --git a/compiler/parser/Parser.y.pp b/compiler/parser/Parser.y.pp index 8a57504e68..855a428798 100644 --- a/compiler/parser/Parser.y.pp +++ b/compiler/parser/Parser.y.pp @@ -32,6 +32,7 @@ import RdrHsSyn import HscTypes ( IsBootInterface, WarningTxt(..) ) import Lexer import RdrName +import TcEvidence ( emptyTcEvBinds ) import TysPrim ( liftedTypeKindTyConName, eqPrimTyCon ) import TysWiredIn ( unitTyCon, unitDataCon, tupleTyCon, tupleCon, nilDataCon, unboxedSingletonTyCon, unboxedSingletonDataCon, diff --git a/compiler/parser/RdrHsSyn.lhs b/compiler/parser/RdrHsSyn.lhs index 3b1a289fd2..10e731b3e0 100644 --- a/compiler/parser/RdrHsSyn.lhs +++ b/compiler/parser/RdrHsSyn.lhs @@ -54,6 +54,7 @@ import RdrName ( RdrName, isRdrTyVar, isRdrTc, mkUnqual, rdrNameOcc, import Name ( Name ) import BasicTypes ( maxPrecedence, Activation(..), RuleMatchInfo, InlinePragma(..), InlineSpec(..) ) +import TcEvidence ( idHsWrapper ) import Lexer import TysWiredIn ( unitTyCon ) import ForeignCall diff --git a/compiler/rename/RnBinds.lhs b/compiler/rename/RnBinds.lhs index 51cd09fb07..0da8070438 100644 --- a/compiler/rename/RnBinds.lhs +++ b/compiler/rename/RnBinds.lhs @@ -35,6 +35,7 @@ import {-# SOURCE #-} RnExpr( rnLExpr, rnStmts ) import HsSyn import RnHsSyn import TcRnMonad +import TcEvidence ( emptyTcEvBinds ) import RnTypes ( rnIPName, rnHsSigType, rnLHsType, checkPrecMatch ) import RnPat import RnEnv diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 40d0d2b3c5..34f68182ec 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -48,6 +48,7 @@ import HsSyn import TcHsSyn import TcRnMonad import TcEnv +import TcEvidence import InstEnv import FunDeps import TcMType @@ -223,7 +224,7 @@ instCallConstraints origin (pred : preds) = do { traceTc "instCallConstraints" $ ppr (mkEqPred (ty1, ty2)) ; co <- unifyType ty1 ty2 ; co_fn <- instCallConstraints origin preds - ; return (co_fn <.> WpEvApp (EvCoercionBox co)) } + ; return (co_fn <.> WpEvApp (EvCoercion co)) } | otherwise = do { ev_var <- emitWanted origin pred diff --git a/compiler/typecheck/TcArrows.lhs b/compiler/typecheck/TcArrows.lhs index e6943ea4ca..f58c566369 100644 --- a/compiler/typecheck/TcArrows.lhs +++ b/compiler/typecheck/TcArrows.lhs @@ -25,7 +25,7 @@ import TcPat import TcUnify import TcRnMonad import TcEnv -import Coercion +import TcEvidence import Id( mkLocalId ) import Inst import Name @@ -50,7 +50,7 @@ import Control.Monad \begin{code} tcProc :: InPat Name -> LHsCmdTop Name -- proc pat -> expr -> TcRhoType -- Expected type of whole proc expression - -> TcM (OutPat TcId, LHsCmdTop TcId, LCoercion) + -> TcM (OutPat TcId, LHsCmdTop TcId, TcCoercion) tcProc pat cmd exp_ty = newArrowScope $ @@ -59,7 +59,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 [] res_ty - ; let res_co = mkTransCo co (mkAppCo co1 (mkReflCo res_ty)) + ; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcReflCo res_ty)) ; return (pat', cmd', res_co) } \end{code} diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs index 9f5257ad38..5e128c7613 100644 --- a/compiler/typecheck/TcBinds.lhs +++ b/compiler/typecheck/TcBinds.lhs @@ -21,6 +21,7 @@ import TcRnMonad import TcEnv import TcUnify import TcSimplify +import TcEvidence import TcHsType import TcPat import TcMType diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index d13b793db6..f2b652722a 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -24,7 +24,7 @@ import qualified TcMType as TcM import TcType import Type import Kind -import Coercion +import TcEvidence import Class import TyCon import TypeRep @@ -38,7 +38,6 @@ import Control.Applicative ( (<|>) ) import TrieMap import VarSet -import HsBinds import TcSMonad import FastString @@ -257,7 +256,7 @@ canIP d fl v nm ty -- possible in principle to not flatten, but since flattening applies -- the inert substitution we choose to flatten anyway. do { (xi,co) <- flatten d fl (mkIPPred nm ty) - ; let no_flattening = isReflCo co + ; let no_flattening = isTcReflCo co ; if no_flattening then let IPPred _ xi_in = classifyPredType xi in continueWith $ CIPCan { cc_id = v, cc_flavor = fl @@ -268,7 +267,7 @@ canIP d fl v nm ty IPPred _ ip_xi = classifyPredType xi ; fl_new <- case fl of Wanted {} -> setEvBind v (EvCast v_new co) fl - Given {} -> setEvBind v_new (EvCast v (mkSymCo co)) fl + Given {} -> setEvBind v_new (EvCast v (mkTcSymCo co)) fl Derived {} -> return fl ; if isNewEvVar evc then continueWith $ CIPCan { cc_id = v_new @@ -301,10 +300,10 @@ canClass :: SubGoalDepth -- Depth canClass d fl v cls tys = do { -- sctx <- getTcSContext ; (xis, cos) <- flattenMany d fl tys - ; let co = mkTyConAppCo (classTyCon cls) cos + ; let co = mkTcTyConAppCo (classTyCon cls) cos xi = mkClassPred cls xis - ; let no_flattening = all isReflCo cos + ; let no_flattening = all isTcReflCo cos -- No flattening, continue with canonical ; if no_flattening then continueWith $ CDictCan { cc_id = v, cc_flavor = fl @@ -315,7 +314,7 @@ canClass d fl v cls tys ; let v_new = evc_the_evvar evc ; fl_new <- case fl of Wanted {} -> setEvBind v (EvCast v_new co) fl - Given {} -> setEvBind v_new (EvCast v (mkSymCo co)) fl + Given {} -> setEvBind v_new (EvCast v (mkTcSymCo co)) fl Derived {} -> return fl -- Continue only if flat constraint is new ; if isNewEvVar evc then @@ -463,7 +462,7 @@ canIrred d fl v ty ; (xi,co) <- flatten d fl ty -- co :: xi ~ ty ; let no_flattening = xi `eqType` ty -- In this particular case it is not safe to - -- say 'isReflCo' because the new constraint may + -- say 'isTcReflCo' because the new constraint may -- be reducible! ; if no_flattening then continueWith $ CIrredEvCan { cc_id = v, cc_flavor = fl @@ -476,7 +475,7 @@ canIrred d fl v ty ; let v' = evc_the_evvar evc ; fl' <- case fl of Wanted {} -> setEvBind v (EvCast v' co) fl - Given {} -> setEvBind v' (EvCast v (mkSymCo co)) fl + Given {} -> setEvBind v' (EvCast v (mkTcSymCo co)) fl Derived {} -> return fl ; if isNewEvVar evc then @@ -536,7 +535,7 @@ unexpanded synonym. -- Flatten a bunch of types all at once. flattenMany :: SubGoalDepth -- Depth - -> CtFlavor -> [Type] -> TcS ([Xi], [LCoercion]) + -> CtFlavor -> [Type] -> TcS ([Xi], [TcCoercion]) -- Coercions :: Xi ~ Type -- Returns True iff (no flattening happened) flattenMany d ctxt tys @@ -551,7 +550,7 @@ flattenMany d ctxt tys -- the new type-function-free type, and a collection of new equality -- constraints. See Note [Flattening] for more detail. flatten :: SubGoalDepth -- Depth - -> CtFlavor -> TcType -> TcS (Xi, LCoercion) + -> CtFlavor -> TcType -> TcS (Xi, TcCoercion) -- Postcondition: Coercion :: Xi ~ TcType flatten d ctxt ty | Just ty' <- tcView ty @@ -561,21 +560,21 @@ flatten d ctxt ty -- DV: The following is tedious to do but maybe we should return to this -- Preserve type synonyms if possible -- ; if no_flattening - -- then return (xi, mkReflCo xi,no_flattening) -- Importantly, not xi! + -- then return (xi, mkTcReflCo xi,no_flattening) -- Importantly, not xi! -- else return (xi,co,no_flattening) -- } flatten d ctxt v@(TyVarTy _) = do { ieqs <- getInertEqs ; let co = liftInertEqsTy ieqs ctxt v -- co : v ~ ty - ty = pSnd (liftedCoercionKind co) + ty = pSnd (tcCoercionKind co) ; if v `eqType` ty then - return (ty,mkReflCo ty) + return (ty,mkTcReflCo ty) else -- NB recursive call. Why? See Note [Non-idempotent inert substitution] -- Actually I believe that applying the substition only *twice* will suffice do { (ty_final,co') <- flatten d ctxt ty -- co' : ty_final ~ ty - ; return (ty_final,co' `mkTransCo` mkSymCo co) } } + ; return (ty_final,co' `mkTcTransCo` mkTcSymCo co) } } \end{code} @@ -613,19 +612,19 @@ This insufficient rewriting was the reason for #5668. flatten d ctxt (AppTy ty1 ty2) = do { (xi1,co1) <- flatten d ctxt ty1 ; (xi2,co2) <- flatten d ctxt ty2 - ; return (mkAppTy xi1 xi2, mkAppCo co1 co2) } + ; return (mkAppTy xi1 xi2, mkTcAppCo co1 co2) } flatten d ctxt (FunTy ty1 ty2) = do { (xi1,co1) <- flatten d ctxt ty1 ; (xi2,co2) <- flatten d ctxt ty2 - ; return (mkFunTy xi1 xi2, mkFunCo co1 co2) } + ; return (mkFunTy xi1 xi2, mkTcFunCo co1 co2) } flatten d fl (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 d fl tys - ; return (mkTyConApp tc xis, mkTyConAppCo tc cos) } + ; return (mkTyConApp tc xis, mkTcTyConAppCo 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 @@ -648,7 +647,7 @@ flatten d fl (TyConApp tc tys) | isGivenOrSolved fl -> do { rhs_xi_var <- newFlattenSkolemTy fam_ty ; (fl',eqv) - <- newGivenEqVar fl fam_ty rhs_xi_var (mkReflCo fam_ty) + <- newGivenEqVar fl fam_ty rhs_xi_var (mkTcReflCo fam_ty) ; let ct = CFunEqCan { cc_id = eqv , cc_flavor = fl' -- Given , cc_fun = tc @@ -657,7 +656,7 @@ flatten d fl (TyConApp tc tys) , cc_depth = d } -- Update the flat cache: just an optimisation! ; updateFlatCache eqv fl' tc xi_args rhs_xi_var WhileFlattening - ; return (mkEqVarLCo eqv, rhs_xi_var, [ct]) } + ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) } | otherwise -> -- Derived or Wanted: make a new /unification/ flatten variable do { rhs_xi_var <- newFlexiTcSTy (typeKind fam_ty) @@ -673,7 +672,7 @@ flatten d fl (TyConApp tc tys) , cc_depth = d } -- Update the flat cache: just an optimisation! ; updateFlatCache eqv fl tc xi_args rhs_xi_var WhileFlattening - ; return (mkEqVarLCo eqv, rhs_xi_var, [ct]) } } + ; return (mkTcCoVarCo eqv, rhs_xi_var, [ct]) } } -- Emit the flat constraints ; updWorkListTcS $ appendWorkListEqs ct @@ -681,8 +680,8 @@ flatten d fl (TyConApp tc tys) ; let (cos_args, cos_rest) = splitAt (tyConArity tc) cos ; return ( mkAppTys rhs_xi xi_rest -- NB mkAppTys: rhs_xi might not be a type variable -- cf Trac #5655 - , foldl AppCo (mkSymCo ret_co `mkTransCo` mkTyConAppCo tc cos_args) - cos_rest + , mkTcAppCos (mkTcSymCo ret_co `mkTcTransCo` mkTcTyConAppCo tc cos_args) + cos_rest ) } @@ -692,7 +691,7 @@ flatten d ctxt ty@(ForAllTy {}) = do { let (tvs, rho) = splitForAllTys ty ; when (under_families tvs rho) $ flattenForAllErrorTcS ctxt ty ; (rho', co) <- flatten d ctxt rho - ; return (mkForAllTys tvs rho', foldr mkForAllCo co tvs) } + ; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) } where under_families tvs rho = go (mkVarSet tvs) rho @@ -709,7 +708,7 @@ flatten d ctxt ty@(ForAllTy {}) getCachedFlatEq :: TyCon -> [Xi] -> CtFlavor -> FlatEqOrigin - -> TcS (Maybe (Xi,Coercion)) + -> TcS (Maybe (Xi, TcCoercion)) -- Returns a coercion between (TyConApp tc xi_args ~ xi) if such an inert item exists -- But also applies the substitution to the item via calling flatten recursively getCachedFlatEq tc xi_args fl feq_origin @@ -731,7 +730,7 @@ getCachedFlatEq tc xi_args fl feq_origin -- The only purpose of this flattening is to apply the -- inert substitution (since everything in the flat cache -- by construction will have a family-free RHS. - ; return $ Just (xi'', co' `mkTransCo` (mkSymCo co)) } + ; return $ Just (xi'', co' `mkTcTransCo` (mkTcSymCo co)) } _ -> do { traceTcS "getCachedFlatEq" $ text "failure!" <+> pprEvVarCache flat_cache ; return Nothing } @@ -769,7 +768,7 @@ canEq _d fl eqv ty1 ty2 | eqType ty1 ty2 -- Dealing with equality here avoids -- later spurious occurs checks for a~a = do { when (isWanted fl) $ - do { _ <- setEqBind eqv (mkReflCo ty1) fl; return () } + do { _ <- setEqBind eqv (mkTcReflCo ty1) fl; return () } ; return Stop } -- Split up an equality between function types into two equalities. @@ -780,11 +779,11 @@ canEq d fl eqv (FunTy s1 t1) (FunTy s2 t2) reseqv_v = evc_the_evvar reseqv ; (fl1,fl2) <- case fl of Wanted {} -> - do { _ <- setEqBind eqv (mkFunCo (mkEqVarLCo argeqv_v) (mkEqVarLCo reseqv_v)) fl + do { _ <- setEqBind eqv (mkTcFunCo (mkTcCoVarCo argeqv_v) (mkTcCoVarCo reseqv_v)) fl ; return (fl,fl) } Given {} -> - do { fl1 <- setEqBind argeqv_v (mkNthCo 0 (mkEqVarLCo eqv)) fl - ; fl2 <- setEqBind reseqv_v (mkNthCo 1 (mkEqVarLCo eqv)) fl + do { fl1 <- setEqBind argeqv_v (mkTcNthCo 0 (mkTcCoVarCo eqv)) fl + ; fl2 <- setEqBind reseqv_v (mkTcNthCo 1 (mkTcCoVarCo eqv)) fl ; return (fl1,fl2) } Derived {} -> @@ -814,17 +813,17 @@ canEq d fl eqv (TyConApp tc1 tys1) (TyConApp tc2 tys2) = -- Generate equalities for each of the corresponding arguments do { let (kis1, tys1') = span isKind tys1 (_kis2, tys2') = span isKind tys2 - ; let kicos = map mkReflCo kis1 + ; let kicos = map mkTcReflCo kis1 ; argeqvs <- zipWithM (newEqVar fl) tys1' tys2' ; fls <- case fl of Wanted {} -> do { _ <- setEqBind eqv - (mkTyConAppCo tc1 (kicos ++ map (mkEqVarLCo . evc_the_evvar) argeqvs)) fl + (mkTcTyConAppCo tc1 (kicos ++ map (mkTcCoVarCo . evc_the_evvar) argeqvs)) fl ; return (map (\_ -> fl) argeqvs) } Given {} -> let do_one argeqv n = setEqBind (evc_the_evvar argeqv) - (mkNthCo n (mkEqVarLCo eqv)) fl + (mkTcNthCo n (mkTcCoVarCo eqv)) fl in zipWithM do_one argeqvs [(length kicos)..] Derived {} -> return (map (\_ -> fl) argeqvs) @@ -852,7 +851,7 @@ canEq d fl eqv ty1 ty2 eqv2 = evc_the_evvar evc2 ; when (isWanted fl) $ - do { _ <- setEqBind eqv (mkAppCo (mkEqVarLCo eqv1) (mkEqVarLCo eqv2)) fl + do { _ <- setEqBind eqv (mkTcAppCo (mkTcCoVarCo eqv1) (mkTcCoVarCo eqv2)) fl ; return () } ; canEqEvVarsCreated d [fl,fl] [evc1,evc2] [s1,t1] [s2,t2] } @@ -1087,8 +1086,8 @@ canEqLeaf d fl eqv s1 s2 ; evc <- newEqVar fl s2 s1 ; let eqv' = evc_the_evvar evc ; fl' <- case fl of - Wanted {} -> setEqBind eqv (mkSymCo (mkEqVarLCo eqv')) fl - Given {} -> setEqBind eqv' (mkSymCo (mkEqVarLCo eqv)) fl + Wanted {} -> setEqBind eqv (mkTcSymCo (mkTcCoVarCo eqv')) fl + Given {} -> setEqBind eqv' (mkTcSymCo (mkTcCoVarCo eqv)) fl Derived {} -> return fl ; if isNewEvVar evc then do { canEqLeafOriented d fl' eqv' s2 s1 } @@ -1151,7 +1150,7 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2 ; let is_cached = {-# SCC "lookupFunEq" #-} lookupFunEq flat_ty fl fam_eqs -} - ; let no_flattening = all isReflCo cos1 + ; let no_flattening = all isTcReflCo cos1 ; if no_flattening && isNothing is_cached then canEqLeafFunEqLeft d fl eqv (fn,xis1) ty2 @@ -1159,19 +1158,19 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2 { let (final_co, final_ty) | no_flattening -- Just in inerts , Just (rhs_ty, ret_eq) <- is_cached - = (mkSymCo ret_eq, rhs_ty) + = (mkTcSymCo ret_eq, rhs_ty) | Nothing <- is_cached -- Just flattening - = (mkTyConAppCo fn cos1, flat_ty) + = (mkTcTyConAppCo fn cos1, flat_ty) | Just (rhs_ty, ret_eq) <- is_cached -- Both - = (mkSymCo ret_eq `mkTransCo` mkTyConAppCo fn cos1, rhs_ty) + = (mkTcSymCo ret_eq `mkTcTransCo` mkTcTyConAppCo fn cos1, rhs_ty) | otherwise = panic "No flattening and not cached!" ; delCachedEvVar eqv fl ; evc <- newEqVar fl final_ty ty2 ; let new_eqv = evc_the_evvar evc ; fl' <- case fl of Wanted {} -> setEqBind eqv - (mkSymCo final_co `mkTransCo` (mkEqVarLCo new_eqv)) fl - Given {} -> setEqBind new_eqv (final_co `mkTransCo` (mkEqVarLCo eqv)) fl + (mkTcSymCo final_co `mkTcTransCo` (mkTcCoVarCo new_eqv)) fl + Given {} -> setEqBind new_eqv (final_co `mkTcTransCo` (mkTcCoVarCo eqv)) fl Derived {} -> return fl ; if isNewEvVar evc then if isNothing is_cached then @@ -1183,12 +1182,12 @@ canEqLeafFunEqLeftRec d fl eqv (fn,tys1) ty2 -- eqv :: F tys1 ~ ty2 } } -lookupFunEq :: PredType -> CtFlavor -> TypeMap Ct -> Maybe (TcType,Coercion) +lookupFunEq :: PredType -> CtFlavor -> TypeMap Ct -> Maybe (TcType, TcCoercion) lookupFunEq pty fl fam_eqs = lookup_funeq pty fam_eqs where lookup_funeq pty fam_eqs | Just ct <- lookupTM pty fam_eqs , cc_flavor ct `canRewrite` fl - = Just (cc_rhs ct, mkEqVarLCo (cc_id ct)) + = Just (cc_rhs ct, mkTcCoVarCo (cc_id ct)) | otherwise = Nothing @@ -1202,7 +1201,7 @@ canEqLeafFunEqLeft d fl eqv (fn,xis1) s2 ; (xi2,co2) <- {-# SCC "flatten" #-} flatten d fl s2 -- co2 :: xi2 ~ s2 - ; let no_flattening_happened = isReflCo co2 + ; let no_flattening_happened = isTcReflCo co2 ; if no_flattening_happened then continueWith $ CFunEqCan { cc_id = eqv , cc_flavor = fl @@ -1215,11 +1214,11 @@ canEqLeafFunEqLeft d fl eqv (fn,xis1) s2 {-# SCC "newEqVar" #-} newEqVar fl (mkTyConApp fn xis1) xi2 ; let new_eqv = evc_the_evvar evc -- F xis1 ~ xi2 - new_cv = mkEqVarLCo new_eqv - cv = mkEqVarLCo eqv -- F xis1 ~ s2 + new_cv = mkTcCoVarCo new_eqv + cv = mkTcCoVarCo eqv -- F xis1 ~ s2 ; fl' <- case fl of - Wanted {} -> setEqBind eqv (new_cv `mkTransCo` co2) fl - Given {} -> setEqBind new_eqv (cv `mkTransCo` mkSymCo co2) fl + Wanted {} -> setEqBind eqv (new_cv `mkTcTransCo` co2) fl + Given {} -> setEqBind new_eqv (cv `mkTcTransCo` mkTcSymCo co2) fl Derived {} -> return fl ; if isNewEvVar evc then do { continueWith $ @@ -1238,7 +1237,7 @@ canEqLeafTyVarLeftRec :: SubGoalDepth canEqLeafTyVarLeftRec d fl eqv tv s2 -- eqv :: tv ~ s2 = do { traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2 ; (xi1,co1) <- flatten d fl (mkTyVarTy tv) -- co1 :: xi1 ~ tv - ; case isReflCo co1 of + ; case isTcReflCo co1 of True -- If reflco and variable, just go on | Just tv' <- getTyVar_maybe xi1 -> canEqLeafTyVarLeft d fl eqv tv' s2 @@ -1248,9 +1247,9 @@ canEqLeafTyVarLeftRec d fl eqv tv s2 -- eqv :: tv ~ s2 ; let new_ev = evc_the_evvar evc ; fl' <- case fl of Wanted {} -> setEqBind eqv - (mkSymCo co1 `mkTransCo` mkEqVarLCo new_ev) fl + (mkTcSymCo co1 `mkTcTransCo` mkTcCoVarCo new_ev) fl Given {} -> setEqBind new_ev - (co1 `mkTransCo` mkEqVarLCo eqv) fl + (co1 `mkTcTransCo` mkTcCoVarCo eqv) fl Derived {} -> return fl ; if isNewEvVar evc then do { canEq d fl' new_ev xi1 s2 } @@ -1266,7 +1265,7 @@ canEqLeafTyVarLeft d fl eqv tv s2 -- eqv : tv ~ s2 = do { traceTcS "canEqLeafTyVarLeft" (pprEq (mkTyVarTy tv) s2) ; (xi2, co) <- flatten d fl s2 -- Flatten RHS co : xi2 ~ s2 - ; let no_flattening_happened = isReflCo co + ; let no_flattening_happened = isTcReflCo co ; traceTcS "canEqLeafTyVarLeft" (nest 2 (vcat [ text "tv =" <+> ppr tv , text "s2 =" <+> ppr s2 @@ -1309,11 +1308,11 @@ canEqLeafTyVarLeft d fl eqv tv s2 -- eqv : tv ~ s2 do { delCachedEvVar eqv fl ; evc <- newEqVar fl (mkTyVarTy tv) xi2' ; let eqv' = evc_the_evvar evc -- eqv' : tv ~ xi2' - cv = mkEqVarLCo eqv -- cv : tv ~ s2 - cv' = mkEqVarLCo eqv' -- cv': tv ~ xi2' + cv = mkTcCoVarCo eqv -- cv : tv ~ s2 + cv' = mkTcCoVarCo eqv' -- cv': tv ~ xi2' ; fl' <- case fl of - Wanted {} -> setEqBind eqv (cv' `mkTransCo` co) fl -- tv ~ xi2' ~ s2 - Given {} -> setEqBind eqv' (cv `mkTransCo` mkSymCo co) fl -- tv ~ s2 ~ xi2' + Wanted {} -> setEqBind eqv (cv' `mkTcTransCo` co) fl -- tv ~ xi2' ~ s2 + Given {} -> setEqBind eqv' (cv `mkTcTransCo` mkTcSymCo co) fl -- tv ~ s2 ~ xi2' Derived {} -> return fl ; if isNewEvVar evc then @@ -1499,7 +1498,7 @@ now!). rewriteWithFunDeps :: [Equation] -> [Xi] -> WantedLoc - -> TcS (Maybe ([Xi], [LCoercion], [(EvVar,WantedLoc)])) + -> TcS (Maybe ([Xi], [TcCoercion], [(EvVar,WantedLoc)])) -- Not quite a WantedEvVar unfortunately -- Because our intention could be to make -- it derived at the end of the day @@ -1552,14 +1551,14 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env rewriteDictParams :: [(Int,(EqVar,WantedLoc))] -- A set of coercions : (pos, ty' ~ ty) -> [Type] -- A sequence of types: tys - -> [(Type,LCoercion)] -- Returns: [(ty', co : ty' ~ ty)] + -> [(Type, TcCoercion)] -- Returns: [(ty', co : ty' ~ ty)] rewriteDictParams param_eqs tys = zipWith do_one tys [0..] where - do_one :: Type -> Int -> (Type,LCoercion) + do_one :: Type -> Int -> (Type, TcCoercion) do_one ty n = case lookup n param_eqs of - Just wev -> (get_fst_ty wev, mkEqVarLCo (fst wev)) - Nothing -> (ty, mkReflCo ty) -- Identity + Just wev -> (get_fst_ty wev, mkTcCoVarCo (fst wev)) + Nothing -> (ty, mkTcReflCo ty) -- Identity get_fst_ty (wev,_wloc) | Just (ty1, _) <- getEqPredTys_maybe (evVarPred wev ) diff --git a/compiler/typecheck/TcClassDcl.lhs b/compiler/typecheck/TcClassDcl.lhs index 68f27148b6..77f1c42982 100644 --- a/compiler/typecheck/TcClassDcl.lhs +++ b/compiler/typecheck/TcClassDcl.lhs @@ -24,6 +24,7 @@ module TcClassDcl ( tcClassSigs, tcClassDecl2, import HsSyn import TcEnv import TcPat( addInlinePrags ) +import TcEvidence( idHsWrapper ) import TcBinds import TcUnify import TcHsType diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index 4fdb92fb29..fc5787c014 100644 --- a/compiler/typecheck/TcDeriv.lhs +++ b/compiler/typecheck/TcDeriv.lhs @@ -32,6 +32,7 @@ import FamInstEnv import TcHsType import TcMType import TcSimplify +import TcEvidence import RnBinds import RnEnv @@ -40,7 +41,6 @@ import HscTypes import Class import Type -import Coercion import ErrUtils import MkId import DataCon @@ -1443,7 +1443,7 @@ genInst :: Bool -- True <=> standalone deriving -> OverlapFlag -> DerivSpec -> TcM (InstInfo RdrName, BagDerivStuff) genInst standalone_deriv oflag - spec@(DS { ds_tc = rep_tycon, ds_tc_args = rep_tc_args + spec@(DS { ds_tvs = tvs, ds_tc = rep_tycon, ds_tc_args = rep_tc_args , ds_theta = theta, ds_newtype = is_newtype , ds_name = name, ds_cls = clas }) | is_newtype @@ -1462,12 +1462,12 @@ genInst standalone_deriv oflag inst_spec = mkInstance oflag theta spec co1 = case tyConFamilyCoercion_maybe rep_tycon of - Just co_con -> mkAxInstCo co_con rep_tc_args + Just co_con -> mkTcAxInstCo co_con rep_tc_args Nothing -> id_co -- Not a family => rep_tycon = main tycon - co2 = mkAxInstCo (newTyConCo rep_tycon) rep_tc_args - co = co1 `mkTransCo` co2 - id_co = mkReflCo (mkTyConApp rep_tycon rep_tc_args) + co2 = mkTcAxInstCo (newTyConCo rep_tycon) rep_tc_args + co = mkTcForAllCos tvs (co1 `mkTcTransCo` co2) + id_co = mkTcReflCo (mkTyConApp rep_tycon rep_tc_args) -- Example: newtype instance N [a] = N1 (Tree a) -- deriving instance Eq b => Eq (N [(b,b)]) diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs index 4fe7ee1b93..5c2c895866 100644 --- a/compiler/typecheck/TcEnv.lhs +++ b/compiler/typecheck/TcEnv.lhs @@ -60,7 +60,7 @@ import TcIface import PrelNames import TysWiredIn import Id -import Coercion +import TcEvidence import Var import VarSet import RdrName @@ -629,10 +629,10 @@ data InstBindings a -- witness dictionary is identical to the argument -- dictionary. Hence no bindings, no pragmas. - Coercion -- The coercion maps from newtype to the representation type - -- (mentioning type variables bound by the forall'd iSpec variables) + TcCoercion -- The coercion maps from newtype to the representation type + -- (quantified over type variables bound by the forall'd iSpec variables) -- E.g. newtype instance N [a] = N1 (Tree a) - -- co : N [a] ~ Tree a + -- co : forall a. N [a] ~ Tree a TyCon -- The TyCon is the newtype N. If it's indexed, then it's the -- representation TyCon, so that tyConDataCons returns [N1], diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs new file mode 100644 index 0000000000..0511aa1051 --- /dev/null +++ b/compiler/typecheck/TcEvidence.lhs @@ -0,0 +1,570 @@ +%
+% (c) The University of Glasgow 2006
+%
+
+\begin{code}
+module TcEvidence (
+
+ -- HsWrapper
+ HsWrapper(..),
+ (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet,
+ idHsWrapper, isIdHsWrapper, pprHsWrapper,
+
+ -- Evidence bindin
+ TcEvBinds(..), EvBindsVar(..),
+ EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,
+
+ EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds,
+
+ EvTerm(..), mkEvCast, evVarsOfTerm,
+
+ -- TcCoercion
+ TcCoercion(..),
+ mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
+ mkTcAxInstCo, mkTcForAllCo, mkTcForAllCos,
+ mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcInstCos,
+ tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
+ isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,
+ liftTcCoSubstWith
+
+ ) where
+#include "HsVersions.h"
+
+import Var
+
+import PprCore () -- Instance OutputableBndr TyVar
+import TypeRep -- Knows type representation
+import TcType
+import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe )
+import TysPrim( funTyCon )
+import TyCon
+import PrelNames
+import VarEnv
+import VarSet
+import Name
+
+import Util
+import Bag
+import Pair
+import Control.Applicative
+import Data.Traversable (traverse, sequenceA)
+import qualified Data.Data as Data
+import Outputable
+import FastString
+import Data.IORef( IORef )
+\end{code}
+
+
+Note [TcCoercions]
+~~~~~~~~~~~~~~~~~~
+| LCoercions are a hack used by the typechecker. Normally,
+Coercions have free variables of type (a ~# b): we call these
+CoVars. However, the type checker passes around equality evidence
+(boxed up) at type (a ~ b).
+
+An LCoercion is simply a Coercion whose free variables have the
+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 LCoercions. However,
+mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
+
+The data type is similar to Coercion.Coercion, with the following
+differences
+ * Most important, TcLetCo adds let-bindings for coercions.
+ 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
+
+ * TcAxiomInstCo takes Types, not Coecions as arguments;
+ the generality is required only in the Simplifier
+
+ * UnsafeCo aren't required
+
+ * Reprsentation invariants are weaker:
+ - we are allowed to have type synonyms in TcTyConAppCo
+ - the first arg of a TcAppCo can be a TcTyConAppCo
+ Reason: they'll get established when we desugar to Coercion
+
+\begin{code}
+data TcCoercion
+ = TcRefl TcType
+ | TcTyConAppCo TyCon [TcCoercion]
+ | TcAppCo TcCoercion TcCoercion
+ | TcForAllCo TyVar TcCoercion
+ | TcInstCo TcCoercion TcType
+ | TcCoVarCo EqVar
+ | TcAxiomInstCo CoAxiom [TcType]
+ | TcSymCo TcCoercion
+ | TcTransCo TcCoercion TcCoercion
+ | TcNthCo Int TcCoercion
+ | TcLetCo TcEvBinds TcCoercion
+ deriving (Data.Data, Data.Typeable)
+
+isEqVar :: Var -> Bool
+-- Is lifted coercion variable (only!)
+isEqVar v = case tyConAppTyCon_maybe (varType v) of
+ Just tc -> tc `hasKey` eqTyConKey
+ Nothing -> False
+
+isTcReflCo_maybe :: TcCoercion -> Maybe TcType
+isTcReflCo_maybe (TcRefl ty) = Just ty
+isTcReflCo_maybe _ = Nothing
+
+isTcReflCo :: TcCoercion -> Bool
+isTcReflCo (TcRefl {}) = True
+isTcReflCo _ = False
+
+getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
+getTcCoVar_maybe (TcCoVarCo v) = Just v
+getTcCoVar_maybe _ = Nothing
+
+mkTcReflCo :: TcType -> TcCoercion
+mkTcReflCo = TcRefl
+
+mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion
+mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]
+
+mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion
+mkTcTyConAppCo 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 -> [TcType] -> TcCoercion
+mkTcAxInstCo ax tys
+ | arity == n_tys = TcAxiomInstCo ax tys
+ | otherwise = ASSERT( arity < n_tys )
+ foldl TcAppCo (TcAxiomInstCo ax (take arity tys))
+ (map TcRefl (drop arity tys))
+ where
+ n_tys = length tys
+ arity = coAxiomArity ax
+
+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)
+mkTcAppCo co1 co2 = TcAppCo co1 co2
+
+mkTcSymCo :: TcCoercion -> TcCoercion
+mkTcSymCo co@(TcRefl {}) = co
+mkTcSymCo (TcSymCo co) = co
+mkTcSymCo co = TcSymCo co
+
+mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
+mkTcTransCo (TcRefl _) co = co
+mkTcTransCo co (TcRefl _) = co
+mkTcTransCo co1 co2 = TcTransCo co1 co2
+
+mkTcNthCo :: Int -> TcCoercion -> TcCoercion
+mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)
+mkTcNthCo n co = TcNthCo n co
+
+mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
+mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
+
+mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
+-- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
+mkTcForAllCo tv (TcRefl ty) = ASSERT( isTyVar tv ) TcRefl (mkForAllTy tv ty)
+mkTcForAllCo tv co = ASSERT( isTyVar tv ) TcForAllCo tv co
+
+mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
+mkTcForAllCos tvs (TcRefl ty) = ASSERT( all isTyVar tvs ) TcRefl (mkForAllTys tvs ty)
+mkTcForAllCos tvs co = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
+
+mkTcInstCos :: TcCoercion -> [TcType] -> TcCoercion
+mkTcInstCos (TcRefl ty) tys = TcRefl (applyTys ty tys)
+mkTcInstCos co tys = foldl TcInstCo co tys
+
+mkTcCoVarCo :: EqVar -> TcCoercion
+-- ipv :: s ~ t (the boxed equality type)
+mkTcCoVarCo ipv
+ | ty1 `eqType` ty2 = TcRefl ty1
+ | otherwise = TcCoVarCo ipv
+ where
+ (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of
+ Nothing -> pprPanic "mkCoVarLCo" (ppr ipv)
+ Just tys -> tys
+\end{code}
+
+\begin{code}
+tcCoercionKind :: TcCoercion -> Pair Type
+tcCoercionKind co = go co
+ where
+ go (TcRefl ty) = Pair ty ty
+ go (TcLetCo _ co) = go co
+ go (TcTyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map go cos)
+ go (TcAppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
+ go (TcForAllCo tv co) = mkForAllTy tv <$> go co
+ go (TcInstCo co ty) = go_inst co [ty]
+ go (TcCoVarCo cv) = eqVarKind cv
+ go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax))
+ (substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))
+ go (TcSymCo co) = swap $ go co
+ go (TcTransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
+ go (TcNthCo d co) = tyConAppArgN d <$> go co
+
+ -- c.f. Coercion.coercionKind
+ go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)
+ go_inst co tys = (`applyTys` tys) <$> go co
+
+eqVarKind :: EqVar -> Pair Type
+eqVarKind cv
+ | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
+ = ASSERT (tc `hasKey` eqTyConKey)
+ Pair ty1 ty2
+ | otherwise = panic "eqVarKind, non coercion variable"
+
+coVarsOfTcCo :: TcCoercion -> VarSet
+-- Only works on *zonked* coercions, because of TcLetCo
+coVarsOfTcCo tc_co
+ = go tc_co
+ where
+ go (TcRefl _) = emptyVarSet
+ go (TcTyConAppCo _ cos) = foldr (unionVarSet . go) emptyVarSet cos
+ go (TcAppCo co1 co2) = go co1 `unionVarSet` go co2
+ go (TcForAllCo _ co) = go co
+ go (TcInstCo co _) = go co
+ go (TcCoVarCo v) = unitVarSet v
+ go (TcAxiomInstCo {}) = emptyVarSet
+ go (TcSymCo co) = go co
+ go (TcTransCo co1 co2) = go co1 `unionVarSet` go co2
+ go (TcNthCo _ co) = go co
+ go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
+ `minusVarSet` get_bndrs bs
+ go (TcLetCo {}) = pprPanic "coVarsOfTcCo called on non-zonked TcCoercion" (ppr tc_co)
+
+ -- We expect only coercion bindings
+ go_bind :: EvBind -> VarSet
+ go_bind (EvBind _ (EvCoercion co)) = go co
+ go_bind (EvBind _ (EvId v)) = unitVarSet v
+ go_bind other = pprPanic "coVarsOfTcCo:Bind" (ppr other)
+
+ get_bndrs :: Bag EvBind -> VarSet
+ get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet
+
+liftTcCoSubstWith :: [TyVar] -> [TcCoercion] -> TcType -> TcCoercion
+-- This version can ignore capture; the free varialbes of the
+-- TcCoerion are all fresh. Result is mush simpler code
+liftTcCoSubstWith tvs cos ty
+ = ASSERT( equalLength tvs cos )
+ go ty
+ where
+ env = zipVarEnv tvs cos
+
+ go ty@(TyVarTy tv) = case lookupVarEnv env tv of
+ Just co -> co
+ Nothing -> mkTcReflCo ty
+ go (AppTy t1 t2) = mkTcAppCo (go t1) (go t2)
+ go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)
+ go (ForAllTy tv ty) = mkTcForAllCo tv (go ty)
+ go (FunTy t1 t2) = mkTcFunCo (go t1) (go t2)
+\end{code}
+
+Pretty printing
+
+\begin{code}
+instance Outputable TcCoercion where
+ ppr = pprTcCo
+
+pprTcCo, pprParendTcCo :: TcCoercion -> SDoc
+pprTcCo co = ppr_co TopPrec co
+pprParendTcCo co = ppr_co TyConPrec co
+
+ppr_co :: Prec -> TcCoercion -> SDoc
+ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)
+
+ppr_co p co@(TcTyConAppCo tc [_,_])
+ | tc `hasKey` funTyConKey = ppr_fun_co p co
+
+ppr_co p (TcTyConAppCo tc cos) = pprTcApp p ppr_co tc cos
+ppr_co p (TcLetCo bs co) = maybeParen p TopPrec $
+ sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
+ppr_co p (TcAppCo co1 co2) = maybeParen p TyConPrec $
+ pprTcCo co1 <+> ppr_co TyConPrec co2
+ppr_co p co@(TcForAllCo {}) = ppr_forall_co p co
+ppr_co p (TcInstCo co ty) = maybeParen p TyConPrec $
+ pprParendTcCo co <> ptext (sLit "@") <> pprType ty
+
+ppr_co _ (TcCoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
+ppr_co p (TcAxiomInstCo con cos) = pprTypeNameApp p ppr_type (getName con) cos
+
+ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
+ ppr_co FunPrec co1
+ <+> ptext (sLit ";")
+ <+> ppr_co FunPrec co2
+ppr_co p (TcSymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
+ppr_co p (TcNthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
+
+ppr_fun_co :: Prec -> TcCoercion -> SDoc
+ppr_fun_co p co = pprArrowChain p (split co)
+ where
+ split :: TcCoercion -> [SDoc]
+ split (TcTyConAppCo f [arg,res])
+ | f `hasKey` funTyConKey
+ = ppr_co FunPrec arg : split res
+ split co = [ppr_co TopPrec co]
+
+ppr_forall_co :: Prec -> TcCoercion -> SDoc
+ppr_forall_co p ty
+ = maybeParen p FunPrec $
+ sep [pprForAll tvs, ppr_co TopPrec rho]
+ where
+ (tvs, rho) = split1 [] ty
+ split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty
+ split1 tvs ty = (reverse tvs, ty)
+\end{code}
+
+%************************************************************************
+%* *
+ HsWrapper
+%* *
+%************************************************************************
+
+\begin{code}
+data HsWrapper
+ = WpHole -- The identity coercion
+
+ | WpCompose HsWrapper HsWrapper
+ -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
+ --
+ -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
+ -- But ([] a) `WpCompose` ([] b) = ([] b a)
+
+ | WpCast TcCoercion -- A cast: [] `cast` co
+ -- Guaranteed not the identity coercion
+
+ -- Evidence abstraction and application
+ -- (both dictionaries and coercions)
+ | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable
+ | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint
+
+ -- Kind and Type abstraction and application
+ | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var)
+ | WpTyApp KindOrType -- [] t the 't' is a type (not coercion)
+
+
+ | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings,
+ -- so that the identity coercion is always exactly WpHole
+ deriving (Data.Data, Data.Typeable)
+
+
+(<.>) :: HsWrapper -> HsWrapper -> HsWrapper
+WpHole <.> c = c
+c <.> WpHole = c
+c1 <.> c2 = c1 `WpCompose` c2
+
+mkWpTyApps :: [Type] -> HsWrapper
+mkWpTyApps tys = mk_co_app_fn WpTyApp tys
+
+mkWpEvApps :: [EvTerm] -> HsWrapper
+mkWpEvApps args = mk_co_app_fn WpEvApp args
+
+mkWpEvVarApps :: [EvVar] -> HsWrapper
+mkWpEvVarApps vs = mkWpEvApps (map EvId vs)
+
+mkWpTyLams :: [TyVar] -> HsWrapper
+mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
+
+mkWpLams :: [Var] -> HsWrapper
+mkWpLams ids = mk_co_lam_fn WpEvLam ids
+
+mkWpLet :: TcEvBinds -> HsWrapper
+-- This no-op is a quite a common case
+mkWpLet (EvBinds b) | isEmptyBag b = WpHole
+mkWpLet ev_binds = WpLet ev_binds
+
+mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
+mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
+
+mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
+-- For applications, the *first* argument must
+-- come *last* in the composition sequence
+mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
+
+idHsWrapper :: HsWrapper
+idHsWrapper = WpHole
+
+isIdHsWrapper :: HsWrapper -> Bool
+isIdHsWrapper WpHole = True
+isIdHsWrapper _ = False
+\end{code}
+
+
+%************************************************************************
+%* *
+ Evidence bindings
+%* *
+%************************************************************************
+
+\begin{code}
+data TcEvBinds
+ = TcEvBinds -- Mutable evidence bindings
+ EvBindsVar -- Mutable because they are updated "later"
+ -- when an implication constraint is solved
+
+ | EvBinds -- Immutable after zonking
+ (Bag EvBind)
+
+ deriving( Data.Typeable )
+
+data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
+ -- The Unique is only for debug printing
+
+instance Data.Data TcEvBinds where
+ -- Placeholder; we can't travers into TcEvBinds
+ toConstr _ = abstractConstr "TcEvBinds"
+ gunfold _ _ = error "gunfold"
+ dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
+
+-----------------
+newtype EvBindMap
+ = EvBindMap {
+ ev_bind_varenv :: VarEnv EvBind
+ } -- Map from evidence variables to evidence terms
+
+emptyEvBindMap :: EvBindMap
+emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
+
+extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap
+extendEvBinds bs v t
+ = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }
+
+lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
+lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
+
+evBindMapBinds :: EvBindMap -> Bag EvBind
+evBindMapBinds bs
+ = foldVarEnv consBag emptyBag (ev_bind_varenv bs)
+
+-----------------
+-- All evidence is bound by EvBinds; no side effects
+data EvBind = EvBind EvVar EvTerm
+
+data EvTerm
+ = EvId EvId -- Term-level variable-to-variable bindings
+ -- (no coercion variables! they come via EvCoercion)
+
+ | EvCoercion TcCoercion -- (Boxed) coercion bindings
+
+ | EvCast EvVar TcCoercion -- d |> co
+
+ | EvDFunApp DFunId -- Dictionary instance application
+ [Type] [EvVar]
+
+ | EvTupleSel EvId Int -- n'th component of the tuple
+
+ | EvTupleMk [EvId] -- tuple built from this stuff
+
+ | EvSuperClass DictId Int -- n'th superclass. Used for both equalities and
+ -- dictionaries, even though the former have no
+ -- selector Id. We count up from _0_
+
+ deriving( Data.Data, Data.Typeable)
+\end{code}
+
+Note [EvBinds/EvTerm]
+~~~~~~~~~~~~~~~~~~~~~
+How evidence is created and updated. Bindings for dictionaries,
+and coercions and implicit parameters are carried around in TcEvBinds
+which during constraint generation and simplification is always of the
+form (TcEvBinds ref). After constraint simplification is finished it
+will be transformed to t an (EvBinds ev_bag).
+
+Evidence for coercions *SHOULD* be filled in using the TcEvBinds
+However, all EvVars that correspond to *wanted* coercion terms in
+an EvBind must be mutable variables so that they can be readily
+inlined (by zonking) after constraint simplification is finished.
+
+Conclusion: a new wanted coercion variable should be made mutable.
+[Notice though that evidence variables that bind coercion terms
+ from super classes will be "given" and hence rigid]
+
+
+\begin{code}
+mkEvCast :: EvVar -> TcCoercion -> EvTerm
+mkEvCast ev lco
+ | isTcReflCo lco = EvId ev
+ | otherwise = EvCast ev lco
+
+emptyTcEvBinds :: TcEvBinds
+emptyTcEvBinds = EvBinds emptyBag
+
+isEmptyTcEvBinds :: TcEvBinds -> Bool
+isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
+isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
+
+
+evVarsOfTerm :: EvTerm -> [EvVar]
+evVarsOfTerm (EvId v) = [v]
+evVarsOfTerm (EvCoercion co) = varSetElems (coVarsOfTcCo co)
+evVarsOfTerm (EvDFunApp _ _ evs) = evs
+evVarsOfTerm (EvTupleSel v _) = [v]
+evVarsOfTerm (EvSuperClass v _) = [v]
+evVarsOfTerm (EvCast v co) = v : varSetElems (coVarsOfTcCo co)
+evVarsOfTerm (EvTupleMk evs) = evs
+\end{code}
+
+
+%************************************************************************
+%* *
+ Pretty printing
+%* *
+%************************************************************************
+
+\begin{code}
+instance Outputable HsWrapper where
+ ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
+
+pprHsWrapper :: SDoc -> HsWrapper -> SDoc
+-- In debug mode, print the wrapper
+-- otherwise just print what's inside
+pprHsWrapper doc wrap
+ = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
+ where
+ help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
+ -- True <=> appears in function application position
+ -- False <=> appears as body of let or lambda
+ help it WpHole = it
+ help it (WpCompose f1 f2) = help (help it f2) f1
+ help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
+ <+> pprParendTcCo co)]
+ help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
+ help it (WpTyApp ty) = no_parens $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
+ help it (WpEvLam id) = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
+ help it (WpTyLam tv) = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
+ help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
+
+ pp_bndr v = pprBndr LambdaBind v <> dot
+
+ add_parens, no_parens :: SDoc -> Bool -> SDoc
+ add_parens d True = parens d
+ add_parens d False = d
+ no_parens d _ = d
+
+instance Outputable TcEvBinds where
+ ppr (TcEvBinds v) = ppr v
+ ppr (EvBinds bs) = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
+
+instance Outputable EvBindsVar where
+ ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
+
+instance Outputable EvBind where
+ ppr (EvBind v e) = sep [ ppr v, nest 2 $ equals <+> ppr e ]
+ -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
+
+instance Outputable EvTerm where
+ ppr (EvId v) = ppr v
+ ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
+ ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co
+ ppr (EvTupleSel v n) = ptext (sLit "tupsel") <> parens (ppr (v,n))
+ ppr (EvTupleMk vs) = ptext (sLit "tupmk") <+> ppr vs
+ ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
+ ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
+\end{code}
+
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index 52177567e3..340b33c749 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -46,7 +46,7 @@ import Name import TyCon import Type import Kind( splitKiTyVars ) -import Coercion +import TcEvidence import Var import VarSet import VarEnv @@ -680,7 +680,7 @@ tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty -- Step 7: make a cast for the scrutinee, in the case that it's from a type family ; let scrut_co | Just co_con <- tyConFamilyCoercion_maybe tycon - = WpCast (mkAxInstCo co_con scrut_inst_tys) + = WpCast (mkTcAxInstCo co_con scrut_inst_tys) | otherwise = idHsWrapper -- Phew! @@ -922,7 +922,7 @@ tcTupArgs args tys ---------------- unifyOpFunTysWrap :: LHsExpr Name -> Arity -> TcRhoType - -> TcM (LCoercion, [TcSigmaType], TcRhoType) + -> TcM (TcCoercion, [TcSigmaType], TcRhoType) -- A wrapper for matchExpectedFunTys unifyOpFunTysWrap op arity ty = matchExpectedFunTys herald arity ty where @@ -1149,18 +1149,18 @@ tcTagToEnum loc fun_name arg res_ty doc3 = ptext (sLit "No family instance for this type") get_rep_ty :: TcType -> TyCon -> [TcType] - -> TcM (LCoercion, TyCon, [TcType]) + -> TcM (TcCoercion, TyCon, [TcType]) -- Converts a family type (eg F [a]) to its rep type (eg FList a) -- and returns a coercion between the two get_rep_ty ty tc tc_args | not (isFamilyTyCon tc) - = return (mkReflCo ty, tc, tc_args) + = return (mkTcReflCo ty, tc, tc_args) | otherwise = do { mb_fam <- tcLookupFamInst tc tc_args ; case mb_fam of Nothing -> failWithTc (tagToEnumError ty doc3) Just (rep_tc, rep_args) - -> return ( mkSymCo (mkAxInstCo co_tc rep_args) + -> return ( mkTcSymCo (mkTcAxInstCo co_tc rep_args) , rep_tc, rep_args ) where co_tc = expectJust "tcTagToEnum" $ diff --git a/compiler/typecheck/TcForeign.lhs b/compiler/typecheck/TcForeign.lhs index 6bc5a4fcf3..bd9f1a9b9d 100644 --- a/compiler/typecheck/TcForeign.lhs +++ b/compiler/typecheck/TcForeign.lhs @@ -30,6 +30,7 @@ import RnEnv import FamInst import FamInstEnv +import Coercion import Type import TypeRep import ForeignCall @@ -40,7 +41,6 @@ import RdrName import DataCon import TyCon import TcType -import Coercion import PrelNames import DynFlags import Outputable diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs index 72f64dddc9..c1f425b2e6 100644 --- a/compiler/typecheck/TcHsSyn.lhs +++ b/compiler/typecheck/TcHsSyn.lhs @@ -42,7 +42,7 @@ import TcRnMonad import PrelNames import TcType import TcMType -import Coercion +import TcEvidence import TysPrim import TysWiredIn import Type @@ -1081,8 +1081,8 @@ zonkVect _ (HsVectInstIn _) = panic "TcHsSyn.zonkVect: HsVectInstIn" zonkEvTerm :: ZonkEnv -> EvTerm -> TcM EvTerm zonkEvTerm env (EvId v) = ASSERT2( isId v, ppr v ) return (EvId (zonkIdOcc env v)) -zonkEvTerm env (EvCoercionBox co) = do { co' <- zonkTcLCoToLCo env co - ; return (EvCoercionBox co') } +zonkEvTerm env (EvCoercion co) = do { co' <- zonkTcLCoToLCo env co + ; return (EvCoercion co') } zonkEvTerm env (EvCast v co) = ASSERT( isId v) do { co' <- zonkTcLCoToLCo env co ; return (mkEvCast (zonkIdOcc env v) co') } @@ -1122,18 +1122,18 @@ zonkEvBind env (EvBind var term) -- same types many types. See Note [Optimized Evidence Binding Zonking] = case term of -- Fast path for reflexivity coercions: - EvCoercionBox co - | Just ty <- isReflCo_maybe co + EvCoercion co + | Just ty <- isTcReflCo_maybe co -> do { zty <- zonkTcTypeToType env ty ; let var' = setVarType var (mkEqPred (zty,zty)) - ; return (EvBind var' (EvCoercionBox (mkReflCo zty))) } + ; return (EvBind var' (EvCoercion (mkTcReflCo zty))) } -- Fast path for variable-variable bindings -- NB: could be optimized further! (e.g. SymCo cv) - | Just cv <- getCoVar_maybe co + | Just cv <- getTcCoVar_maybe co -> do { let cv' = zonkIdOcc env cv -- Just lazily look up - term' = EvCoercionBox (CoVarCo cv') + term' = EvCoercion (TcCoVarCo cv') var' = setVarType var (varType cv') ; return (EvBind var' term') } -- Ugly safe and slow path @@ -1282,7 +1282,7 @@ zonkTypeZapping tv ; return ty } -zonkTcLCoToLCo :: ZonkEnv -> LCoercion -> TcM LCoercion +zonkTcLCoToLCo :: ZonkEnv -> TcCoercion -> TcM TcCoercion -- NB: zonking often reveals that the coercion is an identity -- in which case the Refl-ness can propagate up to the top -- which in turn gives more efficient desugaring. So it's @@ -1290,22 +1290,21 @@ zonkTcLCoToLCo :: ZonkEnv -> LCoercion -> TcM LCoercion zonkTcLCoToLCo env co = go co where - go (CoVarCo cv) = return (mkEqVarLCo (zonkEvVarOcc env cv)) - go (Refl ty) = do { ty' <- zonkTcTypeToType env ty - ; return (Refl ty') } - go (TyConAppCo tc cos) = do { cos' <- mapM go cos; return (mkTyConAppCo tc cos') } - go (AxiomInstCo ax cos) = do { cos' <- mapM go cos; return (AxiomInstCo ax cos') } - go (AppCo co1 co2) = do { co1' <- go co1; co2' <- go co2 - ; return (mkAppCo co1' co2') } - go (UnsafeCo t1 t2) = do { t1' <- zonkTcTypeToType env t1 - ; t2' <- zonkTcTypeToType env t2 - ; return (mkUnsafeCo t1' t2') } - go (SymCo co) = do { co' <- go co; return (mkSymCo co') } - go (NthCo n co) = do { co' <- go co; return (mkNthCo n co') } - go (TransCo co1 co2) = do { co1' <- go co1; co2' <- go co2 - ; return (mkTransCo co1' co2') } - go (InstCo co ty) = do { co' <- go co; ty' <- zonkTcTypeToType env ty - ; return (mkInstCo co' ty') } - go (ForAllCo tv co) = ASSERT( isImmutableTyVar tv ) - do { co' <- go co; return (mkForAllCo tv co') } + go (TcLetCo bs co) = do { (env', bs') <- zonkTcEvBinds env bs + ; co' <- zonkTcLCoToLCo env' co + ; return (TcLetCo bs' co') } + go (TcCoVarCo cv) = return (mkTcCoVarCo (zonkEvVarOcc env cv)) + go (TcRefl ty) = do { ty' <- zonkTcTypeToType env ty + ; return (TcRefl ty') } + go (TcTyConAppCo tc cos) = do { cos' <- mapM go cos; return (mkTcTyConAppCo tc cos') } + go (TcAxiomInstCo ax tys) = do { tys' <- zonkTcTypeToTypes env tys; return (TcAxiomInstCo ax tys') } + go (TcAppCo co1 co2) = do { co1' <- go co1; co2' <- go co2 + ; return (mkTcAppCo co1' co2') } + go (TcSymCo co) = do { co' <- go co; return (mkTcSymCo co') } + go (TcNthCo n co) = do { co' <- go co; return (mkTcNthCo n co') } + go (TcTransCo co1 co2) = do { co1' <- go co1; co2' <- go co2 + ; return (mkTcTransCo co1' co2') } + go (TcForAllCo tv co) = ASSERT( isImmutableTyVar tv ) + do { co' <- go co; return (mkTcForAllCo tv co') } + go (TcInstCo co ty) = do { co' <- go co; ty' <- zonkTcTypeToType env ty; return (TcInstCo co' ty') } \end{code} diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index b86321e82e..33ba9cf116 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -48,6 +48,7 @@ import RnHsSyn import TcRnMonad import RnEnv ( polyKindsErr ) import TcHsSyn ( mkZonkTcTyVar ) +import TcEvidence( HsWrapper ) import TcEnv import TcMType import TcUnify diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index afcab3b022..7ec86fcc6b 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -36,7 +36,7 @@ import TcHsType import TcUnify import MkCore ( nO_METHOD_BINDING_ERROR_ID ) import Type -import Coercion hiding (substTy) +import TcEvidence import TyCon import DataCon import Class @@ -1090,16 +1090,12 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys ; mapAndUnzipM (tc_item rep_d_stuff) op_items } where loc = getSrcSpan dfun_id - - inst_tvs = fst (tcSplitForAllTys (idType dfun_id)) Just (init_inst_tys, _) = snocView inst_tys - rep_ty = pFst (coercionKind co) -- [p] + rep_ty = pFst (tcCoercionKind co) -- [p] rep_pred = mkClassPred clas (init_inst_tys ++ [rep_ty]) -- co : [p] ~ T p - co = substCoWithTys (mkInScopeSet (mkVarSet tyvars)) - inst_tvs (mkTyVarTys tyvars) $ - mkSymCo coi + co = mkTcSymCo (mkTcInstCos coi (mkTyVarTys tyvars)) ---------------- tc_item :: (TcEvBinds, EvVar) -> (Id, DefMeth) -> TcM (TcId, LHsBind TcId) @@ -1121,8 +1117,8 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys ---------------- mk_op_wrapper :: Id -> EvVar -> HsWrapper mk_op_wrapper sel_id rep_d - = WpCast (liftCoSubstWith sel_tvs (map mkReflCo init_inst_tys ++ [co]) - local_meth_ty) + = WpCast (liftTcCoSubstWith sel_tvs (map mkTcReflCo init_inst_tys ++ [co]) + local_meth_ty) <.> WpEvApp (EvId rep_d) <.> mkWpTyApps (init_inst_tys ++ [rep_ty]) where diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index db9055906b..93f499ad42 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -26,7 +26,6 @@ import Var import VarEnv ( ) -- unitVarEnv, mkInScopeSet import TcType -import HsBinds import Class import TyCon @@ -35,7 +34,7 @@ import IParam import FunDeps -import Coercion +import TcEvidence import Outputable import TcRnTypes @@ -332,10 +331,10 @@ kickOutRewritableInerts ct ; traceTcS "Kick out" (ppr ct $$ ppr wl) ; updWorkListTcS (unionWorkList wl) } -rewriteInertEqsFromInertEq :: (TcTyVar,Coercion, CtFlavor) -- A new substitution - -> TyVarEnv (Ct,Coercion) -- All inert equalities - -> TcS (TyVarEnv (Ct,Coercion)) -- The new inert equalities -rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs +rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution + -> TyVarEnv (Ct, TcCoercion) -- All inert equalities + -> TcS (TyVarEnv (Ct,TcCoercion)) -- The new inert equalities +rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs -- The goal: traverse the inert equalities and rewrite some of them, dropping some others -- back to the worklist. This is delicate, see Note [Delicate equality kick-out] = do { mieqs <- Traversable.mapM do_one ieqs @@ -362,23 +361,29 @@ rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs | otherwise -- Just keep it there = return $ Just (ct,inert_co) where + -- We have new guy co : tv ~ something + -- and old inert {wanted} cv : tv' ~ rhs[tv] + -- We want to rewrite to + -- {wanted} cv' : tv' ~ rhs[something] + -- cv = cv' ; rhs[Sym co] + -- rewrite_on_the_spot (ct,_inert_co) - = do { let rhs' = pSnd (liftedCoercionKind co) + = do { let rhs' = pSnd (tcCoercionKind co) ; delCachedEvVar ev fl ; evc <- newEqVar fl (mkTyVarTy tv) rhs' - ; let ev' = evc_the_evvar evc - ; let evco' = mkEqVarLCo ev' + ; let ev' = evc_the_evvar evc + ; let evco' = mkTcCoVarCo ev' ; fl' <- if isNewEvVar evc then do { case fl of Wanted {} - -> setEqBind ev (evco' `mkTransCo` mkSymCo co) fl + -> setEqBind ev (evco' `mkTcTransCo` mkTcSymCo co) fl Given {} - -> setEqBind ev' (mkEqVarLCo ev `mkTransCo` co) fl + -> setEqBind ev' (mkTcCoVarCo ev `mkTcTransCo` co) fl Derived {} -> return fl } else if isWanted fl then - setEqBind ev (evco' `mkTransCo` mkSymCo co) fl + setEqBind ev (evco' `mkTcTransCo` mkTcSymCo co) fl else return fl ; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' } ; return (ct',evco') } @@ -386,9 +391,9 @@ rewriteInertEqsFromInertEq (subst_tv,subst_co, subst_fl) ieqs fl = cc_flavor ct tv = cc_tyvar ct rhs = cc_rhs ct - co = liftCoSubstWith [subst_tv] [subst_co] rhs + co = liftTcCoSubstWith [subst_tv] [subst_co] rhs -kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,Coercion)), InertSet) +kick_out_rewritable :: Ct -> InertSet -> ((WorkList,TyVarEnv (Ct,TcCoercion)), InertSet) -- Returns ALL equalities, to be dealt with later kick_out_rewritable ct (IS { inert_eqs = eqmap , inert_eq_tvs = inscope @@ -617,9 +622,9 @@ solveWithIdentity d eqv wd tv xi ] ; setWantedTyBind tv xi - ; let refl_xi = mkReflCo xi + ; let refl_xi = mkTcReflCo xi - ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercionBox refl_xi) + ; let solved_fl = mkSolvedFlavor wd UnkSkol (EvCoercion refl_xi) ; (_,eqv_given) <- newGivenEqVar solved_fl (mkTyVarTy tv) xi refl_xi ; when (isWanted wd) $ do { _ <- setEqBind eqv refl_xi wd; return () } @@ -805,7 +810,7 @@ doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_i Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem) Wanted {} -> do { _ <- setEvBind (cc_id workItem) - (mkEvCast id1 (mkSymCo (mkTyConAppCo (ipTyCon nm1) [mkEqVarLCo (evc_the_evvar eqv)]))) wfl + (mkEvCast id1 (mkTcSymCo (mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo (evc_the_evvar eqv)]))) wfl ; irWorkItemConsumed "IP/IP (solved by rewriting)" } } doInteractWithInert (CFunEqCan { cc_id = eqv1, cc_flavor = fl1, cc_fun = tc1 @@ -850,10 +855,10 @@ rewriteEqLHS LeftComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) ; gw' <- case gw of Wanted {} -> setEqBind eqv2 - (mkEqVarLCo eqv1 `mkTransCo` mkSymCo (mkEqVarLCo eqv2')) gw + (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcSymCo (mkTcCoVarCo eqv2')) gw Given {} -> setEqBind eqv2' - (mkSymCo (mkEqVarLCo eqv2) `mkTransCo` mkEqVarLCo eqv1) gw + (mkTcSymCo (mkTcCoVarCo eqv2) `mkTcTransCo` mkTcCoVarCo eqv1) gw Derived {} -> return gw ; when (isNewEvVar evc) $ @@ -868,10 +873,10 @@ rewriteEqLHS RightComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) ; gw' <- case gw of Wanted {} -> setEqBind eqv2 - (mkEqVarLCo eqv1 `mkTransCo` mkEqVarLCo eqv2') gw + (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcCoVarCo eqv2') gw Given {} -> setEqBind eqv2' - (mkSymCo (mkEqVarLCo eqv1) `mkTransCo` mkEqVarLCo eqv2) gw + (mkTcSymCo (mkTcCoVarCo eqv1) `mkTcTransCo` mkTcCoVarCo eqv2) gw Derived {} -> return gw @@ -1397,11 +1402,11 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl -- RHS of a type function, so that it never -- appears in an error message -- See Note [Type synonym families] in TyCon - coe = mkAxInstCo coe_tc rep_tys + coe = mkTcAxInstCo coe_tc rep_tys ; case fl of Wanted {} -> do { evc <- newEqVar fl rhs_ty xi -- Wanted version ; let eqv' = evc_the_evvar evc - ; let coercion = coe `mkTransCo` mkEqVarLCo eqv' + ; let coercion = coe `mkTcTransCo` mkTcCoVarCo eqv' ; _ <- setEqBind eqv coercion fl ; when (isNewEvVar evc) $ (let ct = CNonCanonical { cc_id = eqv' @@ -1410,7 +1415,7 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl in updWorkListTcS (extendWorkListEq ct)) ; let _solved = workItem { cc_flavor = solved_fl } - solved_fl = mkSolvedFlavor fl UnkSkol (EvCoercionBox coercion) + solved_fl = mkSolvedFlavor fl UnkSkol (EvCoercion coercion) ; updateFlatCache eqv solved_fl tc args xi WhenSolved @@ -1421,7 +1426,7 @@ doTopReact _inerts workItem@(CFunEqCan { cc_id = eqv, cc_flavor = fl -- Cache in inerts the Solved item Given {} -> do { (fl',eqv') <- newGivenEqVar fl xi rhs_ty $ - mkSymCo (mkEqVarLCo eqv) `mkTransCo` coe + mkTcSymCo (mkTcCoVarCo eqv) `mkTcTransCo` coe ; let ct = CNonCanonical { cc_id = eqv' , cc_flavor = fl' , cc_depth = cc_depth workItem + 1} diff --git a/compiler/typecheck/TcMatches.lhs b/compiler/typecheck/TcMatches.lhs index 4aa19ae15f..d09e384834 100644 --- a/compiler/typecheck/TcMatches.lhs +++ b/compiler/typecheck/TcMatches.lhs @@ -36,7 +36,7 @@ import TysWiredIn import Id import TyCon import TysPrim -import Coercion ( isReflCo, mkSymCo ) +import TcEvidence import Outputable import Util import SrcLoc @@ -153,7 +153,7 @@ matchFunTys matchFunTys herald arity res_ty thing_inside = do { (co, pat_tys, res_ty) <- matchExpectedFunTys herald arity res_ty ; res <- thing_inside pat_tys res_ty - ; return (coToHsWrapper (mkSymCo co), res) } + ; return (coToHsWrapper (mkTcSymCo co), res) } \end{code} %************************************************************************ @@ -734,7 +734,7 @@ tcMcStmt ctxt (ParStmt bndr_stmts_s mzip_op bind_op return_op) res_ty thing_insi -- so for now we just check that it's the identity check_same actual expected = do { co <- unifyType actual expected - ; unless (isReflCo co) $ + ; unless (isTcReflCo co) $ failWithMisMatch [UnifyOrigin { uo_expected = expected , uo_actual = actual }] } diff --git a/compiler/typecheck/TcMatches.lhs-boot b/compiler/typecheck/TcMatches.lhs-boot index fccde2b548..f898f3deb7 100644 --- a/compiler/typecheck/TcMatches.lhs-boot +++ b/compiler/typecheck/TcMatches.lhs-boot @@ -7,7 +7,8 @@ -- for details module TcMatches where -import HsSyn ( GRHSs, MatchGroup, HsWrapper ) +import HsSyn ( GRHSs, MatchGroup ) +import TcEvidence( HsWrapper ) import Name ( Name ) import TcType ( TcRhoType ) import TcRnTypes( TcM, TcId ) diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index c9a67aa76d..137df8af7c 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -35,7 +35,7 @@ import TcType import TcUnify import TcHsType import TysWiredIn -import Coercion +import TcEvidence import StaticFlags import TyCon import DataCon @@ -199,7 +199,7 @@ res_ty free vars. %************************************************************************ \begin{code} -tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (LCoercion, TcId) +tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (TcCoercion, TcId) -- (coi, xp) = tcPatBndr penv x pat_ty -- Then coi : pat_ty ~ typeof(xp) -- @@ -211,11 +211,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 - ; return (mkReflCo pat_ty, bndr_id) } + ; return (mkTcReflCo pat_ty, bndr_id) } tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty = do { bndr <- mkLocalBinder bndr_name pat_ty - ; return (mkReflCo pat_ty, bndr) } + ; return (mkTcReflCo pat_ty, bndr) } ------------ newSigLetBndr :: LetBndrSpec -> Name -> TcSigInfo -> TcM TcId @@ -554,14 +554,14 @@ tc_pat penv (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut ---------------- -unifyPatType :: TcType -> TcType -> TcM LCoercion +unifyPatType :: TcType -> TcType -> TcM TcCoercion -- In patterns we want a coercion from the -- context type (expected) to the actual pattern type -- But we don't want to reverse the args to unifyType because -- that controls the actual/expected stuff in error messages unifyPatType actual_ty expected_ty = do { coi <- unifyType actual_ty expected_ty - ; return (mkSymCo coi) } + ; return (mkTcSymCo coi) } \end{code} Note [Hopping the LIE in lazy patterns] @@ -726,14 +726,14 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside } } ---------------------------- -matchExpectedPatTy :: (TcRhoType -> TcM (LCoercion, a)) +matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercion, a)) -> TcRhoType -> TcM (HsWrapper, a) -- See Note [Matching polytyped patterns] -- Returns a wrapper : pat_ty ~ inner_ty matchExpectedPatTy inner_match pat_ty | null tvs && null theta = do { (co, res) <- inner_match pat_ty - ; return (coToHsWrapper (mkSymCo co), res) } + ; return (coToHsWrapper (mkTcSymCo co), res) } -- The Sym is because the inner_match returns a coercion -- that is the other way round to matchExpectedPatTy @@ -749,7 +749,7 @@ matchExpectedPatTy inner_match pat_ty matchExpectedConTy :: TyCon -- The TyCon that this data -- constructor actually returns -> TcRhoType -- The type of the pattern - -> TcM (LCoercion, [TcSigmaType]) + -> TcM (TcCoercion, [TcSigmaType]) -- See Note [Matching constructor patterns] -- Returns a coercion : T ty1 ... tyn ~ pat_ty -- This is the same way round as matchExpectedListTy etc @@ -764,10 +764,10 @@ matchExpectedConTy data_tc pat_ty ; co1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty -- co1 : T (ty1,ty2) ~ pat_ty - ; let co2 = mkAxInstCo co_tc tys + ; let co2 = mkTcAxInstCo co_tc tys -- co2 : T (ty1,ty2) ~ T7 ty1 ty2 - ; return (mkSymCo co2 `mkTransCo` co1, tys) } + ; return (mkTcSymCo co2 `mkTcTransCo` co1, tys) } | otherwise = matchExpectedTyConApp data_tc pat_ty diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs index fbdfa1b628..4879974387 100644 --- a/compiler/typecheck/TcRnDriver.lhs +++ b/compiler/typecheck/TcRnDriver.lhs @@ -39,7 +39,8 @@ import RdrName import TcHsSyn import TcExpr import TcRnMonad -import Coercion +import TcEvidence +import Coercion( pprCoAxiom ) import FamInst import InstEnv import FamInstEnv diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs index c0a8817e31..381d5355d1 100644 --- a/compiler/typecheck/TcRnMonad.lhs +++ b/compiler/typecheck/TcRnMonad.lhs @@ -15,8 +15,8 @@ module TcRnMonad( import TcRnTypes -- Re-export all import IOEnv -- Re-export all +import TcEvidence -import Coercion import HsSyn hiding (LIE) import HscTypes import Module @@ -382,11 +382,6 @@ newSysLocalIds fs tys = do { us <- newUniqueSupply ; return (zipWith (mkSysLocal fs) (uniqsFromSupply us) tys) } -newCoVar :: TcType -> TcType -> TcRnIf gbl lcl EvVar -newCoVar ty1 ty2 - = do { uniq <- newUnique - ; return (mkLocalId (mkInternalName uniq (mkVarOccFS (fsLit "co")) noSrcSpan) (mkCoercionType ty1 ty2)) } - newName :: OccName -> TcM Name newName occ = do { uniq <- newUnique diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 2b53e174d0..ab26fa1e09 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -88,6 +88,7 @@ module TcRnTypes( import HsSyn import HscTypes +import TcEvidence( EvBind, EvBindsVar, EvTerm ) import Type import Class ( Class ) import TyCon ( TyCon ) @@ -1348,6 +1349,9 @@ data SkolemInfo | BracketSkol -- Template Haskell bracket + | UnifyForAllSkol -- We are unifying two for-all types + TcType + | UnkSkol -- Unhelpful info (until I improve it) instance Outputable SkolemInfo where @@ -1376,6 +1380,7 @@ pprSkolInfo (PatSkol dc mc) = sep [ ptext (sLit "a pattern with constructor") pprSkolInfo (InferSkol ids) = sep [ ptext (sLit "the inferred type of") , vcat [ ppr name <+> dcolon <+> ppr ty | (name,ty) <- ids ]] +pprSkolInfo (UnifyForAllSkol ty) = ptext (sLit "the type") <+> ppr ty -- UnkSkol -- For type variables the others are dealt with by pprSkolTvBinding. diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 2503197dae..4cdc28bfc5 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -1,5 +1,5 @@ \begin{code} -{-# OPTIONS -Wwarn -fno-warn-tabs #-} +{-# OPTIONS -fno-warn-tabs #-} -- The above warning supression flag is a temporary kludge. -- While working on this module you are encouraged to remove it and -- detab the module (please do the detabbing in a separate patch). See @@ -110,7 +110,7 @@ import TcType import DynFlags import Type -import Coercion +import TcEvidence import Class import TyCon import TypeRep @@ -123,11 +123,8 @@ import Bag import MonadUtils import VarSet --- import Pair ( pSnd ) import FastString import Util - -import HsBinds -- for TcEvBinds stuff import Id import TcRnTypes @@ -230,7 +227,7 @@ extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } extendWorkListCt :: Ct -> WorkList -> WorkList -- Agnostic extendWorkListCt ct wl - | isLCoVar (cc_id ct) = extendWorkListEq ct wl + | isEqVar (cc_id ct) = extendWorkListEq ct wl | otherwise = extendWorkListNonEq ct wl appendWorkListCt :: [Ct] -> WorkList -> WorkList @@ -256,8 +253,8 @@ workListFromNonEq ct = extendWorkListNonEq ct emptyWorkList workListFromCt :: Ct -> WorkList -- Agnostic -workListFromCt ct | isLCoVar (cc_id ct) = workListFromEq ct - | otherwise = workListFromNonEq ct +workListFromCt ct | isEqVar (cc_id ct) = workListFromEq ct + | otherwise = workListFromNonEq ct selectWorkItem :: WorkList -> (Maybe Ct, WorkList) @@ -394,7 +391,7 @@ partitionCCanMap pred cmap new_acc_cts = acc_cts `andCts` cts_out (cts_out, cts_keep) = partitionBag pred this_cts -partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,Coercion) -> ([Ct], TyVarEnv (Ct,Coercion)) +partitionEqMap :: (Ct -> Bool) -> TyVarEnv (Ct,TcCoercion) -> ([Ct], TyVarEnv (Ct,TcCoercion)) partitionEqMap pred isubst = let eqs_out = foldVarEnv extend_if_pred [] isubst eqs_in = filterVarEnv_Directly (\_ (ct,_) -> not (pred ct)) isubst @@ -413,7 +410,7 @@ extractUnsolvedCMap cmap = -- See Note [InertSet invariants] data InertSet - = IS { inert_eqs :: TyVarEnv (Ct,Coercion) + = IS { inert_eqs :: TyVarEnv (Ct,TcCoercion) -- Must all be CTyEqCans! If an entry exists of the form: -- a |-> ct,co -- Then ct = CTyEqCan { cc_tyvar = a, cc_rhs = xi } @@ -740,7 +737,7 @@ data EvVarCache = EvVarCache { evc_cache :: TypeMap (EvVar,CtFlavor) -- Map from PredTys to Evidence variables -- used to avoid creating new goals - , evc_flat_cache :: TypeMap (Coercion,(Xi,CtFlavor,FlatEqOrigin)) + , evc_flat_cache :: TypeMap (TcCoercion,(Xi,CtFlavor,FlatEqOrigin)) -- Map from family-free heads (F xi) to family-free types. -- Useful during flattening to share flatten skolem generation -- The boolean flag: @@ -1037,7 +1034,7 @@ getTcSEvVarCacheMap = do { cache_var <- getTcSEvVarCache ; the_cache <- wrapTcS $ TcM.readTcRef cache_var ; return (evc_cache the_cache) } -getTcSEvVarFlatCache :: TcS (TypeMap (Coercion,(Type,CtFlavor,FlatEqOrigin))) +getTcSEvVarFlatCache :: TcS (TypeMap (TcCoercion,(Type,CtFlavor,FlatEqOrigin))) getTcSEvVarFlatCache = do { cache_var <- getTcSEvVarCache ; the_cache <- wrapTcS $ TcM.readTcRef cache_var ; return (evc_flat_cache the_cache) } @@ -1064,8 +1061,8 @@ getTcEvBindsMap ; wrapTcS $ TcM.readTcRef ev_ref } -setEqBind :: EqVar -> LCoercion -> CtFlavor -> TcS CtFlavor -setEqBind eqv co fl = setEvBind eqv (EvCoercionBox co) fl +setEqBind :: EqVar -> TcCoercion -> CtFlavor -> TcS CtFlavor +setEqBind eqv co fl = setEvBind eqv (EvCoercion co) fl setWantedTyBind :: TcTyVar -> TcType -> TcS () -- Add a type binding @@ -1091,7 +1088,7 @@ setEvBind ev t fl #ifdef DEBUG ; binds <- getTcEvBindsMap - ; let cycle = any (reaches binds) (evterm_evs t) + ; let cycle = any (reaches binds) (evVarsOfTerm t) ; when cycle (fail_if_co_loop binds) #endif ; return $ @@ -1105,7 +1102,7 @@ setEvBind ev t fl where fail_if_co_loop binds = pprTrace "setEvBind" (vcat [ text "Cycle in evidence binds, evvar =" <+> ppr ev , ppr (evBindMapBinds binds) ]) $ - when (isLCoVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) + when (isEqVar ev) (pprPanic "setEvBind" (text "BUG: Coercion loop!")) reaches :: EvBindMap -> Var -> Bool -- Does this evvar reach ev? @@ -1113,16 +1110,8 @@ setEvBind ev t fl where go ev0 | ev0 == ev = True | Just (EvBind _ evtrm) <- lookupEvBind ebm ev0 - = any go (evterm_evs evtrm) + = any go (evVarsOfTerm evtrm) | otherwise = False - - evterm_evs (EvId v) = [v] - evterm_evs (EvCoercionBox lco) = varSetElems $ coVarsOfCo lco - evterm_evs (EvDFunApp _ _ evs) = evs - evterm_evs (EvTupleSel v _) = [v] - evterm_evs (EvSuperClass v _) = [v] - evterm_evs (EvCast v co) = v : varSetElems (coVarsOfCo co) - evterm_evs (EvTupleMk evs) = evs #endif \end{code} @@ -1357,7 +1346,8 @@ newEvVar fl pty -- but they don't come with guarantees -- that they can be solved and we don't -- quantify over them. - -> do { traceTcS "newEvVar" $ text "already cached, doing nothing" + -> do { traceTcS "newEvVar: already cached, doing nothing" + (ppr (evc_cache ecache)) ; return (EvVarCreated False cached_evvar) } _ -- Not cached or cached with worse flavor -> do { new <- force_new_ev_var eref ecache fl pty @@ -1425,21 +1415,21 @@ updateFlatCache ev fl fn xis rhs_ty feq_origin new_flat_cache = alterTM fun_ty x_flat_cache flat_cache new_evc = ecache { evc_flat_cache = new_flat_cache } ; wrapTcS $ TcM.writeTcRef eref new_evc } - where x_flat_cache _ = Just (mkEqVarLCo ev,(rhs_ty,fl,feq_origin)) + where x_flat_cache _ = Just (mkTcCoVarCo ev,(rhs_ty,fl,feq_origin)) fun_ty = mkTyConApp fn xis -pprEvVarCache :: TypeMap (Coercion,a) -> SDoc +pprEvVarCache :: TypeMap (TcCoercion,a) -> SDoc pprEvVarCache tm = ppr (foldTM mk_pair tm []) - where mk_pair (co,_) cos = (co, liftedCoercionKind co) : cos + where mk_pair (co,_) cos = (co, tcCoercionKind co) : cos -newGivenEqVar :: CtFlavor -> TcType -> TcType -> Coercion -> TcS (CtFlavor,EvVar) +newGivenEqVar :: CtFlavor -> TcType -> TcType -> TcCoercion -> TcS (CtFlavor,EvVar) -- Pre: fl is Given newGivenEqVar fl ty1 ty2 co = do { ecv <- newEqVar fl ty1 ty2 ; let v = evc_the_evvar ecv -- Will be a new EvVar by post of newEvVar - ; fl' <- setEvBind v (EvCoercionBox co) fl + ; fl' <- setEvBind v (EvCoercion co) fl ; return (fl',v) } newEqVar :: CtFlavor -> TcType -> TcType -> TcS EvVarCreated @@ -1500,47 +1490,47 @@ matchFam tycon args = wrapTcS $ tcLookupFamInst tycon args -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ \begin{code} -getInertEqs :: TcS (TyVarEnv (Ct,Coercion), InScopeSet) +getInertEqs :: TcS (TyVarEnv (Ct,TcCoercion), InScopeSet) getInertEqs = do { inert <- getTcSInerts ; return (inert_eqs inert, inert_eq_tvs inert) } -getCtCoercion :: Ct -> Coercion +getCtCoercion :: Ct -> TcCoercion -- Precondition: A CTyEqCan. getCtCoercion ct - | Just (GivenSolved (Just (EvCoercionBox co))) <- maybe_given + | Just (GivenSolved (Just (EvCoercion co))) <- maybe_given = co | otherwise - = mkEqVarLCo (setVarType (cc_id ct) (ctPred ct)) + = mkTcCoVarCo (setVarType (cc_id ct) (ctPred ct)) -- NB: The variable could be rewritten by a spontaneously - -- solved, so it is not safe to simply do a mkEqVarLCo (cc_id ct) + -- solved, so it is not safe to simply do a mkTcCoVarCo (cc_id ct) -- Instead we use the most accurate type, given by ctPred c where maybe_given = isGiven_maybe (cc_flavor ct) -- See Note [LiftInertEqs] -liftInertEqsTy :: (TyVarEnv (Ct,Coercion),InScopeSet) +liftInertEqsTy :: (TyVarEnv (Ct, TcCoercion),InScopeSet) -> CtFlavor - -> PredType -> Coercion + -> PredType -> TcCoercion liftInertEqsTy (subst,inscope) fl pty = ty_cts_subst subst inscope fl pty -ty_cts_subst :: TyVarEnv (Ct,Coercion) - -> InScopeSet -> CtFlavor -> Type -> Coercion +ty_cts_subst :: TyVarEnv (Ct, TcCoercion) + -> InScopeSet -> CtFlavor -> Type -> TcCoercion ty_cts_subst subst inscope fl ty = go ty where go ty = go' ty - go' (TyVarTy tv) = tyvar_cts_subst tv `orElse` Refl (TyVarTy tv) - go' (AppTy ty1 ty2) = mkAppCo (go ty1) (go ty2) - go' (TyConApp tc tys) = mkTyConAppCo tc (map go tys) + go' (TyVarTy tv) = tyvar_cts_subst tv `orElse` mkTcReflCo (TyVarTy tv) + go' (AppTy ty1 ty2) = mkTcAppCo (go ty1) (go ty2) + go' (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys) - go' (ForAllTy v ty) = mkForAllCo v' $! co + go' (ForAllTy v ty) = mkTcForAllCo v' $! co where (subst',inscope',v') = upd_tyvar_bndr subst inscope v co = ty_cts_subst subst' inscope' fl ty - go' (FunTy ty1 ty2) = mkFunCo (go ty1) (go ty2) + go' (FunTy ty1 ty2) = mkTcFunCo (go ty1) (go ty2) tyvar_cts_subst tv @@ -1556,7 +1546,7 @@ ty_cts_subst subst inscope fl ty -- But we do not want to monadically create a new EvVar. So, we -- create an 'unused_ct' but we cache reflexivity as the -- associated coercion. - | otherwise = extendVarEnv subst v (unused_ct, Refl (TyVarTy new_v)) + | otherwise = extendVarEnv subst v (unused_ct, mkTcReflCo (TyVarTy new_v)) no_change = new_v == v new_v = uniqAway inscope v diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 07875b1f49..a36be651b4 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -14,7 +14,6 @@ module TcSimplify( #include "HsVersions.h" -import HsSyn import TcRnMonad import TcErrors import TcMType @@ -26,7 +25,7 @@ import Unify ( niFixTvSubst, niSubstTvSet ) import Var import VarSet import VarEnv -import Coercion +import TcEvidence import TypeRep import Name import NameEnv ( emptyNameEnv ) @@ -1046,7 +1045,7 @@ solveCTyFunEqs cts ; return (niFixTvSubst ni_subst, unsolved_can_cts) } where solve_one (cv,tv,ty) = do { setWantedTyBind tv ty - ; _ <- setEqBind cv (mkReflCo ty) $ + ; _ <- setEqBind cv (mkTcReflCo ty) $ (Wanted $ panic "Met an already solved function equality!") ; return () -- Don't care about flavors etc this is -- the last thing happening diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs index 54bc0cd6e2..7c37fc0ab7 100644 --- a/compiler/typecheck/TcSplice.lhs +++ b/compiler/typecheck/TcSplice.lhs @@ -55,6 +55,7 @@ import Class import Inst import TyCon import DataCon +import TcEvidence( TcEvBinds(..) ) import Id import IdInfo import DsMeta diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index 018655b04d..d4d2642315 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -26,7 +26,7 @@ module TcType ( -------------------------------- -- Types TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, - TcCoercion, TcTyVar, TcTyVarSet, TcKind, TcCoVar, + TcTyVar, TcTyVarSet, TcKind, TcCoVar, -------------------------------- -- MetaDetails @@ -166,8 +166,8 @@ import Class import Var import ForeignCall import VarSet -import Type import Coercion +import Type import TyCon -- others: @@ -232,8 +232,6 @@ type TcType = Type -- A TcType can have mutable type variables -- a cannot occur inside a MutTyVar in T; that is, -- T is "flattened" before quantifying over a -type TcCoercion = Coercion -- A TcCoercion can contain TcTypes. - -- These types do not have boxy type variables in them type TcPredType = PredType type TcThetaType = ThetaType @@ -445,6 +443,8 @@ pprUserTypeCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type de %* * %************************************************************************ +Tidying is here becuase it has a special case for FlatSkol + \begin{code} -- | This tidies up a type for printing in an error message, or in -- an interface file. @@ -550,7 +550,6 @@ tidyKind = tidyType %************************************************************************ \begin{code} - tidyCo :: TidyEnv -> Coercion -> Coercion tidyCo env@(_, subst) co = go co @@ -575,7 +574,6 @@ tidyCo env@(_, subst) co tidyCos :: TidyEnv -> [Coercion] -> [Coercion] tidyCos env = map (tidyCo env) - \end{code} %************************************************************************ diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index ca34ff7164..23de50af56 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -49,7 +49,7 @@ import TcIface import TcRnMonad import TcType import Type -import Coercion +import TcEvidence import Name ( isSystemName ) import Inst import Kind @@ -119,7 +119,7 @@ expected type, becuase it expects that to have been done already matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] -> Arity -> TcRhoType - -> TcM (LCoercion, [TcSigmaType], TcRhoType) + -> TcM (TcCoercion, [TcSigmaType], TcRhoType) -- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r) -- then co : ty ~ (t1 -> ... -> tn -> ty_r) @@ -138,7 +138,7 @@ matchExpectedFunTys herald arity orig_ty -- then co : ty ~ t1 -> .. -> tn -> ty_r go n_req ty - | n_req == 0 = return (mkReflCo ty, [], ty) + | n_req == 0 = return (mkTcReflCo ty, [], ty) go n_req ty | Just ty' <- tcView ty = go n_req ty' @@ -146,7 +146,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 (mkFunCo (mkReflCo arg_ty) co, arg_ty:tys, ty_r) } + ; return (mkTcFunCo (mkTcReflCo arg_ty) co, arg_ty:tys, ty_r) } go _ (TyConApp tc _) -- A common case | not (isSynFamilyTyCon tc) @@ -189,14 +189,14 @@ matchExpectedFunTys herald arity orig_ty \begin{code} ---------------------- -matchExpectedListTy :: TcRhoType -> TcM (LCoercion, TcRhoType) +matchExpectedListTy :: TcRhoType -> TcM (TcCoercion, TcRhoType) -- Special case for lists matchExpectedListTy exp_ty = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty ; return (co, elt_ty) } ---------------------- -matchExpectedPArrTy :: TcRhoType -> TcM (LCoercion, TcRhoType) +matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercion, TcRhoType) -- Special case for parrs matchExpectedPArrTy exp_ty = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty @@ -205,7 +205,7 @@ matchExpectedPArrTy exp_ty ---------------------- matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> * -> TcRhoType -- orig_ty - -> TcM (LCoercion, -- T k1 k2 k3 a b c ~ orig_ty + -> TcM (TcCoercion, -- T k1 k2 k3 a b c ~ orig_ty [TcSigmaType]) -- Element types, k1 k2 k3 a b c -- It's used for wired-in tycons, so we call checkWiredInTyCon @@ -216,7 +216,7 @@ matchExpectedTyConApp tc orig_ty = do { checkWiredInTyCon tc ; go (tyConArity tc) orig_ty [] } where - go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (LCoercion, [TcSigmaType]) + go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (TcCoercion, [TcSigmaType]) -- If go n ty tys = (co, [t1..tn] ++ tys) -- then co : T t1..tn ~ ty @@ -233,12 +233,12 @@ matchExpectedTyConApp tc orig_ty go n_req ty@(TyConApp tycon args) tys | tc == tycon = ASSERT( n_req == length args) -- ty::* - return (mkReflCo ty, args ++ tys) + return (mkTcReflCo ty, args ++ tys) go n_req (AppTy fun arg) tys | n_req > 0 = do { (co, args) <- go (n_req - 1) fun (arg : tys) - ; return (mkAppCo co (mkReflCo arg), args) } + ; return (mkTcAppCo co (mkTcReflCo arg), args) } go n_req ty tys = defer n_req ty tys @@ -255,7 +255,7 @@ matchExpectedTyConApp tc orig_ty ---------------------- matchExpectedAppTy :: TcRhoType -- orig_ty - -> TcM (LCoercion, -- m a ~ orig_ty + -> TcM (TcCoercion, -- 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 *. @@ -267,7 +267,7 @@ matchExpectedAppTy orig_ty | Just ty' <- tcView ty = go ty' | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty - = return (mkReflCo orig_ty, (fun_ty, arg_ty)) + = return (mkTcReflCo orig_ty, (fun_ty, arg_ty)) go (TyVarTy tv) | ASSERT( isTcTyVar tv) isMetaTyVar tv @@ -469,18 +469,18 @@ The exported functions are all defined as versions of some non-exported generic functions. \begin{code} -unifyType :: TcTauType -> TcTauType -> TcM LCoercion +unifyType :: TcTauType -> TcTauType -> TcM TcCoercion -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 unifyType ty1 ty2 = uType [] ty1 ty2 --------------- -unifyPred :: PredType -> PredType -> TcM LCoercion +unifyPred :: PredType -> PredType -> TcM TcCoercion -- Actual and expected types unifyPred = unifyType --------------- -unifyTheta :: TcThetaType -> TcThetaType -> TcM [LCoercion] +unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercion] -- Actual and expected types unifyTheta theta1 theta2 = do { checkTc (equalLength theta1 theta2) @@ -531,7 +531,7 @@ uType, uType_np, uType_defer :: [EqOrigin] -> TcType -- ty1 is the *actual* type -> TcType -- ty2 is the *expected* type - -> TcM LCoercion + -> TcM TcCoercion -------------- -- It is always safe to defer unification to the main constraint solver @@ -551,7 +551,7 @@ uType_defer (item : origin) ty1 ty2 ; traceTc "utype_defer" (vcat [ppr eqv, ppr ty1, ppr ty2, ppr origin, doc]) } - ; return (mkEqVarLCo eqv) } + ; return (mkTcCoVarCo eqv) } uType_defer [] _ _ = panic "uType_defer" @@ -567,7 +567,7 @@ uType_np origin orig_ty1 orig_ty2 [ sep [ ppr orig_ty1, text "~", ppr orig_ty2] , ppr origin] ; co <- go orig_ty1 orig_ty2 - ; if isReflCo co + ; if isTcReflCo co then traceTc "u_tys yields no coercion" empty else traceTc "u_tys yields coercion:" (ppr co) ; return co } @@ -575,7 +575,7 @@ uType_np origin orig_ty1 orig_ty2 bale_out :: [EqOrigin] -> TcM a bale_out origin = failWithMisMatch origin - go :: TcType -> TcType -> TcM LCoercion + go :: TcType -> TcType -> TcM TcCoercion -- The arguments to 'go' are always semantically identical -- to orig_ty{1,2} except for looking through type synonyms @@ -602,7 +602,7 @@ uType_np origin orig_ty1 orig_ty2 go (FunTy fun1 arg1) (FunTy fun2 arg2) = do { co_l <- uType origin fun1 fun2 ; co_r <- uType origin arg1 arg2 - ; return $ mkFunCo co_l co_r } + ; return $ mkTcFunCo co_l co_r } -- Always defer if a type synonym family (type function) -- is involved. (Data families behave rigidly.) @@ -614,20 +614,20 @@ uType_np origin orig_ty1 orig_ty2 go (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2 -- See Note [TyCon app] = do { cos <- uList origin uType tys1 tys2 - ; return $ mkTyConAppCo tc1 cos } + ; return $ mkTcTyConAppCo tc1 cos } -- See Note [Care with type applications] go (AppTy s1 t1) ty2 | Just (s2,t2) <- tcSplitAppTy_maybe ty2 = do { co_s <- uType_np origin s1 s2 -- See Note [Unifying AppTy] ; co_t <- uType origin t1 t2 - ; return $ mkAppCo co_s co_t } + ; return $ mkTcAppCo co_s co_t } go ty1 (AppTy s2 t2) | Just (s1,t1) <- tcSplitAppTy_maybe ty1 = do { co_s <- uType_np origin s1 s2 ; co_t <- uType origin t1 t2 - ; return $ mkAppCo co_s co_t } + ; return $ mkTcAppCo co_s co_t } go ty1 ty2 | tcIsForAllTy ty1 || tcIsForAllTy ty2 @@ -636,7 +636,7 @@ uType_np origin orig_ty1 orig_ty2 -- Anything else fails go _ _ = bale_out origin -unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM LCoercion +unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM TcCoercion unifySigmaTy origin ty1 ty2 = do { let (tvs1, body1) = tcSplitForAllTys ty1 (tvs2, body2) = tcSplitForAllTys ty2 @@ -647,21 +647,12 @@ unifySigmaTy origin ty1 ty2 in_scope = mkInScopeSet (mkVarSet skol_tvs) phi1 = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1 phi2 = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2 + skol_info = UnifyForAllSkol ty1 - ; ((coi, _untch), lie) <- captureConstraints $ - captureUntouchables $ - uType origin phi1 phi2 - -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a) - -- VERY UNSATISFACTORY; the constraint might be fine, but - -- we fail eagerly because we don't have any place to put - -- the bindings from an implication constraint - -- This only works because most constraints get solved on the fly - -- See Note [Avoid deferring] - ; when (any (`elemVarSet` tyVarsOfWC lie) skol_tvs) - (failWithMisMatch origin) -- ToDo: give details from bad_lie - - ; emitConstraints lie - ; return (foldr mkForAllCo coi skol_tvs) } + ; (ev_binds, co) <- checkConstraints skol_info skol_tvs [] $ + uType origin phi1 phi2 + + ; return (foldr mkTcForAllCo (TcLetCo ev_binds co) skol_tvs) } --------------- uList :: [EqOrigin] @@ -774,7 +765,7 @@ of the substitution; rather, notice that @uVar@ (defined below) nips back into @uTys@ if it turns out that the variable is already bound. \begin{code} -uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM LCoercion +uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM TcCoercion uVar origin swapped tv1 ty2 = do { traceTc "uVar" (vcat [ ppr origin , ppr swapped @@ -792,13 +783,13 @@ uUnfilledVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTyVarDetails -- Tyvar 1 -> TcTauType -- Type 2 - -> TcM LCoercion + -> TcM TcCoercion -- "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 (mkReflCo (mkTyVarTy tv1)) + = return (mkTcReflCo (mkTyVarTy tv1)) | otherwise -- Distinct type variables = do { lookup2 <- lookupTcTyVar tv2 @@ -832,7 +823,7 @@ uUnfilledVars :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTyVarDetails -- Tyvar 1 -> TcTyVar -> TcTyVarDetails -- Tyvar 2 - -> TcM LCoercion + -> TcM TcCoercion -- Invarant: The type variables are distinct, -- Neither is filled in yet @@ -1018,10 +1009,10 @@ lookupTcTyVar tyvar details = ASSERT2( isTcTyVar tyvar, ppr tyvar ) tcTyVarDetails tyvar -updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM LCoercion +updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM TcCoercion updateMeta tv1 ref1 ty2 = do { writeMetaTyVarRef tv1 ref1 ty2 - ; return (mkReflCo ty2) } + ; return (mkTcReflCo ty2) } \end{code} Note [Unifying untouchables] diff --git a/compiler/typecheck/TcUnify.lhs-boot b/compiler/typecheck/TcUnify.lhs-boot index ac4d5ddc78..f53b658f40 100644 --- a/compiler/typecheck/TcUnify.lhs-boot +++ b/compiler/typecheck/TcUnify.lhs-boot @@ -10,13 +10,13 @@ module TcUnify where import TcType ( TcTauType, TcKind, Type, Kind ) import VarEnv ( TidyEnv ) import TcRnTypes ( TcM ) -import Coercion ( LCoercion ) +import TcEvidence ( TcCoercion ) import Outputable ( SDoc ) -- This boot file exists only to tie the knot between -- TcUnify and Inst -unifyType :: TcTauType -> TcTauType -> TcM LCoercion +unifyType :: TcTauType -> TcTauType -> TcM TcCoercion unifyKindEq :: TcKind -> TcKind -> TcM () mkKindErrorCtxt :: Type -> Type -> Kind -> Kind -> TidyEnv -> TcM (TidyEnv, SDoc) \end{code} diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index 17179fd2f1..840365ef78 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -17,16 +17,15 @@ module Coercion ( -- * Main data type Coercion(..), Var, CoVar, - LCoercion, -- ** Functions over coercions coVarKind, - coercionType, coercionKind, coercionKinds, isReflCo, liftedCoercionKind, + coercionType, coercionKind, coercionKinds, isReflCo, isReflCo_maybe, mkCoercionType, -- ** Constructing coercions - mkReflCo, mkCoVarCo, mkEqVarLCo, + mkReflCo, mkCoVarCo, mkAxInstCo, mkPiCo, mkPiCos, mkSymCo, mkTransCo, mkNthCo, mkInstCo, mkAppCo, mkTyConAppCo, mkFunCo, @@ -42,7 +41,7 @@ module Coercion ( splitForAllCo_maybe, -- ** Coercion variables - mkCoVar, isCoVar, isCoVarType, isLCoVar, coVarName, setCoVarName, setCoVarUnique, + mkCoVar, isCoVar, isCoVarType, coVarName, setCoVarName, setCoVarUnique, -- ** Free variables tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, coercionSize, @@ -53,8 +52,8 @@ module Coercion ( isEmptyCvSubst, zapCvSubstEnv, getCvInScope, substCo, substCos, substCoVar, substCoVars, substCoWithTy, substCoWithTys, - cvTvSubst, tvCvSubst, zipOpenCvSubst, - substTy, extendTvSubst, + cvTvSubst, tvCvSubst, mkCvSubst, zipOpenCvSubst, + substTy, extendTvSubst, extendCvSubstAndInScope, substTyVarBndr, substCoVarBndr, -- ** Lifting @@ -67,7 +66,7 @@ module Coercion ( seqCo, -- * Pretty-printing - pprCo, pprParendCo, pprCoAxiom, + pprCo, pprParendCo, pprCoAxiom, -- * Other applyCo @@ -91,7 +90,7 @@ import BasicTypes import Outputable import Unique import Pair -import PrelNames ( funTyConKey, eqPrimTyConKey, eqTyConKey ) +import PrelNames ( funTyConKey, eqPrimTyConKey ) import Control.Applicative import Data.Traversable (traverse, sequenceA) import Control.Arrow (second) @@ -150,24 +149,6 @@ data Coercion deriving (Data.Data, Data.Typeable) \end{code} -Note [LCoercions] -~~~~~~~~~~~~~~~~~ -| LCoercions are a hack used by the typechecker. Normally, -Coercions have free variables of type (a ~# b): we call these -CoVars. However, the type checker passes around equality evidence -(boxed up) at type (a ~ b). - -An LCoercion is simply a Coercion whose free variables have the -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 LCoercions. However, -mkCoVarCo will not work! The equivalent is mkEqVarLCo. - -\begin{code} -type LCoercion = Coercion -\end{code} Note [Refl invariant] ~~~~~~~~~~~~~~~~~~~~~ @@ -314,14 +295,6 @@ setCoVarName = setVarName isCoVar :: Var -> Bool isCoVar v = isCoVarType (varType v) -isLCoVar :: Var -> Bool --- Is lifted coercion variable (only!) -isLCoVar v - | Just tc <- tyConAppTyCon_maybe (varType v) - , tc `hasKey` eqTyConKey - = True - | otherwise = False - isCoVarType :: Type -> Bool isCoVarType ty -- Tests for t1 ~# t2, the unboxed equality | Just tc <- tyConAppTyCon_maybe ty = tc `hasKey` eqPrimTyConKey @@ -399,7 +372,7 @@ pprCo co = ppr_co TopPrec co pprParendCo co = ppr_co TyConPrec co ppr_co :: Prec -> Coercion -> SDoc -ppr_co _ (Refl ty) = angles (ppr ty) +ppr_co _ (Refl ty) = angleBrackets (ppr ty) ppr_co p co@(TyConAppCo tc [_,_]) | tc `hasKey` funTyConKey = ppr_fun_co p co @@ -424,9 +397,6 @@ ppr_co p (SymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendCo c ppr_co p (NthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendCo co] -angles :: SDoc -> SDoc -angles p = char '<' <> p <> char '>' - ppr_fun_co :: Prec -> Coercion -> SDoc ppr_fun_co p co = pprArrowChain p (split co) where @@ -508,14 +478,6 @@ coVarKind cv (ty1,ty2) | otherwise = panic "coVarKind, non coercion variable" -liftedCoVarKind :: EqVar -> (Type,Type) -liftedCoVarKind cv - | Just (tc, [_kind,ty1,ty2]) <- splitTyConApp_maybe (varType cv) - = ASSERT (tc `hasKey` eqTyConKey) - (ty1,ty2) - | otherwise = panic "liftedCoVarKind, non coercion variable" - - -- | Makes a coercion type from two types: the types whose equality -- is proven by the relevant 'Coercion' mkCoercionType :: Type -> Type -> Type @@ -545,16 +507,6 @@ mkCoVarCo cv where (ty1, ty2) = ASSERT( isCoVar cv ) coVarKind cv -mkEqVarLCo :: EqVar -> LCoercion --- ipv :: s ~ t (the boxed equality type) -mkEqVarLCo ipv - | ty1 `eqType` ty2 = Refl ty1 - | otherwise = CoVarCo ipv - where - (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of - Nothing -> pprPanic "mkCoVarLCo" (ppr ipv) - Just tys -> tys - mkReflCo :: Type -> Coercion mkReflCo = Refl @@ -627,7 +579,7 @@ mkTransCo co (Refl _) = co mkTransCo co1 co2 = TransCo co1 co2 mkNthCo :: Int -> Coercion -> Coercion -mkNthCo n (Refl ty) = Refl (getNth n ty) +mkNthCo n (Refl ty) = Refl (tyConAppArgN n ty) mkNthCo n co = NthCo n co -- | Instantiates a 'Coercion' with a 'Type' argument. @@ -818,6 +770,13 @@ extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst extendTvSubst (CvSubst in_scope tenv cenv) tv ty = CvSubst in_scope (extendVarEnv tenv tv ty) cenv +extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst +-- Also extends the in-scope set +extendCvSubstAndInScope (CvSubst in_scope tenv cenv) cv co + = CvSubst (in_scope `extendInScopeSetSet` tyCoVarsOfCo co) + tenv + (extendVarEnv cenv cv co) + substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar) substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var = ASSERT( isCoVar old_var ) @@ -835,13 +794,16 @@ substCoVarBndr subst@(CvSubst in_scope tenv cenv) old_var new_var = uniqAway in_scope subst_old_var subst_old_var = mkCoVar (varName old_var) (substTy subst (varType old_var)) -- It's important to do the substitution for coercions, - -- because only they can have free type variables + -- because they can have free type variables substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar) substTyVarBndr (CvSubst in_scope tenv cenv) old_var = case Type.substTyVarBndr (TvSubst in_scope tenv) old_var of (TvSubst in_scope' tenv', new_var) -> (CvSubst in_scope' tenv' cenv, new_var) +mkCvSubst :: InScopeSet -> [(Var,Coercion)] -> CvSubst +mkCvSubst in_scope prs = CvSubst in_scope Type.emptyTvSubstEnv (mkVarEnv prs) + zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst zipOpenCvSubst vs cos | debugIsOn && (length vs /= length cos) @@ -1092,29 +1054,21 @@ coercionType co = case coercionKind co of -- -- i.e. the kind of @c@ relates @t1@ and @t2@, then @coercionKind c = Pair t1 t2@. -liftedCoercionKind :: LCoercion -> Pair Type -liftedCoercionKind = coercion_kind liftedCoVarKind - coercionKind :: Coercion -> Pair Type -coercionKind = coercion_kind coVarKind - -coercion_kind :: (CoVar -> (Type,Type)) -> Coercion -> Pair Type --- Works for Coercions and LCoercions but you have to pass in what to do --- at the (unlifted or lifted) coercion variable. -coercion_kind f co = go co +coercionKind co = go co where go (Refl ty) = Pair ty ty go (TyConAppCo tc cos) = mkTyConApp tc <$> (sequenceA $ map go cos) go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2 go (ForAllCo tv co) = mkForAllTy tv <$> go co - go (CoVarCo cv) = toPair $ f cv + go (CoVarCo cv) = toPair $ coVarKind cv go (AxiomInstCo ax cos) = let Pair tys1 tys2 = sequenceA $ map go cos in Pair (substTyWith (co_ax_tvs ax) tys1 (co_ax_lhs ax)) (substTyWith (co_ax_tvs ax) tys2 (co_ax_rhs ax)) go (UnsafeCo ty1 ty2) = Pair ty1 ty2 go (SymCo co) = swap $ go co go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2) - go (NthCo d co) = getNth d <$> go co + go (NthCo d co) = tyConAppArgN d <$> go co go (InstCo aco ty) = go_app aco [ty] go_app :: Coercion -> [Type] -> Pair Type @@ -1126,12 +1080,6 @@ coercion_kind f co = go co -- | Apply 'coercionKind' to multiple 'Coercion's coercionKinds :: [Coercion] -> Pair [Type] coercionKinds tys = sequenceA $ map coercionKind tys - -getNth :: Int -> Type -> Type --- Executing Nth -getNth n ty | Just tys <- tyConAppArgs_maybe ty - = ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n -getNth n ty = pprPanic "getNth" (ppr n <+> ppr ty) \end{code} Note [Nested InstCos] diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index 579ae754a6..ebf542ab5a 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -36,7 +36,7 @@ module Type ( mkTyConApp, mkTyConTy, tyConAppTyCon_maybe, tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs, - splitTyConApp_maybe, splitTyConApp, + splitTyConApp_maybe, splitTyConApp, tyConAppArgN, mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, mkPiKinds, mkPiType, mkPiTypes, @@ -503,6 +503,13 @@ tyConAppArgs_maybe _ = Nothing tyConAppArgs :: Type -> [Type] tyConAppArgs ty = tyConAppArgs_maybe ty `orElse` pprPanic "tyConAppArgs" (ppr ty) +tyConAppArgN :: Int -> Type -> Type +-- Executing Nth +tyConAppArgN n ty + = case tyConAppArgs_maybe ty of + Just tys -> ASSERT2( n < length tys, ppr n <+> ppr tys ) tys !! n + Nothing -> pprPanic "tyConAppArgN" (ppr n <+> ppr ty) + -- | Attempts to tease a type apart into a type constructor and the application -- of a number of arguments to that constructor. Panics if that is not possible. -- See also 'splitTyConApp_maybe' diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs index fdadf7f181..0b8a1bf2cc 100644 --- a/compiler/types/TypeRep.lhs +++ b/compiler/types/TypeRep.lhs @@ -31,7 +31,7 @@ module TypeRep ( pprEqPred, pprTheta, pprForAll, pprThetaArrowTy, pprClassPred, pprKind, pprParendKind, Prec(..), maybeParen, pprTcApp, pprTypeNameApp, - pprPrefixApp, pprArrowChain, + pprPrefixApp, pprArrowChain, ppr_type, -- Free variables tyVarsOfType, tyVarsOfTypes, |