instance (OutputableBndr id) => Outputable (HsIPBinds id) where
ppr (IPBinds bs ds) = pprDeeperList vcat (map ppr bs)
- $$ ifPprDebug (ppr ds)
+ $$ ifPprDebug (ppr ds)
instance (OutputableBndr id) => Outputable (IPBind id) where
ppr (IPBind id rhs) = pprBndr LetBind id <+> equals <+> pprExpr (unLoc rhs)
deriving( Data, Typeable)
evVarTerm :: EvVar -> EvTerm
-evVarTerm v | isCoVar v = EvCoercion (mkCoVarCoercion v)
+evVarTerm v | isCoVar v = EvCoercion (mkCoVarCo v)
| otherwise = EvId v
\end{code}
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 "|>")
- <+> pprParendType co)]
+ <+> 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]
instance Outputable EvTerm where
ppr (EvId v) = ppr v
- ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendType co
- ppr (EvCoercion co) = ppr co
+ ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendCo co
+ ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co
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}
okInstDclSig (FixSig _) = False
okInstDclSig _ = True
- sigForThisGroup :: NameSet -> LSig Name -> Bool
- sigForThisGroup ns sig
- = case sigName sig of
- Nothing -> False
- Just n -> n `elemNameSet` ns
-
sigName :: LSig name -> Maybe name
+ -- Used only in Haddock
sigName (L _ sig) = sigNameNoLoc sig
sigNameNoLoc :: Sig name -> Maybe name
+ -- Used only in Haddock
sigNameNoLoc (TypeSig n _) = Just (unLoc n)
sigNameNoLoc (SpecSig n _ _) = Just (unLoc n)
sigNameNoLoc (InlineSig n _) = Just (unLoc n)
rnBind _ trim (L loc bind@(PatBind { pat_lhs = pat
, pat_rhs = grhss
-- pat fvs were stored in bind_fvs
- -- after processing the LHS
+ -- after processing the LHS
, bind_fvs = pat_fvs }))
= setSrcSpan loc $
do { let bndrs = collectPatBinders pat
, fun_infix = is_infix
, fun_matches = matches }))
-- invariant: no free vars here when it's a FunBind
- = setSrcSpan loc $
+ = setSrcSpan loc $
do { let plain_name = unLoc name
; (matches', fvs) <- bindSigTyVarsFV (sig_fn plain_name) $
-- {-# SPECIALISE #-} pragmas can refer to imported Ids
-- so, in the top-level case (when mb_names is Nothing)
-- we use lookupOccRn. If there's both an imported and a local 'f'
- -- then the SPECIALISE pragma is ambiguous, unlike alll other signatures
+ -- then the SPECIALISE pragma is ambiguous, unlike all other signatures
renameSig mb_names sig@(SpecSig v ty inl)
= do { new_v <- case mb_names of
Just {} -> lookupSigOccRn mb_names sig v
import TcPat
import TcMType
import TcType
- import RnBinds( misplacedSigErr )
import Coercion
import TysPrim
import Id
import Outputable
import FastString
- import Data.List( partition )
import Control.Monad
#include "HsVersions.h"
tcImpPrags :: [LSig Name] -> TcM [LTcSpecPrag]
tcImpPrags prags
= do { this_mod <- getModule
- ; let is_imp prag
- = case sigName prag of
- Nothing -> False
- Just name -> not (nameIsLocalOrFrom this_mod name)
- (spec_prags, others) = partition isSpecLSig $
- filter is_imp prags
- ; mapM_ misplacedSigErr others
- -- Messy that this misplaced-sig error comes here
- -- but the others come from the renamer
- ; mapAndRecoverM (wrapLocM tcImpSpec) spec_prags }
-
- tcImpSpec :: Sig Name -> TcM TcSpecPrag
- tcImpSpec prag@(SpecSig (L _ name) _ _)
+ ; mapAndRecoverM (wrapLocM tcImpSpec)
+ [L loc (name,prag) | (L loc prag@(SpecSig (L _ name) _ _)) <- prags
+ , not (nameIsLocalOrFrom this_mod name) ] }
+
+ tcImpSpec :: (Name, Sig Name) -> TcM TcSpecPrag
+ tcImpSpec (name, prag)
= do { id <- tcLookupId name
; checkTc (isAnyInlinePragma (idInlinePragma id))
(impSpecErr name)
; tcSpec id prag }
- tcImpSpec p = pprPanic "tcImpSpec" (ppr p)
impSpecErr :: Name -> SDoc
impSpecErr name
-- where F is a type function and (F a ~ [a])
-- Then unification might succeed with a coercion. But it's much
-- much simpler to require that such signatures have identical contexts
- checkTc (all isIdentityCoI cois)
+ checkTc (all isReflCo cois)
(ptext (sLit "Mutually dependent functions have syntactically distinct contexts"))
}
\end{code}
gen_soln (DS { ds_loc = loc, ds_orig = orig, ds_tvs = tyvars
, ds_cls = clas, ds_tys = inst_tys, ds_theta = deriv_rhs })
= setSrcSpan loc $
- addErrCtxt (derivInstCtxt clas inst_tys) $
+ addErrCtxt (derivInstCtxt the_pred) $
do { -- Check for a bizarre corner case, when the derived instance decl should
-- have form instance C a b => D (T a) where ...
-- Note that 'b' isn't a parameter of T. This gives rise to all sorts
; let tv_set = mkVarSet tyvars
weird_preds = [pred | pred <- deriv_rhs
- , not (tyVarsOfPred pred `subVarSet` tv_set)]
+ , not (tyVarsOfPred pred `subVarSet` tv_set)]
; mapM_ (addErrTc . badDerivedPred) weird_preds
- ; theta <- simplifyDeriv orig tyvars deriv_rhs
+ ; theta <- simplifyDeriv orig the_pred tyvars deriv_rhs
-- checkValidInstance tyvars theta clas inst_tys
-- Not necessary; see Note [Exotic derived instance contexts]
-- in TcSimplify
-- Hence no need to call:
-- checkValidInstance tyvars theta clas inst_tys
; return (sortLe (<=) theta) } -- Canonicalise before returning the solution
+ where
+ the_pred = mkClassPred clas inst_tys
------------------------------------------------------------------
mkInstance :: OverlapFlag -> ThetaType -> DerivSpec -> Instance
where
inst_spec = mkInstance oflag theta spec
co1 = case tyConFamilyCoercion_maybe rep_tycon of
- Just co_con -> ACo (mkTyConApp co_con rep_tc_args)
+ Just co_con -> mkAxInstCo co_con rep_tc_args
Nothing -> id_co
-- Not a family => rep_tycon = main tycon
- co2 = case newTyConCo_maybe rep_tycon of
- Just co_con -> ACo (mkTyConApp co_con rep_tc_args)
- Nothing -> id_co -- The newtype is transparent; no need for a cast
- co = co1 `mkTransCoI` co2
- id_co = IdCo (mkTyConApp rep_tycon rep_tc_args)
+ co2 = mkAxInstCo (newTyConCo rep_tycon) rep_tc_args
+ co = co1 `mkTransCo` co2
+ id_co = mkReflCo (mkTyConApp rep_tycon rep_tc_args)
-- Example: newtype instance N [a] = N1 (Tree a)
-- deriving instance Eq b => Eq (N [(b,b)])
standaloneCtxt ty = hang (ptext (sLit "In the stand-alone deriving instance for"))
2 (quotes (ppr ty))
- derivInstCtxt :: Class -> [Type] -> Message
- derivInstCtxt clas inst_tys
- = ptext (sLit "When deriving the instance for") <+> parens (pprClassPred clas inst_tys)
+ derivInstCtxt :: PredType -> Message
+ derivInstCtxt pred
+ = ptext (sLit "When deriving the instance for") <+> parens (ppr pred)
badDerivedPred :: PredType -> Message
badDerivedPred pred
import TysPrim
import TysWiredIn
import Type
-import Var( TyVar )
import TypeRep
import VarSet
import State
read_nullary_cons
= case nullary_cons of
[] -> []
- [con] -> [nlHsDo DoExpr [bindLex (match_con con)] (result_expr con [])]
+ [con] -> [nlHsDo DoExpr (match_con con) (result_expr con [])]
_ -> [nlHsApp (nlHsVar choose_RDR)
(nlList (map mk_pair nullary_cons))]
-- NB For operators the parens around (:=:) are matched by the
-- enclosing "parens" call, so here we must match the naked
-- data_con_str con
- match_con con | isSym con_str = symbol_pat con_str
- | otherwise = ident_pat con_str
+ match_con con | isSym con_str = [symbol_pat con_str]
+ | otherwise = ident_h_pat con_str
where
con_str = data_con_str con
-- For nullary constructors we must match Ident s for normal constrs
prefix_parser = mk_parser prefix_prec prefix_stmts body
read_prefix_con
- | isSym con_str = [read_punc "(", bindLex (symbol_pat con_str), read_punc ")"]
- | otherwise = [bindLex (ident_pat con_str)]
+ | isSym con_str = [read_punc "(", symbol_pat con_str, read_punc ")"]
+ | otherwise = ident_h_pat con_str
read_infix_con
- | isSym con_str = [bindLex (symbol_pat con_str)]
- | otherwise = [read_punc "`", bindLex (ident_pat con_str), read_punc "`"]
+ | isSym con_str = [symbol_pat con_str]
+ | otherwise = [read_punc "`"] ++ ident_h_pat con_str ++ [read_punc "`"]
prefix_stmts -- T a b c
= read_prefix_con ++ read_args
result_expr con as = nlHsApp (nlHsVar returnM_RDR) (con_app con as) -- return (con as)
punc_pat s = nlConPat punc_RDR [nlLitPat (mkHsString s)] -- Punc 'c'
- ident_pat s = nlConPat ident_RDR [nlLitPat (mkHsString s)] -- Ident "foo"
- symbol_pat s = nlConPat symbol_RDR [nlLitPat (mkHsString s)] -- Symbol ">>"
+
+ -- For constructors and field labels ending in '#', we hackily
+ -- let the lexer generate two tokens, and look for both in sequence
+ -- Thus [Ident "I"; Symbol "#"]. See Trac #5041
+ ident_h_pat s | Just (ss, '#') <- snocView s = [ ident_pat ss, symbol_pat "#" ]
+ | otherwise = [ ident_pat s ]
+
+ ident_pat s = bindLex $ nlConPat ident_RDR [nlLitPat (mkHsString s)] -- Ident "foo" <- lexP
+ symbol_pat s = bindLex $ nlConPat symbol_RDR [nlLitPat (mkHsString s)] -- Symbol ">>" <- lexP
data_con_str con = occNameString (getOccName con)
-- or (#) = 4
-- Note the parens!
read_lbl lbl | isSym lbl_str
- = [read_punc "(",
- bindLex (symbol_pat lbl_str),
- read_punc ")"]
+ = [read_punc "(", symbol_pat lbl_str, read_punc ")"]
| otherwise
- = [bindLex (ident_pat lbl_str)]
+ = ident_h_pat lbl_str
where
lbl_str = occNameString (getOccName lbl)
\end{code}
text "for primitive type" <+> ppr ty)
| otherwise = head res
where
- res = [id | (ty',id) <- tbl, ty `tcEqType` ty']
+ res = [id | (ty',id) <- tbl, ty `eqType` ty']
-----------------------------------------------------------------------
import qualified TcMType as TcM
import qualified TcEnv as TcM
( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
+import Kind
import TcType
import DynFlags
import Bag
import MonadUtils
import VarSet
+import Pair
import FastString
import HsBinds -- for TcEvBinds stuff
import Id
import TcRnTypes
-
+ #ifdef DEBUG
+ import Control.Monad( when )
+ #endif
import Data.IORef
\end{code}
ppr (CIPCan ip fl ip_nm ty)
= ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
ppr (CTyEqCan co fl tv ty)
- = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
+ = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyVarTy tv) ty)
ppr (CFunEqCan co fl tc tys ty)
- = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
+ = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (Pair (mkTyConApp tc tys) ty)
ppr (CFrozenErr co fl)
= ppr fl <+> pprEvVarWithType co
\end{code}
\begin{code}
data SimplContext
- = SimplInfer -- Inferring type of a let-bound thing
- | SimplRuleLhs -- Inferring type of a RULE lhs
- | SimplInteractive -- Inferring type at GHCi prompt
- | SimplCheck -- Checking a type signature or RULE rhs
- deriving Eq
+ = SimplInfer SDoc -- Inferring type of a let-bound thing
+ | SimplRuleLhs RuleName -- Inferring type of a RULE lhs
+ | SimplInteractive -- Inferring type at GHCi prompt
+ | SimplCheck SDoc -- Checking a type signature or RULE rhs
instance Outputable SimplContext where
- ppr SimplInfer = ptext (sLit "SimplInfer")
- ppr SimplRuleLhs = ptext (sLit "SimplRuleLhs")
+ ppr (SimplInfer d) = ptext (sLit "SimplInfer") <+> d
+ ppr (SimplCheck d) = ptext (sLit "SimplCheck") <+> d
+ ppr (SimplRuleLhs n) = ptext (sLit "SimplRuleLhs") <+> doubleQuotes (ftext n)
ppr SimplInteractive = ptext (sLit "SimplInteractive")
- ppr SimplCheck = ptext (sLit "SimplCheck")
isInteractive :: SimplContext -> Bool
isInteractive SimplInteractive = True
-- Simplify equalities only, not dictionaries
-- This is used for the LHS of rules; ee
-- Note [Simplifying RULE lhs constraints] in TcSimplify
- simplEqsOnly SimplRuleLhs = True
- simplEqsOnly _ = False
+ simplEqsOnly (SimplRuleLhs {}) = True
+ simplEqsOnly _ = False
performDefaulting :: SimplContext -> Bool
- performDefaulting SimplInfer = False
- performDefaulting SimplRuleLhs = False
- performDefaulting SimplInteractive = True
- performDefaulting SimplCheck = True
+ performDefaulting (SimplInfer {}) = False
+ performDefaulting (SimplRuleLhs {}) = False
+ performDefaulting SimplInteractive = True
+ performDefaulting (SimplCheck {}) = True
---------------
newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a }
; mapM_ do_unification (varEnvElts ty_binds)
#ifdef DEBUG
- -- ; count <- TcM.readTcRef step_count
- -- ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
+ ; count <- TcM.readTcRef step_count
+ ; when (count > 0) $
+ TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count <+> ppr context)
#endif
-- And return
; ev_binds <- TcM.readTcRef evb_ref
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
- ctxtUnderImplic SimplRuleLhs = SimplCheck
- ctxtUnderImplic ctxt = ctxt
+ ctxtUnderImplic (SimplRuleLhs n) = SimplCheck (ptext (sLit "lhs of rule")
+ <+> doubleQuotes (ftext n))
+ ctxtUnderImplic ctxt = ctxt
tryTcS :: TcS a -> TcS a
-- Like runTcS, but from within the TcS monad
bind_lvl = TcM.topIdLvl dfun_id
pprEq :: TcType -> TcType -> SDoc
-pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
+pprEq ty1 ty2 = pprPredTy $ mkEqPred (ty1,ty2)
isTouchableMetaTyVar :: TcTyVar -> TcS Bool
isTouchableMetaTyVar tv
\begin{code}
module TcSimplify(
simplifyInfer,
- simplifyDefault, simplifyDeriv,
+ simplifyDefault, simplifyDeriv,
simplifyRule, simplifyTop, simplifyInteractive
) where
import TcSMonad
import TcInteract
import Inst
-import Unify( niFixTvSubst, niSubstTvSet )
+import Id ( evVarPred )
+import Unify ( niFixTvSubst, niSubstTvSet )
import Var
import VarSet
import VarEnv
+import Coercion
import TypeRep
import Name
-- but when there is nothing to quantify we don't wrap
-- in a degenerate implication, so we do that here instead
simplifyTop wanteds
- = simplifyCheck SimplCheck wanteds
+ = simplifyCheck (SimplCheck (ptext (sLit "top level"))) wanteds
------------------
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
-> TcM () -- Succeeds iff the constraint is soluble
simplifyDefault theta
= do { wanted <- newFlatWanteds DefaultOrigin theta
- ; _ignored_ev_binds <- simplifyCheck SimplCheck (mkFlatWC wanted)
+ ; _ignored_ev_binds <- simplifyCheck (SimplCheck (ptext (sLit "defaults")))
+ (mkFlatWC wanted)
; return () }
\end{code}
\begin{code}
simplifyDeriv :: CtOrigin
- -> [TyVar]
- -> ThetaType -- Wanted
- -> TcM ThetaType -- Needed
+ -> PredType
+ -> [TyVar]
+ -> ThetaType -- Wanted
+ -> TcM ThetaType -- Needed
-- Given instance (wanted) => C inst_ty
-- Simplify 'wanted' as much as possibles
-- Fail if not possible
- simplifyDeriv orig tvs theta
+ simplifyDeriv orig pred tvs theta
= do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize
-- The constraint solving machinery
-- expects *TcTyVars* not TyVars.
; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
+ doc = parens $ ptext (sLit "deriving") <+> parens (ppr pred)
; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
; (residual_wanted, _binds)
- <- runTcS SimplInfer NoUntouchables $
+ <- runTcS (SimplInfer doc) NoUntouchables $
solveWanteds emptyInert (mkFlatWC wanted)
; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
-- Step 2
-- Now simplify the possibly-bound constraints
; (simpl_results, tc_binds0)
- <- runTcS SimplInfer NoUntouchables $
+ <- runTcS (SimplInfer (ppr (map fst name_taus))) NoUntouchables $
simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint
-- variables; hence *no untouchables*
; (lhs_results, lhs_binds)
- <- runTcS SimplRuleLhs untch $
+ <- runTcS (SimplRuleLhs name) untch $
solveWanteds emptyInert zonked_lhs
; traceTc "simplifyRule" $
-- Hence the rather painful ad-hoc treatement here
; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
- ; rhs_binds1 <- simplifyCheck SimplCheck $
+ ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
+ ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $
WC { wc_flat = emptyBag
, wc_insol = emptyBag
, wc_impl = unitBag $
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
- solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
+ solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
+ ; setCoBind cv (mkReflCo ty) }
------------
type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
\r
import Unify ( tcMatchTy )\r
import Coercion\r
-import Type\r
+import Type hiding( substTyVarBndr, substTy, extendTvSubst )\r
import TypeRep\r
import TyCon\r
import Var\r
import StaticFlags ( opt_NoOptCoercion )\r
import Util\r
import Outputable\r
+import Unify\r
+import Pair\r
+import Maybes( allMaybes )\r
+import FastString\r
\end{code}\r
\r
%************************************************************************\r
mkCoPredTy in the ForAll case, where this note appears. \r
\r
\begin{code}\r
-optCoercion :: TvSubst -> Coercion -> NormalCo\r
+optCoercion :: CvSubst -> Coercion -> NormalCo\r
-- ^ optCoercion applies a substitution to a coercion, \r
-- *and* optimises it to reduce its size\r
optCoercion env co \r
- | opt_NoOptCoercion = substTy env co\r
+ | opt_NoOptCoercion = substCo env co\r
| otherwise = opt_co env False co\r
\r
type NormalCo = Coercion\r
\r
type NormalNonIdCo = NormalCo -- Extra invariant: not the identity\r
\r
-opt_co, opt_co' :: TvSubst\r
+opt_co, opt_co' :: CvSubst\r
-> Bool -- True <=> return (sym co)\r
-> Coercion\r
-> NormalCo \r
opt_co = opt_co'\r
-\r
-{- Debuggery \r
-opt_co env sym co \r
--- = pprTrace "opt_co {" (ppr sym <+> ppr co) $\r
--- co1 `seq` \r
--- pprTrace "opt_co done }" (ppr co1) \r
--- WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (s1,t1) \r
--- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )\r
- = WARN( not (coreEqType co1 simple_result), \r
+{-\r
+opt_co env sym co\r
+ = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $\r
+ co1 `seq`\r
+ pprTrace "opt_co done }" (ppr co1) $\r
+ (WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (Pair s1 t1)\r
+ $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )\r
+ WARN( not (coreEqCoercion co1 simple_result),\r
(text "env=" <+> ppr env) $$\r
(text "input=" <+> ppr co) $$\r
(text "simple=" <+> ppr simple_result) $$\r
(text "opt=" <+> ppr co1) )\r
- co1\r
+ co1)\r
where\r
co1 = opt_co' env sym co\r
- same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2\r
- (s,t) = coercionKind (substTy env co)\r
+ same_co_kind = s1 `eqType` s2 && t1 `eqType` t2\r
+ Pair s t = coercionKind (substCo env co)\r
(s1,t1) | sym = (t,s)\r
| otherwise = (s,t)\r
- (s2,t2) = coercionKind co1\r
+ Pair s2 t2 = coercionKind co1\r
\r
- simple_result | sym = mkSymCoercion (substTy env co)\r
- | otherwise = substTy env co\r
+ simple_result | sym = mkSymCo (substCo env co)\r
+ | otherwise = substCo env co\r
-}\r
\r
-opt_co' env sym (AppTy ty1 ty2) = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)\r
-opt_co' env sym (FunTy ty1 ty2) = FunTy (opt_co env sym ty1) (opt_co env sym ty2)\r
-opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))\r
-opt_co' env sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co env sym ty))\r
-opt_co' _ _ co@(PredTy (EqPred {})) = pprPanic "optCoercion" (ppr co)\r
-\r
-opt_co' env sym co@(TyVarTy tv)\r
- | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty\r
- | not (isCoVar tv) = co -- Identity; does not mention a CoVar\r
- | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..\r
- | not sym = co\r
- | otherwise = mkSymCoercion co\r
+opt_co' env _ (Refl ty) = Refl (substTy env ty)\r
+opt_co' env sym (SymCo co) = opt_co env (not sym) co\r
- opt_co' env sym (TyConAppCo tc cos) = TyConAppCo tc (map (opt_co env sym) cos)\r
++\r
++opt_co' env sym (TyConAppCo tc cos) = mkTyConAppCo tc (map (opt_co env sym) cos)\r
+opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)\r
+opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of\r
- (env', tv') -> ForAllCo tv' (opt_co env' sym co)\r
++ (env', tv') -> mkForAllCo tv' (opt_co env' sym co)\r
++ -- Use the "mk" functions to check for nested Refls\r
++\r
+opt_co' env sym (CoVarCo cv)\r
+ | Just co <- lookupCoVar env cv\r
+ = opt_co (zapCvSubstEnv env) sym co\r
+\r
+ | Just cv1 <- lookupInScope (getCvInScope env) cv\r
+ = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)\r
+ -- cv1 might have a substituted kind!\r
+\r
+ | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)\r
+ ASSERT( isCoVar cv )\r
+ wrapSym sym (CoVarCo cv)\r
+\r
+opt_co' env sym (AxiomInstCo con cos)\r
+ -- Do *not* push sym inside top-level axioms\r
+ -- e.g. if g is a top-level axiom\r
+ -- g a : f a ~ a\r
+ -- then (sym (g ty)) /= g (sym ty) !!\r
+ = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)\r
+ -- Note that the_co does *not* have sym pushed into it\r
+\r
+opt_co' env sym (UnsafeCo ty1 ty2)\r
+ | ty1' `eqType` ty2' = Refl ty1'\r
+ | sym = mkUnsafeCo ty2' ty1'\r
+ | otherwise = mkUnsafeCo ty1' ty2'\r
where\r
- (ty1,ty2) = coVarKind tv\r
-\r
-opt_co' env sym (ForAllTy tv cor) \r
- | isTyVar tv = case substTyVarBndr env tv of\r
- (env', tv') -> ForAllTy tv' (opt_co' env' sym cor)\r
+ ty1' = substTy env ty1\r
+ ty2' = substTy env ty2\r
\r
-opt_co' env sym co@(ForAllTy co_var cor) \r
- | isCoVar co_var \r
- = WARN( co_var `elemVarSet` tyVarsOfType cor, ppr co )\r
- ForAllTy co_var' cor'\r
+opt_co' env sym (TransCo co1 co2)\r
+ | sym = opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g\r
+ | otherwise = opt_trans opt_co1 opt_co2\r
where\r
- (co1,co2) = coVarKind co_var\r
- co1' = opt_co' env sym co1\r
- co2' = opt_co' env sym co2\r
- cor' = opt_co' env sym cor\r
- co_var' = uniqAway (getTvInScope env) (mkWildCoVar (mkCoKind co1' co2'))\r
- -- See Note [Subtle shadowing in coercions]\r
-\r
-opt_co' env sym (TyConApp tc cos)\r
- | Just (arity, desc) <- isCoercionTyCon_maybe tc\r
- = mkAppTys (opt_co_tc_app env sym tc desc (take arity cos))\r
- (map (opt_co env sym) (drop arity cos))\r
- | otherwise\r
- = TyConApp tc (map (opt_co env sym) cos)\r
-\r
---------\r
-opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo\r
--- Used for CoercionTyCons only\r
--- Arguments are *not* already simplified/substituted\r
-opt_co_tc_app env sym tc desc cos\r
- = case desc of\r
- CoAxiom {} -- Do *not* push sym inside top-level axioms\r
- -- e.g. if g is a top-level axiom\r
- -- g a : F a ~ a\r
- -- Then (sym (g ty)) /= g (sym ty) !!\r
- | sym -> mkSymCoercion the_co \r
- | otherwise -> the_co\r
- where\r
- the_co = TyConApp tc (map (opt_co env False) cos)\r
- -- Note that the_co does *not* have sym pushed into it\r
- \r
- CoTrans \r
- | sym -> opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g\r
- | otherwise -> opt_trans opt_co1 opt_co2\r
-\r
- CoUnsafe\r
- | sym -> mkUnsafeCoercion ty2' ty1'\r
- | otherwise -> mkUnsafeCoercion ty1' ty2'\r
-\r
- CoSym -> opt_co env (not sym) co1\r
- CoLeft -> opt_lr fst\r
- CoRight -> opt_lr snd\r
- CoCsel1 -> opt_csel fstOf3\r
- CoCsel2 -> opt_csel sndOf3\r
- CoCselR -> opt_csel thirdOf3\r
-\r
- CoInst -- See if the first arg is already a forall\r
- -- ...then we can just extend the current substitution\r
- | Just (tv, co1_body) <- splitForAllTy_maybe co1\r
- -> opt_co (extendTvSubst env tv ty2') sym co1_body\r
-\r
- -- See if is *now* a forall\r
- | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1\r
- -> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution\r
-\r
- | otherwise\r
- -> TyConApp tc [opt_co1, ty2']\r
+ opt_co1 = opt_co env sym co1\r
+ opt_co2 = opt_co env sym co2\r
\r
+opt_co' env sym (NthCo n co)\r
+ | TyConAppCo tc cos <- co'\r
+ , isDecomposableTyCon tc -- Not synonym families\r
+ = ASSERT( n < length cos )\r
+ cos !! n\r
+ | otherwise\r
+ = NthCo n co'\r
where\r
- (co1 : cos1) = cos\r
- (co2 : _) = cos1\r
+ co' = opt_co env sym co\r
\r
- ty1' = substTy env co1\r
- ty2' = substTy env co2\r
+opt_co' env sym (InstCo co ty)\r
+ -- See if the first arg is already a forall\r
+ -- ...then we can just extend the current substitution\r
+ | Just (tv, co_body) <- splitForAllCo_maybe co\r
+ = opt_co (extendTvSubst env tv ty') sym co_body\r
\r
- -- These opt_cos have the sym pushed into them\r
- opt_co1 = opt_co env sym co1\r
- opt_co2 = opt_co env sym co2\r
+ -- See if it is a forall after optimization\r
+ | Just (tv, co'_body) <- splitForAllCo_maybe co'\r
+ = substCoWithTy tv ty' co'_body -- An inefficient one-variable substitution\r
\r
- the_unary_opt_co = TyConApp tc [opt_co1]\r
+ | otherwise = InstCo co' ty'\r
\r
- opt_lr sel = case splitAppTy_maybe opt_co1 of\r
- Nothing -> the_unary_opt_co \r
- Just lr -> sel lr\r
- opt_csel sel = case splitCoPredTy_maybe opt_co1 of\r
- Nothing -> the_unary_opt_co \r
- Just lr -> sel lr\r
+ where\r
+ co' = opt_co env sym co\r
+ ty' = substTy env ty\r
\r
-------------\r
-opt_transL :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
-opt_transL = zipWith opt_trans\r
+opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
+opt_transList = zipWith opt_trans\r
\r
opt_trans :: NormalCo -> NormalCo -> NormalCo\r
opt_trans co1 co2\r
- | isIdNormCo co1 = co2\r
- | otherwise = opt_trans1 co1 co2\r
+ | isReflCo co1 = co2\r
+ | otherwise = opt_trans1 co1 co2\r
\r
opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo\r
-- First arg is not the identity\r
opt_trans1 co1 co2\r
- | isIdNormCo co2 = co1\r
- | otherwise = opt_trans2 co1 co2\r
+ | isReflCo co2 = co1\r
+ | otherwise = opt_trans2 co1 co2\r
\r
opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo\r
-- Neither arg is the identity\r
-opt_trans2 (TyConApp tc [co1a,co1b]) co2\r
- | tc `hasKey` transCoercionTyConKey\r
- = opt_trans1 co1a (opt_trans2 co1b co2)\r
+opt_trans2 (TransCo co1a co1b) co2\r
+ -- Don't know whether the sub-coercions are the identity\r
+ = opt_trans co1a (opt_trans co1b co2) \r
\r
opt_trans2 co1 co2 \r
| Just co <- opt_trans_rule co1 co2\r
= co\r
\r
-opt_trans2 co1 (TyConApp tc [co2a,co2b])\r
- | tc `hasKey` transCoercionTyConKey\r
- , Just co1_2a <- opt_trans_rule co1 co2a\r
- = if isIdNormCo co1_2a\r
+opt_trans2 co1 (TransCo co2a co2b)\r
+ | Just co1_2a <- opt_trans_rule co1 co2a\r
+ = if isReflCo co1_2a\r
then co2b\r
- else opt_trans2 co1_2a co2b\r
+ else opt_trans1 co1_2a co2b\r
\r
opt_trans2 co1 co2\r
- = mkTransCoercion co1 co2\r
+ = mkTransCo co1 co2\r
\r
------\r
+-- Optimize coercions with a top-level use of transitivity.\r
opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo\r
-opt_trans_rule (TyConApp tc1 args1) (TyConApp tc2 args2)\r
- | tc1 == tc2\r
- = case isCoercionTyCon_maybe tc1 of\r
- Nothing \r
- -> Just (TyConApp tc1 (opt_transL args1 args2))\r
- Just (arity, desc) \r
- | arity == length args1\r
- -> opt_trans_rule_equal_tc desc args1 args2\r
- | otherwise\r
- -> case opt_trans_rule_equal_tc desc \r
- (take arity args1) \r
- (take arity args2) of\r
- Just co -> Just $ mkAppTys co $ \r
- opt_transL (drop arity args1) (drop arity args2)\r
- Nothing -> Nothing \r
- \r
--- Push transitivity inside apply\r
-opt_trans_rule co1 co2\r
- | Just (co1a, co1b) <- splitAppTy_maybe co1\r
- , Just (co2a, co2b) <- etaApp_maybe co2\r
- = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
\r
- | Just (co2a, co2b) <- splitAppTy_maybe co2\r
- , Just (co1a, co1b) <- etaApp_maybe co1\r
- = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
+-- push transitivity down through matching top-level constructors.\r
+opt_trans_rule in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)\r
+ | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $\r
+ TyConAppCo tc1 (opt_transList cos1 cos2)\r
+\r
+-- push transitivity through matching destructors\r
+opt_trans_rule in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)\r
+ | d1 == d2\r
+ , co1 `compatible_co` co2\r
+ = fireTransRule "PushNth" in_co1 in_co2 $\r
+ mkNthCo d1 (opt_trans co1 co2)\r
\r
+-- Push transitivity inside instantiation\r
+opt_trans_rule in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)\r
+ | ty1 `eqType` ty2\r
+ , co1 `compatible_co` co2\r
+ = fireTransRule "TrPushInst" in_co1 in_co2 $\r
+ mkInstCo (opt_trans co1 co2) ty1\r
+ \r
+-- Push transitivity inside apply\r
+opt_trans_rule in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)\r
+ = fireTransRule "TrPushApp" in_co1 in_co2 $\r
+ mkAppCo (opt_trans co1a co2a) (opt_trans co1b co2b)\r
+\r
+-- Push transitivity inside PredCos\r
+opt_trans_rule in_co1@(PredCo pco1) in_co2@(PredCo pco2)\r
+ | Just pco' <- opt_trans_pred pco1 pco2\r
+ = fireTransRule "TrPushPrd" in_co1 in_co2 $\r
+ mkPredCo pco'\r
+\r
+opt_trans_rule co1@(TyConAppCo tc cos1) co2\r
+ | Just cos2 <- etaTyConAppCo_maybe tc co2\r
+ = ASSERT( length cos1 == length cos2 )\r
+ fireTransRule "EtaCompL" co1 co2 $\r
+ TyConAppCo tc (zipWith opt_trans cos1 cos2)\r
+\r
+opt_trans_rule co1 co2@(TyConAppCo tc cos2)\r
+ | Just cos1 <- etaTyConAppCo_maybe tc co1\r
+ = ASSERT( length cos1 == length cos2 )\r
+ fireTransRule "EtaCompR" co1 co2 $\r
+ TyConAppCo tc (zipWith opt_trans cos1 cos2)\r
+\r
+\r
+{- BAY: think harder about this. do we still need it?\r
-- Push transitivity inside (s~t)=>r\r
-- We re-use the CoVar rather than using mkCoPredTy\r
-- See Note [Subtle shadowing in coercions]\r
, isCoVar cv1\r
, Just (s1,t1) <- coVarKind_maybe cv1\r
, Just (s2,t2,r2) <- etaCoPred_maybe co2\r
- = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
+ = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoType (opt_trans s1 s2) (opt_trans t1 t2)))\r
(opt_trans r1 r2))\r
\r
| Just (cv2,r2) <- splitForAllTy_maybe co2\r
, isCoVar cv2\r
, Just (s2,t2) <- coVarKind_maybe cv2\r
, Just (s1,t1,r1) <- etaCoPred_maybe co1\r
- = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
+ = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoType (opt_trans s1 s2) (opt_trans t1 t2)))\r
(opt_trans r1 r2))\r
+-}\r
\r
-- Push transitivity inside forall\r
opt_trans_rule co1 co2\r
- | Just (tv1,r1) <- splitTypeForAll_maybe co1\r
- , Just (tv2,r2) <- etaForAll_maybe co2\r
- , let r2' = substTyWith [tv2] [TyVarTy tv1] r2\r
- = Just (ForAllTy tv1 (opt_trans2 r1 r2'))\r
-\r
- | Just (tv2,r2) <- splitTypeForAll_maybe co2\r
- , Just (tv1,r1) <- etaForAll_maybe co1\r
- , let r1' = substTyWith [tv1] [TyVarTy tv2] r1\r
- = Just (ForAllTy tv1 (opt_trans2 r1' r2))\r
-\r
+ | Just (tv1,r1) <- splitForAllCo_maybe co1\r
+ , Just (tv2,r2) <- etaForAllCo_maybe co2\r
+ , let r2' = substCoWithTy tv2 (mkTyVarTy tv1) r2\r
+ = fireTransRule "EtaAllL" co1 co2 $\r
+ mkForAllCo tv1 (opt_trans2 r1 r2')\r
+\r
+ | Just (tv2,r2) <- splitForAllCo_maybe co2\r
+ , Just (tv1,r1) <- etaForAllCo_maybe co1\r
+ , let r1' = substCoWithTy tv1 (mkTyVarTy tv2) r1\r
+ = fireTransRule "EtaAllR" co1 co2 $\r
+ mkForAllCo tv1 (opt_trans2 r1' r2)\r
+\r
+-- Push transitivity inside axioms\r
opt_trans_rule co1 co2\r
-{- Omitting for now, because unsound\r
- | Just (sym1, (ax_tc1, ax1_args, ax_tvs, ax_lhs, ax_rhs)) <- co1_is_axiom_maybe\r
- , Just (sym2, (ax_tc2, ax2_args, _, _, _)) <- co2_is_axiom_maybe\r
- , ax_tc1 == ax_tc2\r
- , sym1 /= sym2\r
- = Just $\r
- if sym1 \r
- then substTyWith ax_tvs (opt_transL (map mkSymCoercion ax1_args) ax2_args) ax_rhs\r
- else substTyWith ax_tvs (opt_transL ax1_args (map mkSymCoercion ax2_args)) ax_lhs\r
--}\r
\r
- | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- co1_is_axiom_maybe\r
- , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co2\r
- = Just $ \r
+ -- TrPushAxR/TrPushSymAxR\r
+ | Just (sym, con, cos1) <- co1_is_axiom_maybe\r
+ , Just cos2 <- matchAxiom sym con co2\r
+ = fireTransRule "TrPushAxR" co1 co2 $\r
if sym \r
- then mkSymCoercion $ TyConApp ax_tc (opt_transL (map mkSymCoercion cos) ax_args)\r
- else TyConApp ax_tc (opt_transL ax_args cos)\r
+ then SymCo $ AxiomInstCo con (opt_transList (map mkSymCo cos2) cos1)\r
+ else AxiomInstCo con (opt_transList cos1 cos2)\r
\r
- | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- isAxiom_maybe co2\r
- , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co1\r
- = Just $ \r
+ -- TrPushAxL/TrPushSymAxL\r
+ | Just (sym, con, cos2) <- co2_is_axiom_maybe\r
+ , Just cos1 <- matchAxiom (not sym) con co1\r
+ = fireTransRule "TrPushAxL" co1 co2 $\r
if sym \r
- then mkSymCoercion $ TyConApp ax_tc (opt_transL ax_args (map mkSymCoercion cos))\r
- else TyConApp ax_tc (opt_transL cos ax_args)\r
+ then SymCo $ AxiomInstCo con (opt_transList cos2 (map mkSymCo cos1))\r
+ else AxiomInstCo con (opt_transList cos1 cos2)\r
+\r
+ -- TrPushAxSym/TrPushSymAx\r
+ | Just (sym1, con1, cos1) <- co1_is_axiom_maybe\r
+ , Just (sym2, con2, cos2) <- co2_is_axiom_maybe\r
+ , con1 == con2\r
+ , sym1 == not sym2\r
+ , let qtvs = co_ax_tvs con1\r
+ lhs = co_ax_lhs con1 \r
+ rhs = co_ax_rhs con1 \r
+ pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)\r
+ , all (`elemVarSet` pivot_tvs) qtvs\r
+ = fireTransRule "TrPushAxSym" co1 co2 $\r
+ if sym2\r
+ then liftCoSubstWith qtvs (opt_transList cos1 (map mkSymCo cos2)) lhs -- TrPushAxSym\r
+ else liftCoSubstWith qtvs (opt_transList (map mkSymCo cos1) cos2) rhs -- TrPushSymAx\r
where\r
co1_is_axiom_maybe = isAxiom_maybe co1\r
co2_is_axiom_maybe = isAxiom_maybe co2\r
\r
opt_trans_rule co1 co2 -- Identity rule\r
- | (ty1,_) <- coercionKind co1\r
- , (_,ty2) <- coercionKind co2\r
- , ty1 `coreEqType` ty2\r
- = Just ty2\r
+ | Pair ty1 _ <- coercionKind co1\r
+ , Pair _ ty2 <- coercionKind co2\r
+ , ty1 `eqType` ty2\r
+ = fireTransRule "RedTypeDirRefl" co1 co2 $\r
+ Refl ty2\r
\r
opt_trans_rule _ _ = Nothing\r
\r
------------ \r
-isAxiom_maybe :: Coercion -> Maybe (Bool, (TyCon, [Coercion], [TyVar], Type, Type))\r
-isAxiom_maybe co\r
- | Just (tc, args) <- splitTyConApp_maybe co\r
- , Just (_, desc) <- isCoercionTyCon_maybe tc\r
- = case desc of\r
- CoAxiom { co_ax_tvs = tvs, co_ax_lhs = lhs, co_ax_rhs = rhs } \r
- -> Just (False, (tc, args, tvs, lhs, rhs))\r
- CoSym | (arg1:_) <- args \r
- -> case isAxiom_maybe arg1 of\r
- Nothing -> Nothing\r
- Just (sym, stuff) -> Just (not sym, stuff)\r
- _ -> Nothing\r
- | otherwise\r
- = Nothing\r
-\r
-matchesAxiomLhs :: [TyVar] -> Type -> Type -> Maybe [Type]\r
-matchesAxiomLhs tvs ty_tmpl ty \r
- = case tcMatchTy (mkVarSet tvs) ty_tmpl ty of\r
+opt_trans_pred :: Pred Coercion -> Pred Coercion -> Maybe (Pred Coercion)\r
+opt_trans_pred (EqPred co1a co1b) (EqPred co2a co2b)\r
+ = Just (EqPred (opt_trans co1a co2a) (opt_trans co1b co2b))\r
+opt_trans_pred (ClassP cls1 cos1) (ClassP cls2 cos2)\r
+ | cls1 == cls2\r
+ = Just (ClassP cls1 (opt_transList cos1 cos2))\r
+opt_trans_pred (IParam n1 co1) (IParam n2 co2)\r
+ | n1 == n2\r
+ = Just (IParam n1 (opt_trans co1 co2))\r
+opt_trans_pred _ _ = Nothing\r
+\r
+fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion\r
+fireTransRule rule co1 co2 res\r
+ = -- pprTrace ("Trans rule fired: " ++ rule) (vcat [ppr co1, ppr co2, ppr res]) $\r
+ Just res\r
+\r
+-----------\r
+wrapSym :: Bool -> Coercion -> Coercion\r
+wrapSym sym co | sym = SymCo co\r
+ | otherwise = co\r
+\r
+-----------\r
+isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom, [Coercion])\r
+isAxiom_maybe (SymCo co) \r
+ | Just (sym, con, cos) <- isAxiom_maybe co\r
+ = Just (not sym, con, cos)\r
+isAxiom_maybe (AxiomInstCo con cos)\r
+ = Just (False, con, cos)\r
+isAxiom_maybe _ = Nothing\r
+\r
+matchAxiom :: Bool -- True = match LHS, False = match RHS\r
+ -> CoAxiom -> Coercion -> Maybe [Coercion]\r
+-- If we succeed in matching, then *all the quantified type variables are bound*\r
+-- E.g. if tvs = [a,b], lhs/rhs = [b], we'll fail\r
+matchAxiom sym (CoAxiom { co_ax_tvs = qtvs, co_ax_lhs = lhs, co_ax_rhs = rhs }) co\r
+ = case liftCoMatch (mkVarSet qtvs) (if sym then lhs else rhs) co of\r
Nothing -> Nothing\r
- Just subst -> Just (map (substTyVar subst) tvs)\r
-\r
------------ \r
-opt_trans_rule_equal_tc :: CoTyConDesc -> [Coercion] -> [Coercion] -> Maybe Coercion\r
--- Rules for Coercion TyCons only\r
-\r
--- Push transitivity inside instantiation\r
-opt_trans_rule_equal_tc desc [co1,ty1] [co2,ty2]\r
- | CoInst <- desc\r
- , ty1 `coreEqType` ty2\r
- , co1 `compatible_co` co2\r
- = Just (mkInstCoercion (opt_trans2 co1 co2) ty1) \r
-\r
-opt_trans_rule_equal_tc desc [co1] [co2]\r
- | CoLeft <- desc, is_compat = Just (mkLeftCoercion res_co)\r
- | CoRight <- desc, is_compat = Just (mkRightCoercion res_co)\r
- | CoCsel1 <- desc, is_compat = Just (mkCsel1Coercion res_co)\r
- | CoCsel2 <- desc, is_compat = Just (mkCsel2Coercion res_co)\r
- | CoCselR <- desc, is_compat = Just (mkCselRCoercion res_co)\r
- where\r
- is_compat = co1 `compatible_co` co2\r
- res_co = opt_trans2 co1 co2\r
-\r
-opt_trans_rule_equal_tc _ _ _ = Nothing\r
+ Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)\r
\r
-------------\r
compatible_co :: Coercion -> Coercion -> Bool\r
-- Check whether (co1 . co2) will be well-kinded\r
compatible_co co1 co2\r
- = x1 `coreEqType` x2 \r
+ = x1 `eqType` x2 \r
where\r
- (_,x1) = coercionKind co1\r
- (x2,_) = coercionKind co2\r
+ Pair _ x1 = coercionKind co1\r
+ Pair x2 _ = coercionKind co2\r
\r
-------------\r
-etaForAll_maybe :: Coercion -> Maybe (TyVar, Coercion)\r
+etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)\r
-- Try to make the coercion be of form (forall tv. co)\r
-etaForAll_maybe co\r
- | Just (tv, r) <- splitForAllTy_maybe co\r
- , not (isCoVar tv) -- Check it is a *type* forall, not a (t1~t2)=>co\r
+etaForAllCo_maybe co\r
+ | Just (tv, r) <- splitForAllCo_maybe co\r
= Just (tv, r)\r
\r
- | (ty1,ty2) <- coercionKind co\r
- , Just (tv1, _) <- splitTypeForAll_maybe ty1\r
- , Just (tv2, _) <- splitTypeForAll_maybe ty2\r
+ | Pair ty1 ty2 <- coercionKind co\r
+ , Just (tv1, _) <- splitForAllTy_maybe ty1\r
+ , Just (tv2, _) <- splitForAllTy_maybe ty2\r
, tyVarKind tv1 `eqKind` tyVarKind tv2\r
- = Just (tv1, mkInstCoercion co (mkTyVarTy tv1))\r
+ = Just (tv1, mkInstCo co (mkTyVarTy tv1))\r
\r
| otherwise\r
= Nothing\r
\r
-etaCoPred_maybe :: Coercion -> Maybe (Coercion, Coercion, Coercion)\r
-etaCoPred_maybe co \r
- | Just (s,t,r) <- splitCoPredTy_maybe co\r
- = Just (s,t,r)\r
- \r
- -- co :: (s1~t1)=>r1 ~ (s2~t2)=>r2\r
- | (ty1,ty2) <- coercionKind co -- We know ty1,ty2 have same kind\r
- , Just (s1,_,_) <- splitCoPredTy_maybe ty1\r
- , Just (s2,_,_) <- splitCoPredTy_maybe ty2\r
- , typeKind s1 `eqKind` typeKind s2 -- t1,t2 have same kinds\r
- = Just (mkCsel1Coercion co, mkCsel2Coercion co, mkCselRCoercion co)\r
- \r
- | otherwise\r
- = Nothing\r
-\r
-etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)\r
--- Split a coercion g :: t1a t1b ~ t2a t2b\r
--- into (left g, right g) if possible\r
-etaApp_maybe co\r
- | Just (co1, co2) <- splitAppTy_maybe co\r
- = Just (co1, co2)\r
-\r
- | (ty1,ty2) <- coercionKind co\r
- , Just (ty1a, _) <- splitAppTy_maybe ty1\r
- , Just (ty2a, _) <- splitAppTy_maybe ty2\r
- , typeKind ty1a `eqKind` typeKind ty2a\r
- = Just (mkLeftCoercion co, mkRightCoercion co)\r
-\r
- | otherwise\r
- = Nothing\r
-\r
--------------\r
-splitTypeForAll_maybe :: Type -> Maybe (TyVar, Type)\r
--- Returns Just only for a *type* forall, not a (t1~t2)=>co\r
-splitTypeForAll_maybe ty\r
- | Just (tv, rty) <- splitForAllTy_maybe ty\r
- , not (isCoVar tv)\r
- = Just (tv, rty)\r
+etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]\r
+-- If possible, split a coercion \r
+-- g :: T s1 .. sn ~ T t1 .. tn\r
+-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] \r
+etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)\r
+ = ASSERT( tc == tc2 ) Just cos2\r
+\r
+etaTyConAppCo_maybe tc co\r
+ | isDecomposableTyCon tc\r
+ , Pair ty1 ty2 <- coercionKind co\r
+ , Just (tc1, tys1) <- splitTyConApp_maybe ty1\r
+ , Just (tc2, tys2) <- splitTyConApp_maybe ty2\r
+ , tc1 == tc2\r
+ , let n = length tys1\r
+ = ASSERT( tc == tc1 ) \r
+ ASSERT( n == length tys2 )\r
+ Just (decomposeCo n co) \r
+ -- NB: n might be <> tyConArity tc\r
+ -- e.g. data family T a :: * -> *\r
+ -- g :: T a b ~ T c d\r
\r
| otherwise\r
= Nothing\r
-\r
--------------\r
-isIdNormCo :: NormalCo -> Bool\r
--- Cheap identity test: look for coercions with no coercion variables at all\r
--- So it'll return False for (sym g `trans` g)\r
-isIdNormCo ty = go ty\r
- where\r
- go (TyVarTy tv) = not (isCoVar tv)\r
- go (AppTy t1 t2) = go t1 && go t2\r
- go (FunTy t1 t2) = go t1 && go t2\r
- go (ForAllTy tv ty) = go (tyVarKind tv) && go ty\r
- go (TyConApp tc tys) = not (isCoercionTyCon tc) && all go tys\r
- go (PredTy (IParam _ ty)) = go ty\r
- go (PredTy (ClassP _ tys)) = all go tys\r
- go (PredTy (EqPred t1 t2)) = go t1 && go t2\r
\end{code} \r
\begin{code}
-- We expose the relevant stuff from this module via the Type module
{-# OPTIONS_HADDOCK hide #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-
+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
module TypeRep (
TyThing(..),
Type(..),
- PredType(..), -- to friends
+ Pred(..), -- to friends
- Kind, ThetaType, -- Synonyms
+ Kind, SuperKind,
+ PredType, ThetaType, -- Synonyms
- funTyCon, funTyConName,
+ -- Functions over types
+ mkTyConApp, mkTyConTy, mkTyVarTy, mkTyVarTys,
+ isLiftedTypeKind, isCoercionKind,
- -- Pretty-printing
+ -- Pretty-printing
pprType, pprParendType, pprTypeApp,
pprTyThing, pprTyThingCategory,
- pprPred, pprEqPred, pprTheta, pprForAll, pprThetaArrow, pprClassPred,
-
- -- Kinds
- liftedTypeKind, unliftedTypeKind, openTypeKind,
- argTypeKind, ubxTupleKind,
- isLiftedTypeKindCon, isLiftedTypeKind,
- mkArrowKind, mkArrowKinds, isCoercionKind,
- coVarPred,
-
- -- Kind constructors...
- liftedTypeKindTyCon, openTypeKindTyCon, unliftedTypeKindTyCon,
- argTypeKindTyCon, ubxTupleKindTyCon,
-
- -- And their names
- unliftedTypeKindTyConName, openTypeKindTyConName,
- ubxTupleKindTyConName, argTypeKindTyConName,
- liftedTypeKindTyConName,
-
- -- Super Kinds
- tySuperKind, coSuperKind,
- isTySuperKind, isCoSuperKind,
- tySuperKindTyCon, coSuperKindTyCon,
-
- pprKind, pprParendKind
+ pprPredTy, pprEqPred, pprTheta, pprForAll, pprThetaArrowTy, pprClassPred,
+ pprKind, pprParendKind,
+ Prec(..), maybeParen, pprTcApp, pprTypeNameApp,
+ pprPrefixApp, pprPred, pprArrowChain, pprThetaArrow,
+
+ -- Free variables
+ tyVarsOfType, tyVarsOfTypes,
+ tyVarsOfPred, tyVarsOfTheta,
+ varsOfPred, varsOfTheta,
+ predSize,
+
+ -- Substitutions
+ TvSubst(..), TvSubstEnv
) where
#include "HsVersions.h"
-- friends:
import Var
+import VarEnv
+import VarSet
import Name
import BasicTypes
import TyCon
import PrelNames
import Outputable
import FastString
+import Pair
-- libraries
-import Data.Data hiding ( TyCon )
+import qualified Data.Data as Data hiding ( TyCon )
+import qualified Data.Foldable as Data
+import qualified Data.Traversable as Data
\end{code}
----------------------
\begin{code}
-- | The key representation of types within the compiler
data Type
- = TyVarTy TyVar -- ^ Vanilla type variable
+ = TyVarTy TyVar -- ^ Vanilla type variable (*never* a coercion variable)
| AppTy
Type
Type -- ^ Type application to something other than a 'TyCon'. Parameters:
--
- -- 1) Function: must /not/ be a 'TyConApp', must be another 'AppTy', or 'TyVarTy'
+ -- 1) Function: must /not/ be a 'TyConApp',
+ -- must be another 'AppTy', or 'TyVarTy'
--
-- 2) Argument type
[Type] -- ^ Application of a 'TyCon', including newtypes /and/ synonyms.
-- Invariant: saturated appliations of 'FunTyCon' must
-- use 'FunTy' and saturated synonyms must use their own
- -- constructors. However, /unsaturated/ 'FunTyCon's do appear as 'TyConApp's.
+ -- constructors. However, /unsaturated/ 'FunTyCon's
+ -- do appear as 'TyConApp's.
-- Parameters:
--
-- 1) Type constructor being applied to.
--
- -- 2) Type arguments. Might not have enough type arguments here to saturate the constructor.
- -- Even type synonyms are not necessarily saturated; for example unsaturated type synonyms
- -- can appear as the right hand side of a type synonym.
+ -- 2) Type arguments. Might not have enough type arguments
+ -- here to saturate the constructor.
+ -- Even type synonyms are not necessarily saturated;
+ -- for example unsaturated type synonyms
+ -- can appear as the right hand side of a type synonym.
| FunTy
- Type
+ Type
Type -- ^ Special case of 'TyConApp': @TyConApp FunTyCon [t1, t2]@
+ -- See Note [Equality-constrained types]
| ForAllTy
- TyVar
+ TyCoVar -- Type variable
Type -- ^ A polymorphic type
| PredTy
PredType -- ^ The type of evidence for a type predictate.
-- Note that a @PredTy (EqPred _ _)@ can appear only as the kind
- -- of a coercion variable; never as the argument or result
- -- of a 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
+ -- of a coercion variable; never as the argument or result of a
+ -- 'FunTy' (unlike the 'PredType' constructors 'ClassP' or 'IParam')
-- See Note [PredTy], and Note [Equality predicates]
- deriving (Data, Typeable)
+ deriving (Data.Data, Data.Typeable)
-- | The key type representing kinds in the compiler.
-- Invariant: a kind is always in one of these forms:
type SuperKind = Type
\end{code}
+Note [Equality-constrained types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type forall ab. (a ~ [b]) => blah
+is encoded like this:
+
+ ForAllTy (a:*) $ ForAllTy (b:*) $
+ FunTy (PredTy (EqPred a [b]) $
+ blah
+
-------------------------------------
Note [PredTy]
-- > h :: (r\l) => {r} => {l::Int | r}
--
-- Here the @Eq a@ and @?x :: Int -> Int@ and @r\l@ are all called \"predicates\"
-data PredType
- = ClassP Class [Type] -- ^ Class predicate e.g. @Eq a@
- | IParam (IPName Name) Type -- ^ Implicit parameter e.g. @?x :: Int@
- | EqPred Type Type -- ^ Equality predicate e.g @ty1 ~ ty2@
- deriving (Data, Typeable)
+type PredType = Pred Type
+
+data Pred a -- Typically 'a' is instantiated with Type or Coercion
+ = ClassP Class [a] -- ^ Class predicate e.g. @Eq a@
+ | IParam (IPName Name) a -- ^ Implicit parameter e.g. @?x :: Int@
+ | EqPred a a -- ^ Equality predicate e.g @ty1 ~ ty2@
+ deriving (Data.Data, Data.Typeable, Data.Foldable, Data.Traversable, Functor)
-- | A collection of 'PredType's
type ThetaType = [PredType]
%************************************************************************
%* *
+ Simple constructors
+%* *
+%************************************************************************
+
+These functions are here so that they can be used by TysPrim,
+which in turn is imported by Type
+
+\begin{code}
+mkTyVarTy :: TyVar -> Type
+mkTyVarTy = TyVarTy
+
+mkTyVarTys :: [TyVar] -> [Type]
+mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
+
+-- | A key function: builds a 'TyConApp' or 'FunTy' as apppropriate to its arguments.
+-- Applies its arguments to the constructor from left to right
+mkTyConApp :: TyCon -> [Type] -> Type
+mkTyConApp tycon tys
+ | isFunTyCon tycon, [ty1,ty2] <- tys
+ = FunTy ty1 ty2
+
+ | otherwise
+ = TyConApp tycon tys
+
+-- | Create the plain type constructor type which has been applied to no type arguments at all.
+mkTyConTy :: TyCon -> Type
+mkTyConTy tycon = mkTyConApp tycon []
+
+isLiftedTypeKind :: Kind -> Bool
+-- This function is here because it's used in the pretty printer
+isLiftedTypeKind (TyConApp tc []) = tc `hasKey` liftedTypeKindTyConKey
+isLiftedTypeKind _ = False
+
+isCoercionKind :: Kind -> Bool
+-- All coercions are of form (ty1 ~ ty2)
+-- This function is here rather than in Coercion, because it
+-- is used in a knot-tied way to enforce invariants in Var
+isCoercionKind (PredTy (EqPred {})) = True
+isCoercionKind _ = False
+\end{code}
+
+
+%************************************************************************
+%* *
+ Free variables of types and coercions
+%* *
+%************************************************************************
+
+\begin{code}
+tyVarsOfPred :: PredType -> TyCoVarSet
+tyVarsOfPred = varsOfPred tyVarsOfType
+
+tyVarsOfTheta :: ThetaType -> TyCoVarSet
+tyVarsOfTheta = varsOfTheta tyVarsOfType
+
+tyVarsOfType :: Type -> VarSet
+-- ^ NB: for type synonyms tyVarsOfType does /not/ expand the synonym
+tyVarsOfType (TyVarTy v) = unitVarSet v
+tyVarsOfType (TyConApp _ tys) = tyVarsOfTypes tys
+tyVarsOfType (PredTy sty) = varsOfPred tyVarsOfType sty
+tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res
+tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg
+tyVarsOfType (ForAllTy tyvar ty) = delVarSet (tyVarsOfType ty) tyvar
+
+tyVarsOfTypes :: [Type] -> TyVarSet
+tyVarsOfTypes tys = foldr (unionVarSet . tyVarsOfType) emptyVarSet tys
+
+varsOfPred :: (a -> VarSet) -> Pred a -> VarSet
+varsOfPred f (IParam _ ty) = f ty
+varsOfPred f (ClassP _ tys) = foldr (unionVarSet . f) emptyVarSet tys
+varsOfPred f (EqPred ty1 ty2) = f ty1 `unionVarSet` f ty2
+
+varsOfTheta :: (a -> VarSet) -> [Pred a] -> VarSet
+varsOfTheta f = foldr (unionVarSet . varsOfPred f) emptyVarSet
+
+predSize :: (a -> Int) -> Pred a -> Int
+predSize size (IParam _ t) = 1 + size t
+predSize size (ClassP _ ts) = 1 + sum (map size ts)
+predSize size (EqPred t1 t2) = size t1 + size t2
+\end{code}
+
+%************************************************************************
+%* *
TyThing
%* *
%************************************************************************
data TyThing = AnId Id
| ADataCon DataCon
| ATyCon TyCon
+ | ACoAxiom CoAxiom
| AClass Class
instance Outputable TyThing where
pprTyThingCategory :: TyThing -> SDoc
pprTyThingCategory (ATyCon _) = ptext (sLit "Type constructor")
+pprTyThingCategory (ACoAxiom _) = ptext (sLit "Coercion axiom")
pprTyThingCategory (AClass _) = ptext (sLit "Class")
pprTyThingCategory (AnId _) = ptext (sLit "Identifier")
pprTyThingCategory (ADataCon _) = ptext (sLit "Data constructor")
instance NamedThing TyThing where -- Can't put this with the type
getName (AnId id) = getName id -- decl, because the DataCon instance
getName (ATyCon tc) = getName tc -- isn't visible there
+ getName (ACoAxiom cc) = getName cc
getName (AClass cl) = getName cl
getName (ADataCon dc) = dataConName dc
\end{code}
%************************************************************************
%* *
- Wired-in type constructors
+ Substitutions
+ Data type defined here to avoid unnecessary mutual recursion
%* *
%************************************************************************
-We define a few wired-in type constructors here to avoid module knots
-
\begin{code}
---------------------------
--- First the TyCons...
-
--- | See "Type#kind_subtyping" for details of the distinction between the 'Kind' 'TyCon's
-funTyCon, tySuperKindTyCon, coSuperKindTyCon, liftedTypeKindTyCon,
- openTypeKindTyCon, unliftedTypeKindTyCon,
- ubxTupleKindTyCon, argTypeKindTyCon
- :: TyCon
-funTyConName, tySuperKindTyConName, coSuperKindTyConName, liftedTypeKindTyConName,
- openTypeKindTyConName, unliftedTypeKindTyConName,
- ubxTupleKindTyConName, argTypeKindTyConName
- :: Name
-
-funTyCon = mkFunTyCon funTyConName (mkArrowKinds [argTypeKind, openTypeKind] liftedTypeKind)
- -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
- -- But if we do that we get kind errors when saying
- -- instance Control.Arrow (->)
- -- becuase the expected kind is (*->*->*). The trouble is that the
- -- expected/actual stuff in the unifier does not go contra-variant, whereas
- -- the kind sub-typing does. Sigh. It really only matters if you use (->) in
- -- a prefix way, thus: (->) Int# Int#. And this is unusual.
-
-
-tySuperKindTyCon = mkSuperKindTyCon tySuperKindTyConName
-coSuperKindTyCon = mkSuperKindTyCon coSuperKindTyConName
-
-liftedTypeKindTyCon = mkKindTyCon liftedTypeKindTyConName tySuperKind
-openTypeKindTyCon = mkKindTyCon openTypeKindTyConName tySuperKind
-unliftedTypeKindTyCon = mkKindTyCon unliftedTypeKindTyConName tySuperKind
-ubxTupleKindTyCon = mkKindTyCon ubxTupleKindTyConName tySuperKind
-argTypeKindTyCon = mkKindTyCon argTypeKindTyConName tySuperKind
-
---------------------------
--- ... and now their names
-
-tySuperKindTyConName = mkPrimTyConName (fsLit "BOX") tySuperKindTyConKey tySuperKindTyCon
-coSuperKindTyConName = mkPrimTyConName (fsLit "COERCION") coSuperKindTyConKey coSuperKindTyCon
-liftedTypeKindTyConName = mkPrimTyConName (fsLit "*") liftedTypeKindTyConKey liftedTypeKindTyCon
-openTypeKindTyConName = mkPrimTyConName (fsLit "?") openTypeKindTyConKey openTypeKindTyCon
-unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
-ubxTupleKindTyConName = mkPrimTyConName (fsLit "(#)") ubxTupleKindTyConKey ubxTupleKindTyCon
-argTypeKindTyConName = mkPrimTyConName (fsLit "??") argTypeKindTyConKey argTypeKindTyCon
-funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
-
-mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
-mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
- key
- (ATyCon tycon)
- BuiltInSyntax
- -- All of the super kinds and kinds are defined in Prim and use BuiltInSyntax,
- -- because they are never in scope in the source
-
-------------------
--- We also need Kinds and SuperKinds, locally and in TyCon
-
-kindTyConType :: TyCon -> Type
-kindTyConType kind = TyConApp kind []
-
--- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
-liftedTypeKind, unliftedTypeKind, openTypeKind, argTypeKind, ubxTupleKind :: Kind
-
-liftedTypeKind = kindTyConType liftedTypeKindTyCon
-unliftedTypeKind = kindTyConType unliftedTypeKindTyCon
-openTypeKind = kindTyConType openTypeKindTyCon
-argTypeKind = kindTyConType argTypeKindTyCon
-ubxTupleKind = kindTyConType ubxTupleKindTyCon
+-- | Type substitution
+--
+-- #tvsubst_invariant#
+-- The following invariants must hold of a 'TvSubst':
+--
+-- 1. The in-scope set is needed /only/ to
+-- guide the generation of fresh uniques
+--
+-- 2. In particular, the /kind/ of the type variables in
+-- the in-scope set is not relevant
+--
+-- 3. The substition is only applied ONCE! This is because
+-- in general such application will not reached a fixed point.
+data TvSubst
+ = TvSubst InScopeSet -- The in-scope type variables
+ TvSubstEnv -- Substitution of types
+ -- See Note [Apply Once]
+ -- and Note [Extending the TvSubstEnv]
+
+-- | A substitition of 'Type's for 'TyVar's
+type TvSubstEnv = TyVarEnv Type
+ -- A TvSubstEnv is used both inside a TvSubst (with the apply-once
+ -- invariant discussed in Note [Apply Once]), and also independently
+ -- in the middle of matching, and unification (see Types.Unify)
+ -- So you have to look at the context to know if it's idempotent or
+ -- apply-once or whatever
+\end{code}
--- | Given two kinds @k1@ and @k2@, creates the 'Kind' @k1 -> k2@
-mkArrowKind :: Kind -> Kind -> Kind
-mkArrowKind k1 k2 = FunTy k1 k2
+Note [Apply Once]
+~~~~~~~~~~~~~~~~~
+We use TvSubsts to instantiate things, and we might instantiate
+ forall a b. ty
+\with the types
+ [a, b], or [b, a].
+So the substition might go [a->b, b->a]. A similar situation arises in Core
+when we find a beta redex like
+ (/\ a /\ b -> e) b a
+Then we also end up with a substition that permutes type variables. Other
+variations happen to; for example [a -> (a, b)].
--- | Iterated application of 'mkArrowKind'
-mkArrowKinds :: [Kind] -> Kind -> Kind
-mkArrowKinds arg_kinds result_kind = foldr mkArrowKind result_kind arg_kinds
+ ***************************************************
+ *** So a TvSubst must be applied precisely once ***
+ ***************************************************
-tySuperKind, coSuperKind :: SuperKind
-tySuperKind = kindTyConType tySuperKindTyCon
-coSuperKind = kindTyConType coSuperKindTyCon
+A TvSubst is not idempotent, but, unlike the non-idempotent substitution
+we use during unifications, it must not be repeatedly applied.
-isTySuperKind :: SuperKind -> Bool
-isTySuperKind (TyConApp kc []) = kc `hasKey` tySuperKindTyConKey
-isTySuperKind _ = False
+Note [Extending the TvSubst]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See #tvsubst_invariant# for the invariants that must hold.
-isCoSuperKind :: SuperKind -> Bool
-isCoSuperKind (TyConApp kc []) = kc `hasKey` coSuperKindTyConKey
-isCoSuperKind _ = False
+This invariant allows a short-cut when the TvSubstEnv is empty:
+if the TvSubstEnv is empty --- i.e. (isEmptyTvSubt subst) holds ---
+then (substTy subst ty) does nothing.
--------------------
--- Lastly we need a few functions on Kinds
+For example, consider:
+ (/\a. /\b:(a~Int). ...b..) Int
+We substitute Int for 'a'. The Unique of 'b' does not change, but
+nevertheless we add 'b' to the TvSubstEnv, because b's kind does change
-isLiftedTypeKindCon :: TyCon -> Bool
-isLiftedTypeKindCon tc = tc `hasKey` liftedTypeKindTyConKey
+This invariant has several crucial consequences:
-isLiftedTypeKind :: Kind -> Bool
-isLiftedTypeKind (TyConApp tc []) = isLiftedTypeKindCon tc
-isLiftedTypeKind _ = False
+* In substTyVarBndr, we need extend the TvSubstEnv
+ - if the unique has changed
+ - or if the kind has changed
-isCoercionKind :: Kind -> Bool
--- All coercions are of form (ty1 ~ ty2)
--- This function is here rather than in Coercion,
--- because it's used in a knot-tied way to enforce invariants in Var
-isCoercionKind (PredTy (EqPred {})) = True
-isCoercionKind _ = False
+* In substTyVar, we do not need to consult the in-scope set;
+ the TvSubstEnv is enough
-coVarPred :: CoVar -> PredType
-coVarPred tv
- = ASSERT( isCoVar tv )
- case tyVarKind tv of
- PredTy eq -> eq
- other -> pprPanic "coVarPred" (ppr tv $$ ppr other)
+* In substTy, substTheta, we can short-circuit when the TvSubstEnv is empty
\end{code}
%************************************************************************
%* *
-\subsection{The external interface}
-%* *
+ Pretty-printing types
+
+ Defined very early because of debug printing in assertions
+%* *
%************************************************************************
@pprType@ is the standard @Type@ printer; the overloaded @ppr@ function is
------------------
pprType, pprParendType :: Type -> SDoc
-pprType ty = ppr_type TopPrec ty
+pprType ty = ppr_type TopPrec ty
pprParendType ty = ppr_type TyConPrec ty
-pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
--- The first arg is the tycon, or sometimes class
--- Print infix if the tycon/class looks like an operator
-pprTypeApp tc tys = ppr_type_app TopPrec (getName tc) tys
+pprKind, pprParendKind :: Kind -> SDoc
+pprKind = pprType
+pprParendKind = pprParendType
------------------
-pprPred :: PredType -> SDoc
-pprPred (ClassP cls tys) = pprClassPred cls tys
-pprPred (IParam ip ty) = ppr ip <> dcolon <> pprType ty
-pprPred (EqPred ty1 ty2) = pprEqPred (ty1,ty2)
-
-pprEqPred :: (Type,Type) -> SDoc
-pprEqPred (ty1,ty2) = sep [ ppr_type FunPrec ty1
- , nest 2 (ptext (sLit "~"))
- , ppr_type FunPrec ty2]
+pprPredTy :: PredType -> SDoc
+pprPredTy = pprPred ppr_type
+
+pprPred :: (Prec -> a -> SDoc) -> Pred a -> SDoc
+pprPred pp (ClassP cls tys) = ppr_class_pred pp cls tys
+pprPred pp (IParam ip ty) = ppr ip <> dcolon <> pp TopPrec ty
+pprPred pp (EqPred ty1 ty2) = ppr_eq_pred pp (Pair ty1 ty2)
+
+------------
+pprEqPred :: Pair Type -> SDoc
+pprEqPred = ppr_eq_pred ppr_type
+
+ppr_eq_pred :: (Prec -> a -> SDoc) -> Pair a -> SDoc
+ppr_eq_pred pp (Pair ty1 ty2) = sep [ pp FunPrec ty1
+ , nest 2 (ptext (sLit "~"))
+ , pp FunPrec ty2]
-- Precedence looks like (->) so that we get
-- Maybe a ~ Bool
-- (a->a) ~ Bool
-- Note parens on the latter!
+------------
pprClassPred :: Class -> [Type] -> SDoc
-pprClassPred clas tys = ppr_type_app TopPrec (getName clas) tys
+pprClassPred = ppr_class_pred ppr_type
+ppr_class_pred :: (Prec -> a -> SDoc) -> Class -> [a] -> SDoc
+ppr_class_pred pp clas tys = pprTypeNameApp TopPrec pp (getName clas) tys
+
+------------
pprTheta :: ThetaType -> SDoc
-- pprTheta [pred] = pprPred pred -- I'm in two minds about this
-pprTheta theta = parens (sep (punctuate comma (map pprPred theta)))
+pprTheta theta = parens (sep (punctuate comma (map pprPredTy theta)))
+
+pprThetaArrowTy :: ThetaType -> SDoc
+pprThetaArrowTy = pprThetaArrow ppr_type
-pprThetaArrow :: ThetaType -> SDoc
-pprThetaArrow [] = empty
-pprThetaArrow [pred]
- | noParenPred pred = pprPred pred <+> darrow
-pprThetaArrow preds = parens (sep (punctuate comma (map pprPred preds))) <+> darrow
+pprThetaArrow :: (Prec -> a -> SDoc) -> [Pred a] -> SDoc
+pprThetaArrow _ [] = empty
+pprThetaArrow pp [pred]
+ | noParenPred pred = pprPred pp pred <+> darrow
+pprThetaArrow pp preds = parens (sep (punctuate comma (map (pprPred pp) preds)))
+ <+> darrow
-noParenPred :: PredType -> Bool
+noParenPred :: Pred a -> Bool
-- A predicate that can appear without parens before a "=>"
-- C a => a -> a
-- a~b => a -> b
instance Outputable Type where
ppr ty = pprType ty
-instance Outputable PredType where
- ppr = pprPred
+instance Outputable (Pred Type) where
+ ppr = pprPredTy -- Not for arbitrary (Pred a), because the
+ -- (Outputable a) doesn't give precedence
instance Outputable name => OutputableBndr (IPName name) where
pprBndr _ n = ppr n -- Simple for now
------------------
-- OK, here's the main printer
-pprKind, pprParendKind :: Kind -> SDoc
-pprKind = pprType
-pprParendKind = pprParendType
-
ppr_type :: Prec -> Type -> SDoc
- ppr_type _ (TyVarTy tv) -- Note [Infix type variables]
- | isSymOcc (getOccName tv) = parens (ppr tv)
- | otherwise = ppr tv
+ ppr_type _ (TyVarTy tv) = ppr_tvar tv
ppr_type p (PredTy pred) = maybeParen p TyConPrec $
- ifPprDebug (ptext (sLit "<pred>")) <> (ppr pred)
-ppr_type p (TyConApp tc tys) = ppr_tc_app p tc tys
+ ifPprDebug (ptext (sLit "<pred>")) <> (pprPredTy pred)
+ppr_type p (TyConApp tc tys) = pprTcApp p ppr_type tc tys
ppr_type p (AppTy t1 t2) = maybeParen p TyConPrec $
pprType t1 <+> ppr_type TyConPrec t2
-ppr_type p ty@(ForAllTy _ _) = ppr_forall_type p ty
+ppr_type p ty@(ForAllTy {}) = ppr_forall_type p ty
ppr_type p ty@(FunTy (PredTy _) _) = ppr_forall_type p ty
ppr_type p (FunTy ty1 ty2)
- = -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
- maybeParen p FunPrec $
- sep (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
+ = pprArrowChain p (ppr_type FunPrec ty1 : ppr_fun_tail ty2)
where
- ppr_fun_tail (FunTy ty1 ty2)
- | not (is_pred ty1) = (arrow <+> ppr_type FunPrec ty1) : ppr_fun_tail ty2
- ppr_fun_tail other_ty = [arrow <+> pprType other_ty]
+ -- We don't want to lose synonyms, so we mustn't use splitFunTys here.
+ ppr_fun_tail (FunTy ty1 ty2)
+ | not (is_pred ty1) = ppr_type FunPrec ty1 : ppr_fun_tail ty2
+ ppr_fun_tail other_ty = [ppr_type TopPrec other_ty]
+
is_pred (PredTy {}) = True
is_pred _ = False
ppr_forall_type :: Prec -> Type -> SDoc
ppr_forall_type p ty
= maybeParen p FunPrec $
- sep [pprForAll tvs, pprThetaArrow ctxt, pprType tau]
+ sep [pprForAll tvs, pprThetaArrowTy ctxt, pprType tau]
where
(tvs, rho) = split1 [] ty
(ctxt, tau) = split2 [] rho
- -- We need to be extra careful here as equality constraints will occur as
- -- type variables with an equality kind. So, while collecting quantified
- -- variables, we separate the coercion variables out and turn them into
- -- equality predicates.
- split1 tvs (ForAllTy tv ty)
- | not (isCoVar tv) = split1 (tv:tvs) ty
- split1 tvs ty = (reverse tvs, ty)
+ split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
+ split1 tvs ty = (reverse tvs, ty)
split2 ps (PredTy p `FunTy` ty) = split2 (p:ps) ty
- split2 ps (ForAllTy tv ty)
- | isCoVar tv = split2 (coVarPred tv : ps) ty
split2 ps ty = (reverse ps, ty)
- -------------------
-ppr_tc_app :: Prec -> TyCon -> [Type] -> SDoc
-ppr_tc_app _ tc []
- = ppr_tc tc
-ppr_tc_app _ tc [ty]
- | tc `hasKey` listTyConKey = brackets (pprType ty)
- | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pprType ty <> ptext (sLit ":]")
- | tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
- | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
- | tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
- | tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
- | tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
-
-ppr_tc_app p tc tys
- | isTupleTyCon tc && tyConArity tc == length tys
- = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map pprType tys)))
- | otherwise
- = ppr_type_app p (getName tc) tys
-
-ppr_type_app :: Prec -> Name -> [Type] -> SDoc
--- Used for classes as well as types; that's why it's separate from ppr_tc_app
-ppr_type_app p tc tys
- | is_sym_occ -- Print infix if possible
- , [ty1,ty2] <- tys -- We know nothing of precedence though
- = maybeParen p FunPrec (sep [ppr_type FunPrec ty1,
- pprInfixVar True (ppr tc) <+> ppr_type FunPrec ty2])
- | otherwise
- = maybeParen p TyConPrec (hang (pprPrefixVar is_sym_occ (ppr tc))
- 2 (sep (map pprParendType tys)))
- where
- is_sym_occ = isSymOcc (getOccName tc)
-
-ppr_tc :: TyCon -> SDoc -- No brackets for SymOcc
-ppr_tc tc
- = pp_nt_debug <> ppr tc
- where
- pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
- then ptext (sLit "<recnt>")
- else ptext (sLit "<nt>"))
- | otherwise = empty
-
+ ppr_tvar :: TyVar -> SDoc
+ ppr_tvar tv -- Note [Infix type variables]
+ | isSymOcc (getOccName tv) = parens (ppr tv)
+ | otherwise = ppr tv
+
--------------------
pprForAll :: [TyVar] -> SDoc
pprForAll [] = empty
pprForAll tvs = ptext (sLit "forall") <+> sep (map pprTvBndr tvs) <> dot
pprTvBndr :: TyVar -> SDoc
-pprTvBndr tv | isLiftedTypeKind kind = ppr_tvar tv
- | otherwise = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
- where
- kind = tyVarKind tv
+pprTvBndr tv
- | isLiftedTypeKind kind = ppr tv
- | otherwise = parens (ppr tv <+> dcolon <+> pprKind kind)
++ | isLiftedTypeKind kind = ppr_tvar tv
++ | otherwise = parens (ppr_tvar tv <+> dcolon <+> pprKind kind)
+ where
+ kind = tyVarKind tv
\end{code}
Note [Infix type variables]
See Trac #2766.
+\begin{code}
+pprTcApp :: Prec -> (Prec -> a -> SDoc) -> TyCon -> [a] -> SDoc
+pprTcApp _ _ tc [] -- No brackets for SymOcc
+ = pp_nt_debug <> ppr tc
+ where
+ pp_nt_debug | isNewTyCon tc = ifPprDebug (if isRecursiveTyCon tc
+ then ptext (sLit "<recnt>")
+ else ptext (sLit "<nt>"))
+ | otherwise = empty
+pprTcApp _ pp tc [ty]
+ | tc `hasKey` listTyConKey = brackets (pp TopPrec ty)
+ | tc `hasKey` parrTyConKey = ptext (sLit "[:") <> pp TopPrec ty <> ptext (sLit ":]")
+ | tc `hasKey` liftedTypeKindTyConKey = ptext (sLit "*")
+ | tc `hasKey` unliftedTypeKindTyConKey = ptext (sLit "#")
+ | tc `hasKey` openTypeKindTyConKey = ptext (sLit "(?)")
+ | tc `hasKey` ubxTupleKindTyConKey = ptext (sLit "(#)")
+ | tc `hasKey` argTypeKindTyConKey = ptext (sLit "??")
+pprTcApp p pp tc tys
+ | isTupleTyCon tc && tyConArity tc == length tys
+ = tupleParens (tupleTyConBoxity tc) (sep (punctuate comma (map (pp TopPrec) tys)))
+ | otherwise
+ = pprTypeNameApp p pp (getName tc) tys
+
+----------------
+pprTypeApp :: NamedThing a => a -> [Type] -> SDoc
+-- The first arg is the tycon, or sometimes class
+-- Print infix if the tycon/class looks like an operator
+pprTypeApp tc tys = pprTypeNameApp TopPrec ppr_type (getName tc) tys
+
+pprTypeNameApp :: Prec -> (Prec -> a -> SDoc) -> Name -> [a] -> SDoc
+-- Used for classes and coercions as well as types; that's why it's separate from pprTcApp
+pprTypeNameApp p pp tc tys
+ | is_sym_occ -- Print infix if possible
+ , [ty1,ty2] <- tys -- We know nothing of precedence though
+ = maybeParen p FunPrec $
+ sep [pp FunPrec ty1, pprInfixVar True (ppr tc) <+> pp FunPrec ty2]
+ | otherwise
+ = pprPrefixApp p (pprPrefixVar is_sym_occ (ppr tc)) (map (pp TyConPrec) tys)
+ where
+ is_sym_occ = isSymOcc (getOccName tc)
+
+----------------
+pprPrefixApp :: Prec -> SDoc -> [SDoc] -> SDoc
+pprPrefixApp p pp_fun pp_tys = maybeParen p TyConPrec $
+ hang pp_fun 2 (sep pp_tys)
+
+----------------
+pprArrowChain :: Prec -> [SDoc] -> SDoc
+-- pprArrowChain p [a,b,c] generates a -> b -> c
+pprArrowChain _ [] = empty
+pprArrowChain p (arg:args) = maybeParen p FunPrec $
+ sep [arg, sep (map (arrow <+>) args)]
+\end{code}
projects / ghc-hetmet.git / commitdiff