diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,25 @@ # Changelog +## 0.1.0.2 + +* Fix `Applicative` via `Overriding1`: a per-field modifier now reshapes *any* + field (e.g. a nested `[[a]]` via `Compose [] []`), matching + `Functor`/`Foldable`/`Traversable`. Previously the modifier was consulted only + for fields already of shape `h a`, so nested fields were wrongly rejected as + "supports only covariant fields". +* New `overrides` test-suite: derive each class through a modifier newtype + (`Sum`/`Product`/`Any`/`All`/`Min`/`Max`/`Down`/`Compose`/`ZipList`/`Op`/ + `Basic`/`Kleisli`/…) with runtime assertions that the reshape took effect. +* Fix ill-scoped Core from a per-field reshape over an *abstract* functor (e.g. + a nested `Compose f (Compose g …)` with `Representational1` constraints). The + reshape-validation constraint carried the method's own type variable and was + emitted at instance scope, so its (dictionary-shaped) evidence referenced a + variable that was out of scope — `-dcore-lint` rejected it though it ran at + `-O0`. The validation now runs at a closed type, keeping the evidence + well-scoped while still rejecting unsound overrides. Applies to `Functor`, + `Foldable`, `Traversable`, `Applicative`, `Bifunctor`/`Bifoldable` and + `Category`. + ## 0.1.0.1 * `Category` via `Overriding2`: accept the field-keyed override forms diff --git a/negative/RunNegative.hs b/negative/RunNegative.hs new file mode 100644 --- /dev/null +++ b/negative/RunNegative.hs @@ -0,0 +1,10 @@ +-- | Runs the should-fail harness ('negative/run-negative.sh') as a cabal test: +-- compiles invalid per-field overrides and asserts they are rejected (and that +-- valid controls still compile). Exits with the script's status. +module Main (main) where + +import System.Process (rawSystem) +import System.Exit (exitWith) + +main :: IO () +main = rawSystem "bash" ["negative/run-negative.sh"] >>= exitWith diff --git a/negative/run-negative.sh b/negative/run-negative.sh new file mode 100644 --- /dev/null +++ b/negative/run-negative.sh @@ -0,0 +1,63 @@ +#!/usr/bin/env bash +# Should-fail harness for per-field Override validation. +# +# A reshape `field via M` is only sound when `field` is coercible to the +# modifier `M` applied to the parameters. The plugin emits a GHC-checked +# `Coercible` wanted for every reshape, so an INVALID override must be a +# compile error. This can't be expressed in a normal module (the module +# wouldn't compile), so we compile each snippet with the plugin and assert the +# expected outcome. Negative cases MUST fail; positive controls MUST compile +# (so a regression that makes the plugin reject *everything* is also caught). +# +# Run from anywhere: bash negative/run-negative.sh +set -u +[ -d "$HOME/.ghcup/bin" ] && export PATH="$HOME/.ghcup/bin:$PATH" +cd "$(dirname "$0")/.." # project root +cabal build stock >/dev/null 2>&1 || { echo "stock failed to build"; exit 2; } + +TMP="$(mktemp -d)"; trap 'rm -rf "$TMP"' EXIT +PRE='{-# OPTIONS_GHC -fplugin Stock #-} +{-# LANGUAGE DerivingVia, DataKinds, TypeOperators #-} +module N where +import Stock +import Control.Category +import Control.Arrow (Kleisli(..)) +import Control.Applicative (ZipList(..)) +import Data.Bifunctor +import Prelude hiding (id, (.)) +newtype Op cat a b = Op (cat b a) +instance Category cat => Category (Op cat) where { id = Op id; Op f . Op g = Op (g . f) } +newtype Basic m a b = Basic m +instance Monoid m => Category (Basic m) where { id = Basic mempty; Basic a . Basic b = Basic (a <> b) }' + +fails=0 +# check NAME EXPECT BODY where EXPECT = reject | accept +check () { + local name="$1" expect="$2" body="$3" + printf '%s\n%s\n' "$PRE" "$body" > "$TMP/N.hs" + if cabal exec -- ghc -O0 -fno-code -package stock -fforce-recomp "$TMP/N.hs" >/dev/null 2>&1 + then got=accept; else got=reject; fi + if [ "$got" = "$expect" ]; then + printf 'ok %-46s (%s)\n' "$name" "$expect" + else + printf 'FAIL %-46s expected %s, got %s\n' "$name" "$expect" "$got"; fails=$((fails+1)) + fi +} + +echo "== negative: invalid reshapes MUST be rejected ==" +check "Functor Maybe via []" reject "data A a = A (Maybe a) deriving Functor via Overriding1 A '[ '[ [] ] ]" +check "Foldable Maybe via []" reject "data B a = B (Maybe a) deriving Foldable via Overriding1 B '[ '[ [] ] ]" +check "Applicative Maybe via []" reject "data C a = C (Maybe a) deriving (Functor,Applicative) via Overriding1 C '[ '[ [] ] ]" +check "Eq Int via Bool" reject "data E = E Int deriving (Eq,Show) via Stock (Override E '[ Int via Bool ])" +check "Category Int via Op (->)" reject "data T1 a b = T1 { z :: Int } deriving Category via Overriding2 T1 '[ T1 at 0 via Op (->) ]" +check "Category a->b via Op (->)" reject "data T2 a b = T2 { f :: a -> b } deriving Category via Overriding2 T2 '[ T2 at 0 via Op (->) ]" + +echo "== positive controls: valid reshapes MUST compile ==" +check "Functor ZipList override" accept "data P a = P [a] deriving Functor via Overriding1 P '[ '[ZipList] ]" +check "Category sparse At (Basic/Kleisli)" accept "data T3 a b = T3 { zero :: String, one :: a -> b, two :: a -> [b] } + deriving Category via Overriding2 T3 '[ T3 at 0 via Basic String, T3 at 2 via Kleisli [] ]" +check "Category b->a via Op (->)" accept "data T4 a b = T4 { g :: b -> a } deriving Category via Overriding2 T4 '[ T4 at 0 via Op (->) ]" + +echo +if [ "$fails" -eq 0 ]; then echo "negative harness: all expectations met"; else echo "negative harness: $fails FAILURE(S)"; fi +exit "$fails" diff --git a/plugin/Stock/Applicative.hs b/plugin/Stock/Applicative.hs --- a/plugin/Stock/Applicative.hs +++ b/plugin/Stock/Applicative.hs @@ -82,21 +82,28 @@ -- @FsParam@ | @FsApp h dApplicative@ | @FsConst ft dMonoid@; an arrow or -- other unsupported shape still bails with 'Nothing'. - specsW <- forM (zip3 [0 :: Int ..] kinds fldTys) \(i, k, ft) -> case k of - Just FParam -> pure (Just (FsParam, [])) - Just (FApp h) -> case override1Mod gen mMods i of - -- Override1: reshape the field functor @h a -> m a@ (e.g. ZipList), - -- with a @h t ~R m t@ coercion threaded through pure/<*>/liftA2. + specsW <- forM (zip3 [0 :: Int ..] kinds fldTys) \(i, k, ft) -> + -- Consult the @Override1@ modifier FIRST, regardless of the field's + -- raw shape: that lets a modifier reshape an otherwise-unsupported + -- field (e.g. a nested @[[a]]@ via @Compose [] []@) into a one-level + -- applicative @m a@ — exactly as Functor\/Foldable\/Traversable do. + -- The @field t ~R m t@ coercion is threaded through pure\/\<*\>. + case override1Mod gen mMods i of Just m -> do ev <- newWanted loc (mkClassPred applicativeCls [m]) - vw <- newWanted loc (mkStockReprEq (mkAppTy h ctvTy) (mkAppTy m ctvTy)) -- validate reshape + -- validate at the closed type @()@ (see Stock.Functor) + -- so the evidence stays free of the method-local @ctv@. + vw <- newWanted loc (mkStockReprEq (substTyWith [ctv] [unitTy] ft) + (mkAppTy m unitTy)) let coFn t = mkStockCo (PluginProv "stock") Representational - (mkAppTy h t) (mkAppTy m t) + (substTyWith [ctv] [t] ft) (mkAppTy m t) 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]) - pure (Just (FsConst ft (ctEvExpr ev), [mkNonCanonical ev])) - _ -> pure Nothing + Nothing -> case k of + Just FParam -> pure (Just (FsParam, [])) + Just (FApp h) -> 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]) + pure (Just (FsConst ft (ctEvExpr ev), [mkNonCanonical ev])) + _ -> pure Nothing case sequence specsW of Nothing -> pure Nothing diff --git a/plugin/Stock/Bifunctor.hs b/plugin/Stock/Bifunctor.hs --- a/plugin/Stock/Bifunctor.hs +++ b/plugin/Stock/Bifunctor.hs @@ -199,7 +199,14 @@ 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))) + -- validate at closed types (see Stock.Functor) so the + -- evidence stays free of @pTv@\/@qTv@. The two params get + -- DISTINCT closed types (@()@ and @Bool@): collapsing both to + -- the same type would hide an order-swap (@a->b@ vs @b->a@ via + -- @Op@ both become @()->()@), wrongly accepting it. + vw <- newWanted loc (mkStockReprEq + (substTyWith [pTv, qTv] [unitTy, boolTy] ftPQ) + (app2 m unitTy boolTy)) pure [mkNonCanonical vw] _ -> pure [] -- id = /\a. (P ..) |> sym (Stock2(..) a a ~ P a a) diff --git a/plugin/Stock/Functor.hs b/plugin/Stock/Functor.hs --- a/plugin/Stock/Functor.hs +++ b/plugin/Stock/Functor.hs @@ -115,7 +115,15 @@ 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) + -- We check it at the CLOSED type @()@ rather than the method binder + -- @svTv@: the reshape is parametric in the element, so this still + -- rejects bad overrides, while keeping the (possibly dictionary-shaped, + -- e.g. via @Representational1@) evidence free of the method-local + -- @svTv@ — otherwise GHC binds that evidence at instance level, where + -- @svTv@ is out of scope, and emits ill-scoped Core (a nested-abstract + -- @Compose@ reshape did exactly this). + vw <- newWanted loc (mkStockReprEq (substTyWith [svTv] [unitTy] ftA) + (mkAppTy modf unitTy)) m <- varMap functorCls mContra loc svTv rvTy covFwd conFwd Cov effFt 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] @@ -215,7 +223,10 @@ 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 + -- validate at the closed type @()@ (see synthMap1) so the + -- evidence stays free of the method-local @atv@. + vw <- newWanted loc (mkStockReprEq (substTyWith [atv] [unitTy] ftA) + (mkAppTy m unitTy)) let co = mkStockCo (PluginProv "stock") Representational ftA (mkAppTy m aTy) pure (Just (Just (foldMapOf m (ctEvExpr ev) (Cast (Var x) co), [mkNonCanonical ev, mkNonCanonical vw]))) Nothing -> foldField ftA (Var x) diff --git a/plugin/Stock/Traversable.hs b/plugin/Stock/Traversable.hs --- a/plugin/Stock/Traversable.hs +++ b/plugin/Stock/Traversable.hs @@ -122,7 +122,10 @@ 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 + -- validate at the closed type @()@ (see Stock.Functor) so the + -- evidence stays free of the method-local @aTv@. + vw <- newWanted loc (mkStockReprEq (substTyWith [aTv] [unitTy] ftA) + (mkAppTy m unitTy)) let coS = mkStockCo (PluginProv "stock") Representational ftA (mkAppTy m aTy) coRb = mkStockCo (PluginProv "stock") Representational (mkAppTy m bTy) rvFt trav = mkApps (Var traverseSel) diff --git a/stock.cabal b/stock.cabal --- a/stock.cabal +++ b/stock.cabal @@ -1,21 +1,21 @@ cabal-version: 3.0 name: stock -version: 0.1.0.1 +version: 0.1.0.2 synopsis: Stock-style deriving via coercion, with no Generic description: A GHC type-checker plugin that derives class instances for - __@@__ and higher-kinded variants at /compile time/, straight + __@@__ 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: - * __@@__: @@, @@, @@, @@, @@, @@, + * __@@__: @@, @@, @@, @@, @@, @@, @@, @@, @@, @@ - * __@@__: @@, @@, @@,† @@, + * __@@__: @@, @@, @@,† @@, @@, @@, @@, @@, @@, @@, @@, @@ - * __@@__: @@, @@, @@,† @@, + * __@@__: @@, @@, @@,† @@, @@, @@, @@, @@ † @@, @@ -34,7 +34,7 @@ * __@@__: @@ Ordinary @DerivingVia@ modifiers compose with - : + : * @@ reverses ordering, enumeration and bounds * @@ reverses @@ effects @@ -100,6 +100,7 @@ extra-doc-files: README.md CHANGELOG.md extra-source-files: LICENSE + negative/run-negative.sh common warnings ghc-options: -Wall -Wcompat -Wincomplete-record-updates @@ -154,6 +155,27 @@ stock ghc-options: -fplugin=Stock hs-source-dirs: test + +-- Override-via-newtype coverage: derive each class through a modifier newtype +-- (Sum / Down / Compose / Op / Basic / …) and assert the reshape took effect. +test-suite overrides + import: warnings + type: exitcode-stdio-1.0 + main-is: Overrides.hs + build-depends: base >=4.18 && <5, stock + ghc-options: -fplugin=Stock + hs-source-dirs: test + +-- Should-fail harness: compiles invalid per-field overrides and asserts the +-- plugin rejects them (with valid controls that must still compile). Runs +-- negative/run-negative.sh (compile-must-fail can't live in a normal module). +test-suite negative + import: warnings + type: exitcode-stdio-1.0 + main-is: RunNegative.hs + build-depends: base >=4.18 && <5, + process + hs-source-dirs: negative benchmark bench import: warnings diff --git a/test/Overrides.hs b/test/Overrides.hs new file mode 100644 --- /dev/null +++ b/test/Overrides.hs @@ -0,0 +1,140 @@ +{-# OPTIONS_GHC -fplugin Stock -Wno-unused-imports #-} +{-# LANGUAGE DerivingVia, DataKinds, TypeOperators, KindSignatures #-} +{-# LANGUAGE FlexibleContexts, UndecidableInstances #-} +{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving #-} + +-- | Override-via-newtype coverage: derive each class through a /modifier +-- newtype/ (Sum, Product, Any, All, Min, Max, Down, Compose, ZipList, Op, +-- Basic, Kleisli, a Bounded-flip, …) and check at runtime that the reshape +-- actually took effect. These exercise the @Override@\/@Overriding@ reshape +-- paths — historically the most bug-prone part of the plugin. +module Main (main) where + +import Data.Kind (Type) +import Stock +import Control.Category (Category, id, (.)) +import Control.Arrow (Kleisli(..)) +import Control.Applicative (ZipList(..)) +import Control.Monad (unless) +import System.Exit (exitFailure) +import Data.Functor.Compose (Compose(..)) +import Data.Functor.Identity (Identity(..)) +import Data.Coerce (Coercible) +import Data.Monoid (Sum(..), Product(..), Any(..), All(..)) +import Data.Semigroup (Min(..), Max(..)) +import Data.Ord (Down(..)) +import Prelude hiding (id, (.)) + +-- custom modifier newtypes +newtype Op cat a b = Op (cat b a) +instance Category cat => Category (Op cat) where { id = Op id; Op f . Op g = Op (g . f) } +newtype Basic m a b = Basic m +instance Monoid m => Category (Basic m) where { id = Basic mempty; Basic a . Basic b = Basic (a <> b) } +newtype Hi a = Hi a -- flips a field's bounds +instance Bounded a => Bounded (Hi a) where { minBound = Hi maxBound; maxBound = Hi minBound } + +-- ── Semigroup / Monoid through assorted monoid newtypes ── +data Acc = Acc Int Int Bool deriving (Eq, Show) via Stock Acc + deriving (Semigroup, Monoid) via Overriding Acc '[ '[ Sum Int, Product Int, Any ] ] + +data Mm = Mm Int Int deriving (Eq, Show) via Stock Mm + deriving Semigroup via Overriding Mm '[ '[ Min, Max ] ] + +data Flags = Flags Bool Bool deriving (Eq, Show) via Stock Flags + deriving (Semigroup, Monoid) via Overriding Flags '[ '[ All, Any ] ] + +-- ── Ord: reverse one field with Down ── +data OrdD = OrdD Int Int deriving (Eq, Show) via Stock OrdD + deriving Ord via Stock (Override OrdD '[ '[ Down, _ ] ]) + +-- ── Bounded: flip one field's bounds with Hi ── +data Bd = Bd Bool Ordering deriving (Eq, Show) via Stock Bd + deriving Bounded via Stock (Override Bd '[ '[ Hi, _ ] ]) + +-- ── Functor / Foldable / Applicative: reshape a nested [[a]] via Compose ── +data Nest a = Nest [[a]] a deriving Show via Stock (Nest a) + deriving (Functor, Foldable, Applicative) via + Overriding1 Nest '[ '[ (Compose [] [] :: Type -> Type), Keep ] ] + +-- ── Applicative: zip semantics via ZipList ── +data Zp a = Zp [a] [a] deriving (Eq, Show) via Stock (Zp a) + deriving (Functor, Applicative) via Overriding1 Zp '[ '[ ZipList, ZipList ] ] + +-- ── Category: per-field modifiers (sparse At form): Basic + Op ── +data Trans a b = Trans { fwd :: a -> b, lbl :: String, bwd :: b -> a } + deriving Category via Overriding2 Trans + '[ Trans at 1 via Basic String, Trans at 2 via Op (->) ] + +-- ── Category: monadic arrows via Kleisli ── +data Km a b = Km (a -> Maybe b) + deriving Category via Overriding2 Km '[ '[ Kleisli Maybe ] ] + +runKm :: Km a b -> a -> Maybe b +runKm (Km f) = f + +-- ── "iterate through play": algebraic-identity substitutions on a field ── +-- Compose Identity = id : reshaping a Maybe a field via Compose Identity Maybe +-- must behave exactly like leaving it alone. Compose [] Maybe wraps it in a list. +data Wp a = Wp (Maybe a) a deriving (Eq, Show) via Stock (Wp a) + deriving Functor via Stock1 Wp +data WpI a = WpI (Maybe a) a deriving (Eq, Show) via Stock (WpI a) + deriving Functor via Overriding1 WpI '[ '[ Compose Identity Maybe, Keep ] ] +data WpL a = WpL [Maybe a] a deriving (Eq, Show) via Stock (WpL a) + deriving Functor via Overriding1 WpL '[ '[ Compose [] Maybe, Keep ] ] + +-- depth-3 nested Compose still reaches the bottom +data N3 a = N3 [[[a]]] a deriving (Eq, Show) via Stock (N3 a) + deriving Functor via Overriding1 N3 '[ '[ Compose (Compose [] []) [], Keep ] ] + +-- single-level polymorphic modifier (abstract f, g): derivation produces a context +data Dfg (f :: Type -> Type) (g :: Type -> Type) a = Dfg (f (g a)) a +deriving via Overriding1 (Dfg f g) '[ '[ Compose f g, Keep ] ] + instance (Functor f, Functor g) => Functor (Dfg f g) + +-- nested-abstract Compose: derives once each functor carries Representational1 f +-- = (forall x y. Coercible x y => Coercible (f x) (f y)), which lets GHC coerce +-- under the abstract functor. (The reshape validation is checked at the closed +-- type (), so its evidence stays well-scoped — see Stock.Functor.) +data Rt (f :: Type -> Type) (g :: Type -> Type) a = Rt (f (g (f (g a)))) a +deriving via Overriding1 (Rt f g) '[ '[ Compose f (Compose g (Compose f g)), Keep ] ] + instance ( Functor f, Functor g + , (forall x y. Coercible x y => Coercible (f x) (f y)) + , (forall x y. Coercible x y => Coercible (g x) (g y)) ) + => Functor (Rt f g) +deriving via Overriding1 (Rt f g) '[ '[ Compose f (Compose g (Compose f g)), Keep ] ] + instance ( Foldable f, Foldable g + , (forall x y. Coercible x y => Coercible (f x) (f y)) + , (forall x y. Coercible x y => Coercible (g x) (g y)) ) + => Foldable (Rt f g) + +main :: IO () +main = do + let ck s b = if b then putStrLn ("ok " ++ s) + else putStrLn ("FAIL " ++ s) >> exitFailure + ck "Semigroup Sum/Product/Any" (Acc 1 2 False <> Acc 10 3 True == Acc 11 6 True) + ck "Monoid mempty" (mempty == Acc 0 1 False) + ck "Semigroup Min/Max" (Mm 3 5 <> Mm 1 9 == Mm 1 9) + ck "Monoid All/Any" (mempty == Flags True False) + ck "Semigroup All/Any" (Flags True True <> Flags True False == Flags True True) + ck "Ord Down field0" (compare (OrdD 1 0) (OrdD 2 0) == GT) + ck "Bounded Hi flips field0" (minBound == Bd True LT && maxBound == Bd False GT) + ck "Functor over [[a]]" (case fmap (+1) (Nest [[1],[2,3]] 9) of Nest xs y -> xs == [[2],[3,4]] && y == 10) + ck "Foldable over [[a]]" (sum (Nest [[1,2],[3]] 4) == 10) + ck "Applicative pure (Compose)" (case (pure 5 :: Nest Int) of Nest xs y -> xs == [[5]] && y == 5) + ck "Applicative ZipList <*>" (((,) <$> Zp [1,2] [10] <*> Zp [3,4] [20]) == Zp [(1,3),(2,4)] [(10,20)]) + let t1 = Trans (+1) "a" (subtract 1) :: Trans Int Int + t2 = Trans (*2) "b" (`div` 2) :: Trans Int Int + t3 = t1 . t2 + ck "Category fwd composes" (fwd t3 3 == 7) + ck "Category Basic String <>" (lbl t3 == "ab") + let k1 = Km (\x -> if x > 0 then Just (x*2) else Nothing) :: Km Int Int + k2 = Km (\x -> Just (x+1)) :: Km Int Int + ck "Category Kleisli compose" (runKm (k1 . k2) 3 == Just 8 && runKm (k1 . k2) (-5) == Nothing) + -- Compose Identity = id : the override must be invariant w.r.t. plain Stock1 + ck "Compose Identity ≅ plain" (case (fmap (+1) (Wp (Just 1) 9), fmap (+1) (WpI (Just 1) 9)) of + (Wp a x, WpI b y) -> (a, x) == (b, y) && (a, x) == (Just 2, 10)) + ck "Compose [] T wraps field" (case fmap (+1) (WpL [Just 1, Nothing] 9) of WpL a x -> a == [Just 2, Nothing] && x == 10) + ck "depth-3 Compose reaches bot" (case fmap (+1) (N3 [[[1, 2]]] 9) of N3 a x -> a == [[[2, 3]]] && x == 10) + ck "polymorphic Compose f g" (case fmap (+1) (Dfg (Just [1, 2]) 9 :: Dfg Maybe [] Int) of Dfg a x -> a == Just [2, 3] && x == 10) + ck "nested-abstract via Repr1" (case fmap (+1) (Rt (Just [Just [1]]) 9 :: Rt Maybe [] Int) of Rt a x -> a == Just [Just [2]] && x == 10) + ck "nested-abstract Foldable" (sum (Rt (Just [Just [1], Just [2, 3]]) 100 :: Rt Maybe [] Int) == 106)