diff options
Diffstat (limited to 'compiler/typecheck/TcInteract.hs')
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 118 |
1 files changed, 86 insertions, 32 deletions
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index bdb11e236c..39424de8c1 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -47,6 +47,7 @@ import FamInstEnv import Unify ( tcUnifyTyWithTFs ) import TcEvidence +import MkCore ( mkStringExprFS, mkNaturalExpr ) import Outputable import TcRnTypes @@ -690,11 +691,11 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble }) = continueWith workItem where - swap_me :: SwapFlag -> CtEvidence -> EvTerm + swap_me :: SwapFlag -> CtEvidence -> EvExpr swap_me swap ev = case swap of - NotSwapped -> ctEvTerm ev - IsSwapped -> EvCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev))) + NotSwapped -> ctEvExpr ev + IsSwapped -> evCoercion (mkTcSymCo (evTermCoercion (EvExpr (ctEvExpr ev)))) interactIrred _ wi = pprPanic "interactIrred" (ppr wi) @@ -1000,9 +1001,9 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs { what_next <- solveOneFromTheOther ev_i ev_w ; traceTcS "lookupInertDict" (ppr what_next) ; case what_next of - KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i) + KeepInert -> do { setEvBindIfWanted ev_w (ctEvExpr ev_i) ; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) } - KeepWork -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w) + KeepWork -> do { setEvBindIfWanted ev_i (ctEvExpr ev_w) ; updInertDicts $ \ ds -> delDict ds cls tys ; continueWith workItem } } } @@ -1056,7 +1057,7 @@ shortCutSolver dflags ev_w ev_i new_wanted_cached cache pty | ClassPred cls tys <- classifyPredType pty = lift $ case findDict cache loc_w cls tys of - Just ctev -> return $ Cached (ctEvTerm ctev) + Just ctev -> return $ Cached (ctEvExpr ctev) Nothing -> Fresh <$> newWantedNC loc_w pty | otherwise = mzero @@ -1092,7 +1093,7 @@ shortCutSolver dflags ev_w ev_i -- so we can solve recursive dictionaries. ; subgoalBinds <- mapM (try_solve_from_instance loc' cache') (freshGoals evc_vs) - ; return $ (mk_ev (map getEvTerm evc_vs), ev, cls, preds) + ; return $ (mk_ev (map getEvExpr evc_vs), ev, cls, preds) : concat subgoalBinds } | otherwise -> mzero @@ -1361,7 +1362,7 @@ reactFunEq from_this fsk1 solve_this fsk2 fsk_eq_pred = mkTcEqPredLikeEv solve_this (mkTyVarTy fsk2) (mkTyVarTy fsk1) - ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co) + ; new_ev <- newGivenEvVar loc (fsk_eq_pred, evCoercion fsk_eq_co) ; emitWorkNC [new_ev] } | CtDerived { ctev_loc = loc } <- solve_this @@ -1549,7 +1550,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv | Just (ev_i, swapped, keep_deriv) <- inertsCanDischarge inerts tv rhs (ctEvFlavour ev, eq_rel) = do { setEvBindIfWanted ev $ - EvCoercion (maybeSym swapped $ + evCoercion (maybeSym swapped $ tcDowngradeRole (eqRelRole eq_rel) (ctEvRole ev_i) (ctEvCoercion ev_i)) @@ -1615,7 +1616,7 @@ solveByUnification wd tv xi text "Right Kind is:" <+> ppr (typeKind xi) ] ; unifyTyVar tv xi - ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi)) } + ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) } ppr_kicked :: Int -> SDoc ppr_kicked 0 = empty @@ -1825,7 +1826,7 @@ reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty) = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co -- final_co :: fsk ~ rhs_ty ; new_ev <- newGivenEvVar deeper_loc (mkPrimEqPred (mkTyVarTy fsk) rhs_ty, - EvCoercion final_co) + evCoercion final_co) ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty ; stopWith old_ev "Fun/Top (given)" } @@ -1948,7 +1949,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args ; new_ev <- case ctEvFlavour old_ev of Given -> newGivenEvVar deeper_loc ( mkPrimEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk) - , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos + , evCoercion (mkTcTyConAppCo Nominal fam_tc cos `mkTcTransCo` mkTcSymCo ax_co `mkTcTransCo` ctEvCoercion old_ev) ) @@ -1984,7 +1985,7 @@ dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS () -- Does not evaluate 'co' if 'ev' is Derived dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi ) - do { setWantedEvTerm dest (EvCoercion co) + do { setWantedEvTerm dest (EvExpr (evCoercion co)) ; unflattenFmv fmv xi ; n_kicked <- kickOutAfterUnification fmv ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) } @@ -2201,7 +2202,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls ; continueWith work_item } | Just ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached - = do { setEvBindIfWanted fl (ctEvTerm ev) + = do { setEvBindIfWanted fl (ctEvExpr ev) ; stopWith fl "Dict/Top (cached)" } | otherwise -- Wanted or Derived, but not cached @@ -2234,12 +2235,12 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls = loc finish_wanted :: [TcPredType] - -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct) + -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct) -- Precondition: evidence term matches the predicate workItem finish_wanted theta mk_ev = do { addSolvedDict fl cls xis ; evc_vars <- mapM (newWanted deeper_loc) theta - ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvTerm evc_vars)) + ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvExpr evc_vars)) ; emitWorkNC (freshGoals evc_vars) ; stopWith fl "Dict/Top (solved wanted)" } @@ -2286,7 +2287,7 @@ type SafeOverlapping = Bool data LookupInstResult = NoInstance | GenInst { lir_new_theta :: [TcPredType] - , lir_mk_ev :: [EvTerm] -> EvTerm + , lir_mk_ev :: [EvExpr] -> EvTerm , lir_safe_over :: SafeOverlapping } instance Outputable LookupInstResult where @@ -2530,7 +2531,7 @@ matchInstEnv dflags short_cut_solver clas tys loc = do { checkWellStagedDFun pred dfun_id loc ; (tys, theta) <- instDFunType dfun_id mb_inst_tys ; return $ GenInst { lir_new_theta = theta - , lir_mk_ev = EvDFunApp dfun_id tys + , lir_mk_ev = EvExpr . evDFunApp dfun_id tys , lir_safe_over = so } } @@ -2548,7 +2549,7 @@ matchCTuple clas tys -- (isCTupleClass clas) holds -- The dfun *is* the data constructor! where data_con = tyConSingleDataCon (classTyCon clas) - tuple_ev = EvDFunApp (dataConWrapId data_con) tys + tuple_ev = EvExpr . evDFunApp (dataConWrapId data_con) tys {- ******************************************************************** * * @@ -2556,17 +2557,70 @@ matchCTuple clas tys -- (isCTupleClass clas) holds * * ***********************************************************************-} +{- +Note [KnownNat & KnownSymbol and EvLit] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A part of the type-level literals implementation are the classes +"KnownNat" and "KnownSymbol", which provide a "smart" constructor for +defining singleton values. Here is the key stuff from GHC.TypeLits + + class KnownNat (n :: Nat) where + natSing :: SNat n + + newtype SNat (n :: Nat) = SNat Integer + +Conceptually, this class has infinitely many instances: + + instance KnownNat 0 where natSing = SNat 0 + instance KnownNat 1 where natSing = SNat 1 + instance KnownNat 2 where natSing = SNat 2 + ... + +In practice, we solve `KnownNat` predicates in the type-checker +(see typecheck/TcInteract.hs) because we can't have infinitely many instances. +The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`. + +We make the following assumptions about dictionaries in GHC: + 1. The "dictionary" for classes with a single method---like `KnownNat`---is + a newtype for the type of the method, so using a evidence amounts + to a coercion, and + 2. Newtypes use the same representation as their definition types. + +So, the evidence for `KnownNat` is just a value of the representation type, +wrapped in two newtype constructors: one to make it into a `SNat` value, +and another to make it into a `KnownNat` dictionary. + +Also note that `natSing` and `SNat` are never actually exposed from the +library---they are just an implementation detail. Instead, users see +a more convenient function, defined in terms of `natSing`: + + natVal :: KnownNat n => proxy n -> Integer + +The reason we don't use this directly in the class is that it is simpler +and more efficient to pass around an integer rather than an entire function, +especially when the `KnowNat` evidence is packaged up in an existential. + +The story for kind `Symbol` is analogous: + * class KnownSymbol + * newtype SSymbol + * Evidence: a Core literal (e.g. mkNaturalExpr) +-} + matchKnownNat :: Class -> [Type] -> TcS LookupInstResult matchKnownNat clas [ty] -- clas = KnownNat - | Just n <- isNumLitTy ty = makeLitDict clas ty (EvNum n) + | Just n <- isNumLitTy ty = do + et <- mkNaturalExpr n + makeLitDict clas ty et matchKnownNat _ _ = return NoInstance matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult matchKnownSymbol clas [ty] -- clas = KnownSymbol - | Just n <- isStrLitTy ty = makeLitDict clas ty (EvStr n) + | Just s <- isStrLitTy ty = do + et <- mkStringExprFS s + makeLitDict clas ty et matchKnownSymbol _ _ = return NoInstance -makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult +makeLitDict :: Class -> Type -> EvExpr -> TcS LookupInstResult -- makeLitDict adds a coercion that will convert the literal into a dictionary -- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit] -- in TcEvidence. The coercion happens in 2 steps: @@ -2577,7 +2631,7 @@ makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult -- The process is mirrored for Symbols: -- String -> SSymbol n -- SSymbol n -> KnownSymbol n -makeLitDict clas ty evLit +makeLitDict clas ty et | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty] -- co_dict :: KnownNat n ~ SNat n , [ meth ] <- classMethods clas @@ -2587,7 +2641,7 @@ makeLitDict clas ty evLit $ idType meth -- forall n. KnownNat n => SNat n , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] -- SNat n ~ Integer - , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep)) + , let ev_tm = EvExpr $ mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep)) = return $ GenInst { lir_new_theta = [] , lir_mk_ev = \_ -> ev_tm , lir_safe_over = True } @@ -2626,7 +2680,7 @@ doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult doFunTy clas ty arg_ty ret_ty = do { let preds = map (mk_typeable_pred clas) [arg_ty, ret_ty] build_ev [arg_ev, ret_ev] = - EvTypeable ty $ EvTypeableTrFun arg_ev ret_ev + evTypeable ty $ EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev) build_ev _ = panic "TcInteract.doFunTy" ; return $ GenInst preds build_ev True } @@ -2637,7 +2691,7 @@ doFunTy clas ty arg_ty ret_ty doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult doTyConApp clas ty tc kind_args = return $ GenInst (map (mk_typeable_pred clas) kind_args) - (\kinds -> EvTypeable ty $ EvTypeableTyCon tc kinds) + (\kinds -> evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds)) True -- | Representation for TyCon applications of a concrete kind. We just use the @@ -2664,7 +2718,7 @@ doTyApp clas ty f tk = return NoInstance -- We can't solve until we know the ctr. | otherwise = return $ GenInst (map (mk_typeable_pred clas) [f, tk]) - (\[t1,t2] -> EvTypeable ty $ EvTypeableTyApp t1 t2) + (\[t1,t2] -> evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)) True -- Emit a `Typeable` constraint for the given type. @@ -2677,7 +2731,7 @@ mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ] doTyLit :: Name -> Type -> TcS LookupInstResult doTyLit kc t = do { kc_clas <- tcLookupClass kc ; let kc_pred = mkClassPred kc_clas [ t ] - mk_ev [ev] = EvTypeable t $ EvTypeableTyLit ev + mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev) mk_ev _ = panic "doTyLit" ; return (GenInst [kc_pred] mk_ev True) } @@ -2730,14 +2784,14 @@ a TypeRep for them. For qualified but not polymorphic types, like matchLiftedEquality :: [Type] -> TcS LookupInstResult matchLiftedEquality args = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ] - , lir_mk_ev = EvDFunApp (dataConWrapId heqDataCon) args + , lir_mk_ev = EvExpr . evDFunApp (dataConWrapId heqDataCon) args , lir_safe_over = True }) -- See also Note [The equality types story] in TysPrim matchLiftedCoercible :: [Type] -> TcS LookupInstResult matchLiftedCoercible args@[k, t1, t2] = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ] - , lir_mk_ev = EvDFunApp (dataConWrapId coercibleDataCon) + , lir_mk_ev = EvExpr . evDFunApp (dataConWrapId coercibleDataCon) args , lir_safe_over = True }) where @@ -2839,9 +2893,9 @@ matchHasField dflags short_cut clas tys loc -- Use the equality proof to cast the selector Id to -- type (r -> a), then use the newtype coercion to cast -- it to a HasField dictionary. - mk_ev (ev1:evs) = EvSelector sel_id tvs evs `EvCast` co + mk_ev (ev1:evs) = EvExpr $ evSelector sel_id tvs evs `evCast` co where - co = mkTcSubCo (evTermCoercion ev1) + co = mkTcSubCo (evTermCoercion (EvExpr ev1)) `mkTcTransCo` mkTcSymCo co2 mk_ev [] = panic "matchHasField.mk_ev" |