diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,21 @@ # Changelog +## 0.1.0.1 + +* `Category` via `Overriding2`: accept the field-keyed override forms + (`Con at i via M`, `name via M`), not only the dense `'[ '[ .. ] ]` + positional list; and fix a kind bug where a modifier's phantom + parameters (e.g. `Basic m a b`) were left at skolem kinds. +* Per-field override reshapes are now validated: an override that maps a + field to a non-coercible modifier (e.g. `Maybe via []`, `Int via Op`) + is rejected with a clear error instead of silently emitting an unsound + coercion. Applies to `Functor`, `Foldable`, `Traversable`, + `Applicative` (`Stock1`) and `Category` (`Stock2`); the other classes + already validated. +* Documentation: fixed the package-description rendering (cabal-version + 3.0 needs real blank lines, not the `.` convention) and made the class + / wrapper / companion links resolve. + ## 0.1.0.0 Initial release. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -11,7 +11,7 @@ The classes each wrapper synthesises: + `Stock`: `Eq`, `Ord`, `Show`, `Read`, `Semigroup`, `Monoid`, `Enum`, `Bounded`, `Ix`, `Generic` (that's right) -+ `Stock1`: `Functor` / `Contravariant`, `Foldable`, `Applicative`, `Generic1`, `Eq1`, `Ord1`, `Show1`, `Read1`, `Traversable`† ++ `Stock1`: `Functor` / `Contravariant`, `Foldable`, `Applicative`, `Generic1`, `Eq1`, `Ord1`, `Show1`, `Read1`, `Traversable`†, `TestEquality`, `TestCoercion` + `Stock2`: `Bifunctor`, `Bifoldable`, `Eq2`, `Ord2`, `Show2`, `Read2`, `Category`, `Bitraversable`† (`unpack` / unboxed-strict fields are rejected, with a clear error) @@ -162,9 +162,19 @@ ## Conclusions / realizations -Using _inspection-testing_ shows that the code we generate is -byte-identical to stock (`==-`). `Eq`, `Ord`, `Enum`, `Functor` -optimise to the *same Core* as GHC's own `deriving` on a twin type. +Every claim here is machine-checked with _inspection-testing_ (it +compares optimised Core, not behaviour): + ++ `Eq`, `Ord`, `Enum`, `Functor`, `Bounded`, `Foldable` optimise to + Core *byte-identical* to GHC's own `deriving` on a twin type. ++ `Traversable` / `Bitraversable` — which GHC can't stock-derive at all + — produce a `traverse` / `bitraverse` byte-identical to the natural + hand-written definition. ++ every other class provably erases the `Stock` wrapper and its + coercions completely (so it is exactly as fast as hand-written). + +In short: where GHC derives the class, you get the same Core GHC emits; +where it doesn't, you get the Core you would have written by hand. `Read` (and `Read1`) build `readPrec` exactly as GHC's derived `Read` does — the same `ReadPrec` combinators — and let `readsPrec` come from diff --git a/plugin/Stock.hs b/plugin/Stock.hs --- a/plugin/Stock.hs +++ b/plugin/Stock.hs @@ -9,8 +9,8 @@ {-# OPTIONS_GHC -Wno-x-partial -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-unused-imports #-} --- | Synthesize class instances for the @Stock@ \/ @Stock1@ \/ --- @Stock2@ newtype wrappers directly from a datatype's structure, +-- | Synthesize class instances for the 'Stock' \/ 'Stock1' \/ +-- 'Stock2' newtype wrappers directly from a datatype's structure, -- same as hand-written without @Generic@. This one module both -- provides the wrappers and /is/ the plugin, so a single name does -- everything: @@ -25,12 +25,13 @@ -- -- Supported classes: -- --- * @Stock@: @Eq@, @Ord@, @Show@, @Read@, @Semigroup@, @Monoid@, @Enum@, --- @Bounded@, @Ix@, @Generic@. --- * @Stock1@: @Functor@ \/ @Contravariant@, @Foldable@, @Applicative@, --- @Generic1@, @Eq1@, @Ord1@, @Show1@, @Read1@, @Traversable@. --- * @Stock2@: @Bifunctor@, @Bifoldable@, @Eq2@, @Ord2@, @Show2@, @Read2@, --- @Category@, @Bitraversable@. +-- * 'Stock': 'Eq', 'Ord', 'Show', 'Read', 'Semigroup', 'Monoid', 'Enum', +-- 'Bounded', 'Ix', 'Generic'. +-- * 'Stock1': 'Functor' \/ 'Contravariant', 'Foldable', 'Applicative', +-- 'Generic1', 'Eq1', 'Ord1', 'Show1', 'Read1', 'Traversable', +-- 'TestEquality', 'TestCoercion'. +-- * 'Stock2': 'Bifunctor', 'Bifoldable', 'Eq2', 'Ord2', 'Show2', 'Read2', +-- 'Category', 'Bitraversable'. -- -- @Traversable@\/@Bitraversable@ are synthesized at the wrapper (@Stock1 -- F@\/@Stock2 P@) and used directly, or put on your type with the one-liner @@ -53,7 +54,7 @@ -- there is no @Rep@, no reflection, no instance lookup; you pay -- exactly the usual dictionary plumbing (including any dictionaries -- that polymorphic or polymorphically-recursive code builds at --- runtime), and never anything extra for having used @Stock@. +-- runtime), and never anything extra for having used 'Stock'. module Stock ( Stock(..), Stock1(..), Stock2(..), plugin @@ -129,6 +130,12 @@ import Control.Category (Category) import Data.Ix (Ix) import GHC.Generics (Generic, Generic1) +-- Imported only so Haddock can resolve the @'TestEquality'@ etc. identifier +-- links in this module's documentation (the plugin itself looks these classes +-- up by name via the GHC API). '-Wno-unused-imports' (above) silences them. +import Data.Bitraversable (Bitraversable) +import Data.Type.Equality (TestEquality) +import Data.Type.Coercion (TestCoercion) import Stock.Surface (lowerOverrides) import Stock.Internal import Stock.Bounded @@ -158,7 +165,7 @@ } -- | Present a raw @CtLoc -> TcPluginM (EvTerm, [Ct])@ synthesizer (@Ord@, --- @Show@, @Read@, @Enum@, @Ix@) as a @Deriver@, so every built-in @Stock@ +-- @Show@, @Read@, @Enum@, @Ix@) as a @Deriver@, so every built-in 'Stock' -- class dispatches uniformly through 'runDeriverAttempt' — exactly like the -- SDK-native ones (@Eq@, @Bounded@, @Semigroup@, …). -- Each constructor is paired with its per-field override coercions @@ -212,7 +219,7 @@ -- | Look up a 'TyCon' by module and name, returning 'Nothing' if the module -- is not in scope — so the plugin stays inert instead of erroring when our --- @Stock@ wrapper isn't imported. +-- 'Stock' wrapper isn't imported. solveStock :: PluginState -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult solveStock st _ev _given wanted = do results <- for wanted (trySolve st) @@ -256,7 +263,7 @@ addCts :: [Ct] -> Attempt -> Attempt addCts extra (sol, ws, ins) = (sol, extra ++ ws, ins) --- | Dispatch a recognised @Stock@(-@Override@) representation to the right +-- | Dispatch a recognised 'Stock'(-@Override@) representation to the right -- built-in deriver (or a discovered companion via 'tryWitness'). dispatchStock :: PluginState -> Ct -> Class -> Type -> Repr -> TcPluginM Attempt dispatchStock st ct cls wrappedTy repr diff --git a/plugin/Stock/Applicative.hs b/plugin/Stock/Applicative.hs --- a/plugin/Stock/Applicative.hs +++ b/plugin/Stock/Applicative.hs @@ -88,9 +88,10 @@ -- Override1: reshape the field functor @h a -> m a@ (e.g. ZipList), -- with a @h t ~R m t@ coercion threaded through pure/<*>/liftA2. Just m -> do ev <- newWanted loc (mkClassPred applicativeCls [m]) + vw <- newWanted loc (mkStockReprEq (mkAppTy h ctvTy) (mkAppTy m ctvTy)) -- validate reshape let coFn t = mkStockCo (PluginProv "stock") Representational (mkAppTy h t) (mkAppTy m t) - pure (Just (FsApp m (ctEvExpr ev) (Just coFn), [mkNonCanonical ev])) + pure (Just (FsApp m (ctEvExpr ev) (Just coFn), [mkNonCanonical ev, mkNonCanonical vw])) Nothing -> do ev <- newWanted loc (mkClassPred applicativeCls [h]) pure (Just (FsApp h (ctEvExpr ev) Nothing, [mkNonCanonical ev])) Just FConst -> do ev <- newWanted loc (mkClassPred monoidCls [ft]) diff --git a/plugin/Stock/Bifunctor.hs b/plugin/Stock/Bifunctor.hs --- a/plugin/Stock/Bifunctor.hs +++ b/plugin/Stock/Bifunctor.hs @@ -129,12 +129,11 @@ case geStock2 gen of Just st2Tc -- peel an optional @Override2 cfg P@: @realP@ is the genuine constructor, - -- @mMods@ the per-field positional modifiers (single inner list — one ctor). - | let (realP, mMods) = case geOverride2 gen of - Just ov2Tc - | Just (tc, [_, rp, cfg]) <- splitTyConApp_maybe p0, tc == ov2Tc - -> (rp, listToMaybe =<< decodePositional cfg) - _ -> (p0, Nothing) + -- @mMods@ the per-field modifiers (Keep-filled). Use the shared decoder + -- ('peelOverride2With' -> 'decodeOvCfg') so it accepts the field-keyed + -- forms (@Con at i via M@, @name via M@) and not only the dense + -- positional @'[ '[ .. ] ]@ list. + | let (realP, mMods) = peelOverride2With (ovTcsGen "Override2" gen) p0 , Just pTc <- tyConAppTyCon_maybe realP , [dc] <- tyConDataCons pTc, not (isNewTyCon pTc) -> do monoidCls <- tcLookupClass monoidClassName @@ -164,8 +163,15 @@ -- per field: a Category @h@ (+ coercion), or a constant @m@ handled -- Const-style via its Monoid (the automatic, @Basic@-free path). resolve i ftPQ = case mMods of - Just mods | Just m <- safeIdx mods i, not (isKeep m) -> - Just (CatF m (\t1 t2 -> mkStockCo (PluginProv "stock") Representational + Just mods | Just m0 <- safeIdx mods i, not (isKeep m0) -> + -- A modifier decoded from the field-keyed @At Con i := M@ form + -- can carry skolem /kind/ variables for phantom parameters + -- (e.g. @Basic m a b@'s @a@\/@b@), unlike the dense list form + -- which pins them to the datatype's param kind. Re-kind those + -- free variables to @k@ so @Category (m a b)@ is solvable. + let fvs = nonDetEltsUniqSet (tyCoVarsOfType m0) + m = substTyWith fvs (map (const kTy) fvs) m0 + in Just (CatF m (\t1 t2 -> mkStockCo (PluginProv "stock") Representational (instAt t1 t2 !! i) (app2 m t1 t2))) _ -> case classifyCatField pTv qTv ftPQ of Just h -> Just (CatF h (\t1 t2 -> mkRepReflCo (instAt t1 t2 !! i))) @@ -183,6 +189,19 @@ MonF m -> do ev <- newWanted loc (mkClassPred monoidCls [m]) pure (ctEvExpr ev, mkNonCanonical ev)) flds let (dEs, dWs) = unzip dws + -- validate each override reshape (@realField ~R m a b@) with a GHC + -- wanted, so the unchecked @mkStockCo@ axioms can't smuggle in an + -- unsound coercion (reject @Int via Op@, @a->b via Op@, …). + ovWs <- case mMods of + Nothing -> pure [] + Just mods -> fmap concat $ forM (zip [0 :: Int ..] realFtsPQ) \(i, ftPQ) -> + case safeIdx mods i of + Just m0 | not (isKeep m0) -> do + let fvs = nonDetEltsUniqSet (tyCoVarsOfType m0) + m = substTyWith fvs (map (const kTy) fvs) m0 + vw <- newWanted loc (mkStockReprEq ftPQ (app2 m (mkTyVarTy pTv) (mkTyVarTy qTv))) + pure [mkNonCanonical vw] + _ -> pure [] -- id = /\a. (P ..) |> sym (Stock2(..) a a ~ P a a) aTv <- freshTyVar "a" let aTy = mkTyVarTy aTv @@ -216,7 +235,7 @@ body = Case (Cast (Var gId) (coDown bTy cTy)) gCb resTy [Alt (DataAlt dc) gIds inner] compImpl = mkLams [bTv, cTv, a2Tv, gId, hId] body dict = mkApps (Var dictCon) [Type kTy, Type wrappedTy, idImpl, compImpl] - pure (Just (EvExpr dict, dWs)) + pure (Just (EvExpr dict, dWs ++ ovWs)) _ -> pure Nothing -- | Total list indexing. diff --git a/plugin/Stock/Functor.hs b/plugin/Stock/Functor.hs --- a/plugin/Stock/Functor.hs +++ b/plugin/Stock/Functor.hs @@ -113,8 +113,11 @@ let effFt = mkAppTy modf svTy -- m a coS = mkStockCo (PluginProv "stock") Representational ftA effFt coR = mkStockCo (PluginProv "stock") Representational rvFt (mkAppTy modf rvTy) + -- validate the reshape: GHC must agree @field a ~R m a@, else the + -- unchecked @coS@\/@coR@ axioms would be unsound (reject bad overrides). + vw <- newWanted loc (mkStockReprEq ftA effFt) m <- varMap functorCls mContra loc svTv rvTy covFwd conFwd Cov effFt - pure (fmap (\(e, ws) -> (Cast (App e (Cast (Var x) coS)) (mkSymCo coR), ws)) m) + pure (fmap (\(e, ws) -> (Cast (App e (Cast (Var x) coS)) (mkSymCo coR), mkNonCanonical vw : ws)) m) binders = if isCov then [svTv, rvTv] else [rvTv, svTv] malts <- forM dcons \dc -> do @@ -212,8 +215,9 @@ contrib i x ftA = case override1Mod gen mMods i of -- Override1 reshapes the field's (one-level) functor @h a -> m a@. Just m -> do ev <- newWanted loc (mkClassPred foldableCls [m]) + vw <- newWanted loc (mkStockReprEq ftA (mkAppTy m aTy)) -- validate reshape let co = mkStockCo (PluginProv "stock") Representational ftA (mkAppTy m aTy) - pure (Just (Just (foldMapOf m (ctEvExpr ev) (Cast (Var x) co), [mkNonCanonical ev]))) + pure (Just (Just (foldMapOf m (ctEvExpr ev) (Cast (Var x) co), [mkNonCanonical ev, mkNonCanonical vw]))) Nothing -> foldField ftA (Var x) malts <- forM dcons \dc -> do let ftsA = map scaledThing (dataConInstOrigArgTys dc (fixed ++ [aTy])) diff --git a/plugin/Stock/Traversable.hs b/plugin/Stock/Traversable.hs --- a/plugin/Stock/Traversable.hs +++ b/plugin/Stock/Traversable.hs @@ -122,6 +122,7 @@ fieldOf i x ftA rvFt = case override1Mod gen mMods i of Just m -> do -- Override1: traverse through @m@, re-wrap @m b -> h b@ ev <- newWanted loc (mkClassPred travCls [m]) + vw <- newWanted loc (mkStockReprEq ftA (mkAppTy m aTy)) -- validate reshape let coS = mkStockCo (PluginProv "stock") Representational ftA (mkAppTy m aTy) coRb = mkStockCo (PluginProv "stock") Representational (mkAppTy m bTy) rvFt trav = mkApps (Var traverseSel) @@ -131,7 +132,7 @@ let coerceFn = Lam mb (Cast (Var mb) coRb) -- m b -> h b pure (Just ( apE (mkAppTy m bTy) rvFt (pureE (mkVisFunTyMany (mkAppTy m bTy) rvFt) coerceFn) trav - , [mkNonCanonical ev] )) + , [mkNonCanonical ev, mkNonCanonical vw] )) Nothing -> traverseField ftA (Var x) malts <- forM dcons \dc -> do let fts = map scaledThing (dataConInstOrigArgTys dc (fixed ++ [aTy])) diff --git a/stock.cabal b/stock.cabal --- a/stock.cabal +++ b/stock.cabal @@ -1,97 +1,88 @@ cabal-version: 3.0 name: stock -version: 0.1.0.0 +version: 0.1.0.1 synopsis: Stock-style deriving via coercion, with no Generic description: - A GHC type-checker plugin that derives class instances for @Stock T@ - and higher-kinded variants at /compile time/, straight from the - structure of /T/ without a @Generic@ representation or runtime cost. - . + A GHC type-checker plugin that derives class instances for + __@@__ and higher-kinded variants at /compile time/, straight + from the structure of /T/ without a @Generic@ representation or + runtime cost. Synthesized instances emulate GHC's /stock/ deriving. + Supported classes: - . - * @Stock@: Eq, Ord, Show, Read, Semigroup, Monoid, Enum, Bounded, Ix, Generic - * @Stock1@: Functor, Foldable, Traversable, Contravariant, Applicative, Eq1, Ord1, Show1, Read1, Generic1, TestEquality, TestCoercion - * @Stock2@: Bifunctor, Bifoldable, Bitraversable, Eq2, Ord2, Show2, Read2, Category - . - Every claim below is machine-checked with @inspection-testing@ (it - compares optimised Core, not behaviour): - . - * For @Eq@, @Ord@, @Enum@, @Functor@, @Bounded@ and @Foldable@ the - emitted Core is /byte-identical/ to GHC's own stock deriving. - * @Traversable@ and @Bitraversable@ — which GHC cannot stock-derive - at all — produce a @traverse@\/@bitraverse@ /byte-identical/ to the - natural hand-written definition. - * Every remaining class is proven to erase the @Stock@ wrapper and - its coercions /completely/, so the instance is exactly as fast as a - hand-written one and behaves identically to stock deriving wherever - GHC has it. - . - In short: where GHC derives the class, the result is the same Core - GHC emits; where it does not, the result is the Core you would have - written by hand. - . - @Traversable@\/@Bitraversable@ are synthesised as genuine instances - but cannot be reached by a bare @deriving via@ (the coercion is - blocked by the abstract applicative's nominal role; see @"Stock"@). - . + + * __@@__: @@, @@, @@, @@, @@, @@, + @@, @@, @@, @@ + * __@@__: @@, @@, @@,† @@, + @@, @@, @@, @@, @@, @@, + @@, @@ + * __@@__: @@, @@, @@,† @@, + @@, @@, @@, @@ + + † @@, + @@ + are synthesisable but cannot be used with @DerivingVia@ due to role + issues. + Companion packages add more classes through @DeriveStock@ instances - (see @"Stock.Derive"@), discovered automatically without an extra - @-fplugin@ flag : - . - * @stock-deepseq@: NFData, NFData1, NFData2 - * @stock-hashable@: Hashable, Hashable1, Hashable2 - * @stock-aeson@: ToJSON, ToJSON1, ToJSON2; FromJSON, FromJSON1, FromJSON2 - * @stock-quickcheck@: Arbitrary, Arbitrary1, Arbitrary2; CoArbitrary - * @stock-profunctors@: Profunctor - . - Ordinary @DerivingVia@ modifiers compose with @Stock@: - @Down (Stock T)@ reverses ordering, enumeration and bounds; - @Backwards (Stock1 F)@ reverses @Applicative@ effects; @Reverse - (Stock1 F)@ reverses @Foldable@\/@Traversable@. - . + (see "Stock.Derive"), discovered automatically without an extra + @-fplugin@ flag: + + * __@@__: @@, @@, @@ + * __@@__: @@, @@, @@ + * __@@__: @@, @@, @@; @@, @@, @@ + * __@@__: @@, @@, @@; @@ + * __@@__: @@ + + Ordinary @DerivingVia@ modifiers compose with + : + + * @@ reverses ordering, enumeration and bounds + * @@ reverses @@ effects + * @@ reverses @@ \/ @@ + > {-# options_ghc -fplugin Stock #-} > {-# language DerivingVia #-} - > + > > import Stock > import Data.Ord (Down(..)) > - > -- >>> sort [Bronze, Silver, Gold] + > -- >>> sort [Bronze,Silver,Gold] > -- [Gold,Silver,Bronze] > data Place = Bronze | Silver | Gold - > deriving (Eq, Show) via Stock Place + > deriving (Eq, Show) via Stock Place > deriving (Ord, Bounded, Enum) via Down (Stock Place) - . - Per-field modifiers (@Override@, @"Stock.Override"@, re-exported by - @"Stock"@) customise individual fields by name, type, or position; @_@ + + Per-field modifiers (@Override@, "Stock.Override", re-exported by + "Stock") customise individual fields by name, type, or position; @_@ leaves a field unchanged. A modifier is any newtype with the relevant instance. - . - Hit points and coins accumulate with addition, poisoning - contaminates by disjunction (or), @items@, and @weapons@ union with - addition to product a multiset. - . + + This game example shows hit points and coins accumulate with + addition, poisoning contaminates by disjunction (or), @items@, and + @weapons@ union with addition to produce a multiset. + > import Data.Map.Monoidal (MonoidalMap(..)) - > .. + > > type MultiSet key = MonoidalMap key (Sum Int) - > + > > data Inventory = Inventory - > { hp :: Int - > , coins :: Int - > , poisoned :: Bool - > , items :: Map Item Int -- these unfortunately default - > , weapons :: Map Weapon Int -- to left-biased union + > { hp :: Int -- (+) + > , coins :: Int -- (+) + > , poisoned :: Bool -- (||) + > , items :: Map Item Int -- unionWith (+) + > , weapons :: Map Weapon Int -- unionWith (+) > } - > deriving (Eq, Ord, Show, Read) via + > deriving (Eq, Ord, Show, Read) via > Stock Inventory - > deriving (Semigroup, Monoid) via + > deriving (Semigroup, Monoid) via > Overriding Inventory - > '[ hp via Sum - > , coins via Sum - > , poisoned via Any - > , items via MultiSet Item - > , weapons via MultiSet Weapon - > ] - . + > '[ hp via Sum + > , coins via Sum + > , poisoned via Any + > , items via MultiSet Item + > , weapons via MultiSet Weapon + > ] + Synthesis runs once per instance (not per use): @deriving Cls via Stock T@ produces a single shared @instance Cls T@ that every call reuses. license: BSD-3-Clause