From 74ad75e87317196c600dfabc61aee1b87d95c214 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Wed, 2 Oct 2019 12:36:44 +0300 Subject: Re-implement unsafe coercions in terms of unsafe equality proofs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit (Commit message written by Omer, most of the code is written by Simon and Richard) See Note [Implementing unsafeCoerce] for how unsafe equality proofs and the new unsafeCoerce# are implemented. New notes added: - [Checking for levity polymorphism] in CoreLint.hs - [Implementing unsafeCoerce] in base/Unsafe/Coerce.hs - [Patching magic definitions] in Desugar.hs - [Wiring in unsafeCoerce#] in Desugar.hs Only breaking change in this patch is unsafeCoerce# is not exported from GHC.Exts, instead of GHC.Prim. Fixes #17443 Fixes #16893 NoFib ----- -------------------------------------------------------------------------------- Program Size Allocs Instrs Reads Writes -------------------------------------------------------------------------------- CS -0.1% 0.0% -0.0% -0.0% -0.0% CSD -0.1% 0.0% -0.0% -0.0% -0.0% FS -0.1% 0.0% -0.0% -0.0% -0.0% S -0.1% 0.0% -0.0% -0.0% -0.0% VS -0.1% 0.0% -0.0% -0.0% -0.0% VSD -0.1% 0.0% -0.0% -0.0% -0.1% VSM -0.1% 0.0% -0.0% -0.0% -0.0% anna -0.0% 0.0% -0.0% -0.0% -0.0% ansi -0.1% 0.0% -0.0% -0.0% -0.0% atom -0.1% 0.0% -0.0% -0.0% -0.0% awards -0.1% 0.0% -0.0% -0.0% -0.0% banner -0.1% 0.0% -0.0% -0.0% -0.0% bernouilli -0.1% 0.0% -0.0% -0.0% -0.0% binary-trees -0.1% 0.0% -0.0% -0.0% -0.0% boyer -0.1% 0.0% -0.0% -0.0% -0.0% boyer2 -0.1% 0.0% -0.0% -0.0% -0.0% bspt -0.1% 0.0% -0.0% -0.0% -0.0% cacheprof -0.1% 0.0% -0.0% -0.0% -0.0% calendar -0.1% 0.0% -0.0% -0.0% -0.0% cichelli -0.1% 0.0% -0.0% -0.0% -0.0% circsim -0.1% 0.0% -0.0% -0.0% -0.0% clausify -0.1% 0.0% -0.0% -0.0% -0.0% comp_lab_zift -0.1% 0.0% -0.0% -0.0% -0.0% compress -0.1% 0.0% -0.0% -0.0% -0.0% compress2 -0.1% 0.0% -0.0% -0.0% -0.0% constraints -0.1% 0.0% -0.0% -0.0% -0.0% cryptarithm1 -0.1% 0.0% -0.0% -0.0% -0.0% cryptarithm2 -0.1% 0.0% -0.0% -0.0% -0.0% cse -0.1% 0.0% -0.0% -0.0% -0.0% digits-of-e1 -0.1% 0.0% -0.0% -0.0% -0.0% digits-of-e2 -0.1% 0.0% -0.0% -0.0% -0.0% dom-lt -0.1% 0.0% -0.0% -0.0% -0.0% eliza -0.1% 0.0% -0.0% -0.0% -0.0% event -0.1% 0.0% -0.0% -0.0% -0.0% exact-reals -0.1% 0.0% -0.0% -0.0% -0.0% exp3_8 -0.1% 0.0% -0.0% -0.0% -0.0% expert -0.1% 0.0% -0.0% -0.0% -0.0% fannkuch-redux -0.1% 0.0% -0.0% -0.0% -0.0% fasta -0.1% 0.0% -0.5% -0.3% -0.4% fem -0.1% 0.0% -0.0% -0.0% -0.0% fft -0.1% 0.0% -0.0% -0.0% -0.0% fft2 -0.1% 0.0% -0.0% -0.0% -0.0% fibheaps -0.1% 0.0% -0.0% -0.0% -0.0% fish -0.1% 0.0% -0.0% -0.0% -0.0% fluid -0.1% 0.0% -0.0% -0.0% -0.0% fulsom -0.1% 0.0% +0.0% +0.0% +0.0% gamteb -0.1% 0.0% -0.0% -0.0% -0.0% gcd -0.1% 0.0% -0.0% -0.0% -0.0% gen_regexps -0.1% 0.0% -0.0% -0.0% -0.0% genfft -0.1% 0.0% -0.0% -0.0% -0.0% gg -0.1% 0.0% -0.0% -0.0% -0.0% grep -0.1% 0.0% -0.0% -0.0% -0.0% hidden -0.1% 0.0% -0.0% -0.0% -0.0% hpg -0.1% 0.0% -0.0% -0.0% -0.0% ida -0.1% 0.0% -0.0% -0.0% -0.0% infer -0.1% 0.0% -0.0% -0.0% -0.0% integer -0.1% 0.0% -0.0% -0.0% -0.0% integrate -0.1% 0.0% -0.0% -0.0% -0.0% k-nucleotide -0.1% 0.0% -0.0% -0.0% -0.0% kahan -0.1% 0.0% -0.0% -0.0% -0.0% knights -0.1% 0.0% -0.0% -0.0% -0.0% lambda -0.1% 0.0% -0.0% -0.0% -0.0% last-piece -0.1% 0.0% -0.0% -0.0% -0.0% lcss -0.1% 0.0% -0.0% -0.0% -0.0% life -0.1% 0.0% -0.0% -0.0% -0.0% lift -0.1% 0.0% -0.0% -0.0% -0.0% linear -0.1% 0.0% -0.0% -0.0% -0.0% listcompr -0.1% 0.0% -0.0% -0.0% -0.0% listcopy -0.1% 0.0% -0.0% -0.0% -0.0% maillist -0.1% 0.0% -0.0% -0.0% -0.0% mandel -0.1% 0.0% -0.0% -0.0% -0.0% mandel2 -0.1% 0.0% -0.0% -0.0% -0.0% mate -0.1% 0.0% -0.0% -0.0% -0.0% minimax -0.1% 0.0% -0.0% -0.0% -0.0% mkhprog -0.1% 0.0% -0.0% -0.0% -0.0% multiplier -0.1% 0.0% -0.0% -0.0% -0.0% n-body -0.1% 0.0% -0.0% -0.0% -0.0% nucleic2 -0.1% 0.0% -0.0% -0.0% -0.0% para -0.1% 0.0% -0.0% -0.0% -0.0% paraffins -0.1% 0.0% -0.0% -0.0% -0.0% parser -0.1% 0.0% -0.0% -0.0% -0.0% parstof -0.1% 0.0% -0.0% -0.0% -0.0% pic -0.1% 0.0% -0.0% -0.0% -0.0% pidigits -0.1% 0.0% -0.0% -0.0% -0.0% power -0.1% 0.0% -0.0% -0.0% -0.0% pretty -0.1% 0.0% -0.1% -0.1% -0.1% primes -0.1% 0.0% -0.0% -0.0% -0.0% primetest -0.1% 0.0% -0.0% -0.0% -0.0% prolog -0.1% 0.0% -0.0% -0.0% -0.0% puzzle -0.1% 0.0% -0.0% -0.0% -0.0% queens -0.1% 0.0% -0.0% -0.0% -0.0% reptile -0.1% 0.0% -0.0% -0.0% -0.0% reverse-complem -0.1% 0.0% -0.0% -0.0% -0.0% rewrite -0.1% 0.0% -0.0% -0.0% -0.0% rfib -0.1% 0.0% -0.0% -0.0% -0.0% rsa -0.1% 0.0% -0.0% -0.0% -0.0% scc -0.1% 0.0% -0.1% -0.1% -0.1% sched -0.1% 0.0% -0.0% -0.0% -0.0% scs -0.1% 0.0% -0.0% -0.0% -0.0% simple -0.1% 0.0% -0.0% -0.0% -0.0% solid -0.1% 0.0% -0.0% -0.0% -0.0% sorting -0.1% 0.0% -0.0% -0.0% -0.0% spectral-norm -0.1% 0.0% -0.0% -0.0% -0.0% sphere -0.1% 0.0% -0.0% -0.0% -0.0% symalg -0.1% 0.0% -0.0% -0.0% -0.0% tak -0.1% 0.0% -0.0% -0.0% -0.0% transform -0.1% 0.0% -0.0% -0.0% -0.0% treejoin -0.1% 0.0% -0.0% -0.0% -0.0% typecheck -0.1% 0.0% -0.0% -0.0% -0.0% veritas -0.0% 0.0% -0.0% -0.0% -0.0% wang -0.1% 0.0% -0.0% -0.0% -0.0% wave4main -0.1% 0.0% -0.0% -0.0% -0.0% wheel-sieve1 -0.1% 0.0% -0.0% -0.0% -0.0% wheel-sieve2 -0.1% 0.0% -0.0% -0.0% -0.0% x2n1 -0.1% 0.0% -0.0% -0.0% -0.0% -------------------------------------------------------------------------------- Min -0.1% 0.0% -0.5% -0.3% -0.4% Max -0.0% 0.0% +0.0% +0.0% +0.0% Geometric Mean -0.1% -0.0% -0.0% -0.0% -0.0% Test changes ------------ - break006 is marked as broken, see #17833 - The compiler allocates less when building T14683 (an unsafeCoerce#- heavy happy-generated code) on 64-platforms. Allocates more on 32-bit platforms. - Rest of the increases are tiny amounts (still enough to pass the threshold) in micro-benchmarks. I briefly looked at each one in a profiling build: most of the increased allocations seem to be because of random changes in the generated code. Metric Decrease: T14683 Metric Increase: T12150 T12234 T12425 T13035 T14683 T5837 T6048 Co-Authored-By: Richard Eisenberg Co-Authored-By: Ömer Sinan Ağacan --- compiler/GHC/HsToCore.hs | 227 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 219 insertions(+), 8 deletions(-) (limited to 'compiler/GHC/HsToCore.hs') diff --git a/compiler/GHC/HsToCore.hs b/compiler/GHC/HsToCore.hs index 6802319be2..fc290737ca 100644 --- a/compiler/GHC/HsToCore.hs +++ b/compiler/GHC/HsToCore.hs @@ -9,6 +9,7 @@ The Desugarer: turning HsSyn into Core. {-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module GHC.HsToCore ( -- * Desugaring operations @@ -27,29 +28,32 @@ import TcRnTypes import TcRnMonad ( finalSafeMode, fixSafeInstances ) import TcRnDriver ( runTcInteractive ) import Id +import IdInfo import Name import Type +import TyCon ( tyConDataCons ) import Avail import CoreSyn import CoreFVs ( exprsSomeFreeVarsList ) import CoreOpt ( simpleOptPgm, simpleOptExpr ) +import CoreUtils +import CoreUnfold import PprCore import GHC.HsToCore.Monad import GHC.HsToCore.Expr import GHC.HsToCore.Binds import GHC.HsToCore.Foreign.Decl -import PrelNames ( coercibleTyConKey ) -import TysPrim ( eqReprPrimTyCon ) -import Unique ( hasKey ) -import Coercion ( mkCoVarCo ) -import TysWiredIn ( coercibleDataCon ) +import PrelNames +import TysPrim +import Coercion +import TysWiredIn import DataCon ( dataConWrapId ) -import MkCore ( mkCoreLet ) +import MkCore import Module import NameSet import NameEnv import Rules -import BasicTypes ( Activation(.. ), competesWith, pprRuleName ) +import BasicTypes import CoreMonad ( CoreToDo(..) ) import CoreLint ( endPassIO ) import VarSet @@ -130,6 +134,7 @@ deSugar hsc_env ; (msgs, mb_res) <- initDs hsc_env tcg_env $ do { ds_ev_binds <- dsEvBinds ev_binds ; core_prs <- dsTopLHsBinds binds_cvr + ; core_prs <- patchMagicDefns core_prs ; (spec_prs, spec_rules) <- dsImpSpecs imp_specs ; (ds_fords, foreign_prs) <- dsForeigns fords ; ds_rules <- mapMaybeM dsRule rules @@ -506,7 +511,7 @@ For that we replace any forall'ed `c :: Coercible a b` value in a RULE by corresponding `co :: a ~#R b` and wrap the LHS and the RHS in `let c = MkCoercible co in ...`. This is later simplified to the desired form by simpleOptExpr (for the LHS) resp. the simplifiers (for the RHS). -See also Note [Getting the map/coerce RULE to work] in CoreSubst. +See also Note [Getting the map/coerce RULE to work] in CoreOpt. Note [Rules and inlining/other rules] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -543,3 +548,209 @@ firing. But it's not clear what to do instead. We could make the class method rules inactive in phase 2, but that would delay when subsequent transformations could fire. -} + +{- +************************************************************************ +* * +* Magic definitions +* * +************************************************************************ + +Note [Patching magic definitions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We sometimes need to have access to defined Ids in pure contexts. Usually, we +simply "wire in" these entities, as we do for types in TysWiredIn and for Ids +in MkId. See Note [Wired-in Ids] in MkId. + +However, it is sometimes *much* easier to define entities in Haskell, +even if we need pure access; note that wiring-in an Id requires all +entities used in its definition *also* to be wired in, transitively +and recursively. This can be a huge pain. The little trick +documented here allows us to have the best of both worlds. + +Motivating example: unsafeCoerce#. See [Wiring in unsafeCoerce#] for the +details. + +The trick is to + +* Define the known-key Id in a library module, with a stub definition, + unsafeCoerce# :: ..a suitable type signature.. + unsafeCoerce# = error "urk" + +* Magically over-write its RHS here in the desugarer, in + patchMagicDefns. This update can be done with full access to the + DsM monad, and hence, dsLookupGlobal. We thus do not have to wire in + all the entities used internally, a potentially big win. + + This step should not change the Name or type of the Id. + +Because an Id stores its unfolding directly (as opposed to in the second +component of a (Id, CoreExpr) pair), the patchMagicDefns function returns +a new Id to use. + +Here are the moving parts: + +- patchMagicDefns checks whether we're in a module with magic definitions; + if so, patch the magic definitions. If not, skip. + +- patchMagicDefn just looks up in an environment to find a magic defn and + patches it in. + +- magicDefns holds the magic definitions. + +- magicDefnsEnv allows for quick access to magicDefns. + +- magicDefnModules, built also from magicDefns, contains the modules that + need careful attention. + +Note [Wiring in unsafeCoerce#] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We want (Haskell) + + unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) + (a :: TYPE r1) (b :: TYPE r2). + a -> b + unsafeCoerce# x = case unsafeEqualityProof @r1 @r2 of + UnsafeRefl -> case unsafeEqualityProof @a @b of + UnsafeRefl -> x + +or (Core) + + unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) + (a :: TYPE r1) (b :: TYPE r2). + a -> b + unsafeCoerce# = \ @r1 @r2 @a @b (x :: a). + case unsafeEqualityProof @RuntimeRep @r1 @r2 of + UnsafeRefl (co1 :: r1 ~# r2) -> + case unsafeEqualityProof @(TYPE r2) @(a |> TYPE co1) @b of + UnsafeRefl (co2 :: (a |> TYPE co1) ~# b) -> + (x |> (GRefl :: a ~# (a |> TYPE co1)) ; co2) + +It looks like we can write this in Haskell directly, but we can't: +the levity polymorphism checks defeat us. Note that `x` is a levity- +polymorphic variable. So we must wire it in with a compulsory +unfolding, like other levity-polymorphic primops. + +The challenge is that UnsafeEquality is a GADT, and wiring in a GADT +is *hard*: it has a worker separate from its wrapper, with all manner +of complications. (Simon and Richard tried to do this. We nearly wept.) + +The solution is documented in Note [Patching magic definitions]. We now +simply look up the UnsafeEquality GADT in the environment, leaving us +only to wire in unsafeCoerce# directly. + +Wrinkle: +-------- +We must make absolutely sure that unsafeCoerce# is inlined. You might +think that giving it a compulsory unfolding is enough. However, +unsafeCoerce# is put in an interface file like any other definition. +At optimization level 0, we enable -fignore-interface-pragmas, which +ignores pragmas in interface files. We thus must check to see whether +there is a compulsory unfolding, even with -fignore-interface-pragmas. +This is done in TcIface.tcIdInfo. + +Test case: ghci/linker/dyn/T3372 + +-} + + +-- Postcondition: the returned Ids are in one-to-one correspondence as the +-- input Ids; each returned Id has the same type as the passed-in Id. +-- See Note [Patching magic definitions] +patchMagicDefns :: OrdList (Id,CoreExpr) + -> DsM (OrdList (Id,CoreExpr)) +patchMagicDefns pairs + -- optimization: check whether we're in a magic module before looking + -- at all the ids + = do { this_mod <- getModule + ; if this_mod `elemModuleSet` magicDefnModules + then traverse patchMagicDefn pairs + else return pairs } + +patchMagicDefn :: (Id, CoreExpr) -> DsM (Id, CoreExpr) +patchMagicDefn orig_pair@(orig_id, orig_rhs) + | Just mk_magic_pair <- lookupNameEnv magicDefnsEnv (getName orig_id) + = do { magic_pair@(magic_id, _) <- mk_magic_pair orig_id orig_rhs + + -- Patching should not change the Name or the type of the Id + ; MASSERT( getUnique magic_id == getUnique orig_id ) + ; MASSERT( varType magic_id `eqType` varType orig_id ) + + ; return magic_pair } + | otherwise + = return orig_pair + +magicDefns :: [(Name, Id -> CoreExpr -- old Id and RHS + -> DsM (Id, CoreExpr) -- new Id and RHS + )] +magicDefns = [ (unsafeCoercePrimName, mkUnsafeCoercePrimPair) ] + +magicDefnsEnv :: NameEnv (Id -> CoreExpr -> DsM (Id, CoreExpr)) +magicDefnsEnv = mkNameEnv magicDefns + +magicDefnModules :: ModuleSet +magicDefnModules = mkModuleSet $ map (nameModule . getName . fst) magicDefns + +mkUnsafeCoercePrimPair :: Id -> CoreExpr -> DsM (Id, CoreExpr) +-- See Note [Wiring in unsafeCoerce#] for the defn we are creating here +mkUnsafeCoercePrimPair _old_id old_expr + = do { unsafe_equality_proof_id <- dsLookupGlobalId unsafeEqualityProofName + ; unsafe_equality_tc <- dsLookupTyCon unsafeEqualityTyConName + + ; let [unsafe_refl_data_con] = tyConDataCons unsafe_equality_tc + + rhs = mkLams [ runtimeRep1TyVar, runtimeRep2TyVar + , openAlphaTyVar, openBetaTyVar + , x ] $ + mkSingleAltCase scrut1 + (mkWildValBinder scrut1_ty) + (DataAlt unsafe_refl_data_con) + [rr_cv] $ + mkSingleAltCase scrut2 + (mkWildValBinder scrut2_ty) + (DataAlt unsafe_refl_data_con) + [ab_cv] $ + Var x `mkCast` x_co + + [x, rr_cv, ab_cv] = mkTemplateLocals + [ openAlphaTy -- x :: a + , rr_cv_ty -- rr_cv :: r1 ~# r2 + , ab_cv_ty -- ab_cv :: (alpha |> alpha_co ~# beta) + ] + + -- Returns (scrutinee, scrutinee type, type of covar in AltCon) + unsafe_equality k a b + = ( mkTyApps (Var unsafe_equality_proof_id) [k,b,a] + , mkTyConApp unsafe_equality_tc [k,b,a] + , mkHeteroPrimEqPred k k a b + ) + -- NB: UnsafeRefl :: (b ~# a) -> UnsafeEquality a b, so we have to + -- carefully swap the arguments above + + (scrut1, scrut1_ty, rr_cv_ty) = unsafe_equality runtimeRepTy + runtimeRep1Ty + runtimeRep2Ty + (scrut2, scrut2_ty, ab_cv_ty) = unsafe_equality (tYPE runtimeRep2Ty) + (openAlphaTy `mkCastTy` alpha_co) + openBetaTy + + -- alpha_co :: TYPE r1 ~# TYPE r2 + -- alpha_co = TYPE rr_cv + alpha_co = mkTyConAppCo Nominal tYPETyCon [mkCoVarCo rr_cv] + + -- x_co :: alpha ~R# beta + x_co = mkGReflCo Representational openAlphaTy (MCo alpha_co) `mkTransCo` + mkSubCo (mkCoVarCo ab_cv) + + + info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma + `setUnfoldingInfo` mkCompulsoryUnfolding rhs + + ty = mkSpecForAllTys [ runtimeRep1TyVar, runtimeRep2TyVar + , openAlphaTyVar, openBetaTyVar ] $ + mkVisFunTy openAlphaTy openBetaTy + + id = mkExportedVanillaId unsafeCoercePrimName ty `setIdInfo` info + ; return (id, old_expr) } + + where -- cgit v1.2.1