polytropos-plugin 0.1.0.2 → 0.1.0.3
raw patch · 4 files changed
+524/−14 lines, 4 filesdep −filepath
Dependencies removed: filepath
Files
- CHANGELOG.md +6/−0
- polytropos-plugin.cabal +1/−2
- src/Polytropos/Plugin.hs +311/−12
- tests/smoke/Main.hs +206/−0
CHANGELOG.md view
@@ -1,5 +1,11 @@ # Changelog for polytropos-plugin +## 0.1.0.3 — 2026-11-03++- Add `KnownRowMorph` constraint solver emitting literal `RowMorph` index arrays for static channel permutations.+- Add `FrameWire` constraint solver synthesizing automatic gather and scatter plans for frame-rule register wiring.+- Generalize `ConstructorIndex` solver to poly-kinded constructors (`k -> Type` and `Type -> Type`).+ ## 0.1.0.0 — Initial Release - GHC typechecker plugin synthesizing literal dictionaries and $O(1)$ jump tables directly into Core AST
polytropos-plugin.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: polytropos-plugin-version: 0.1.0.2+version: 0.1.0.3 synopsis: TcPlugin that emits literal evidence for Polytropos row classes description: A GHC typechecker plugin for <https://hackage.haskell.org/package/polytropos polytropos>@@ -68,7 +68,6 @@ , tasty-hunit >= 0.10 && < 0.11 , polytropos-plugin , process- , filepath , directory ghc-options:
src/Polytropos/Plugin.hs view
@@ -189,6 +189,10 @@ , classTyCon ) +import GHC.Core.TyCon+ ( tyConDataCons+ )+ import GHC.Core.Multiplicity ( scaledThing , scaledMult@@ -305,6 +309,7 @@ * Note [Solving Pipeline: Wanteds, Givens, and Staged Evidence Synthesis] [ref:note-solving-pipeline] * Note [SubRow and SubSum Interior Mechanics: Matchers and Witness Generation] [ref:note-subrow-subsum-mechanics] * Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+ * Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring] External Canonical Design References: * docs/notes/POLYTROPOS_DESIGN.md (decisions D1–D10, open questions)@@ -373,8 +378,10 @@ data Rep = Rep {-# UNPACK #-} !Word {-# UNPACK #-} !(SmallArray Any) `Polytropos.Plugin` is a GHC typechecker plugin that intercepts evidence constraints:- - `FieldIndex label row a`: Computes the 0-based integer slot offset `i`.- - `ConstructorIndex con row`: Computes the 0-based constructor tag `t` (Word).+ - `FieldIndex label row a`: Computes the 0-based integer slot offset `i` across+ standard, HKD, and multi-sorted effect rows (see Note [Poly-Kinded Row Indexing for Multi-Sorted Effects] [ref:note-poly-kinded-indexing]).+ - `ConstructorIndex con row`: Computes the 0-based constructor tag `t` (Word) across+ variant and effect rows. - `RowEq` / `RowShow` / `RowEqSum` / `RowShowSum`: Directly synthesizes unrolled Core expressions comparing or showing each slot in sequence, using literal `Int` and `Word` constants (see `mkIntExpr` and `mkWordExpr`).@@ -665,6 +672,10 @@ , psTypeErrorTyCon :: !TyCon -- ^ GHC.Internal.TypeError.TypeError , psPromotedText :: !TyCon -- ^ promoted 'Text , psPromotedVcat :: !TyCon -- ^ promoted ':$$:+ , psUnsafeMkRowMorph :: !Var -- ^ Polytropos.RowMorph.unsafeMkRowMorph+ , psUnsafeMkFrame :: !Var -- ^ Polytropos.RowMorph.unsafeMkFramePlan+ , psPairTyCon :: !TyCon -- ^ Polytropos.Core.Pair+ , psPromotedPair :: !TyCon -- ^ promoted '(:=) } -------------------------------------------------------------------------------@@ -725,6 +736,16 @@ let psPromotedText = promoteDataCon textDataCon psPromotedVcat = promoteDataCon vcatDataCon + pairOcc <- lookupOrig coreMod (mkTcOcc "Pair")+ psPairTyCon <- tcLookupTyCon pairOcc+ let psPromotedPair = case tyConDataCons psPairTyCon of+ (dc : _) -> promoteDataCon dc+ [] -> error "Polytropos.Plugin: Pair tycon has no data constructors"++ rowMorphMod <- findModule "Polytropos.RowMorph" (Just "polytropos-core")+ psUnsafeMkRowMorph <- lookupIdInModule rowMorphMod "unsafeMkRowMorph"+ psUnsafeMkFrame <- lookupIdInModule rowMorphMod "unsafeMkFramePlan"+ pure PluginState{..} findModule :: String -> Maybe String -> TcPluginM 'Init Module@@ -887,7 +908,11 @@ -- Unrolls GHC Core Types to human-readable strings via 'ppr' and 'showSDocUnsafe'. formatRecordRow :: [(Int, FastString, Type)] -> String formatRecordRow fields =- "{ " ++ intercalate ", " [ unpackFS n ++ " :: " ++ showSDocUnsafe (ppr ty) | (_, n, ty) <- fields ] ++ " }"+ "{ " ++ intercalate ", " (map formatField fields) ++ " }"+ where+ formatField (_, n, ty)+ | nullFS n = showSDocUnsafe (ppr ty)+ | otherwise = unpackFS n ++ " :: " ++ showSDocUnsafe (ppr ty) -- | Formats a sum row's schema for display in compiler diagnostics: -- "< Con1 RecordPayload | Con2 TypePayload | Con3 >"@@ -898,11 +923,13 @@ formatVariantRow ctors = "< " ++ intercalate " | " (map formatCtor ctors) ++ " >" where- formatCtor (_, n, conRowTy) =- case walkRowWithTypes conRowTy of- [] -> unpackFS n- [(_, fn, ty)] | nullFS fn -> unpackFS n ++ " :: " ++ showSDocUnsafe (ppr ty)- fs -> unpackFS n ++ " " ++ formatRecordRow fs+ formatCtor (_, n, conRowTy)+ | nullFS n = showSDocUnsafe (ppr conRowTy)+ | otherwise =+ case walkRowWithTypes conRowTy of+ [] -> unpackFS n+ [(_, fn, ty)] | nullFS fn -> unpackFS n ++ " :: " ++ showSDocUnsafe (ppr ty)+ fs -> unpackFS n ++ " " ++ formatRecordRow fs -- | Formats a field suggestion clause: -- - If close matches exist: "Did you mean: 'name' or 'age'?"@@ -1057,6 +1084,12 @@ -> solveSubSum state ct cls tys | nameOccName name == mkTcOcc "KnownHash" -> noNew <$> solveKnownHash ct cls tys+ | nameOccName name == mkTcOcc "KnownRowMorph"+ -> solveKnownRowMorph state ct cls tys+ | nameOccName name == mkTcOcc "FrameWire"+ -> solveFrameWire state ct cls tys+ | nameOccName name == mkTcOcc "IsLabel"+ -> pure $ Right () | otherwise -> pure $ Right () _ -> pure $ Right ()@@ -1074,6 +1107,7 @@ -- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence] -- See Note [Human-Centric TypeError Diagnostics & Fuzzy Matching] [ref:note-typeerror-diagnostics] -- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+-- See Note [Poly-Kinded Row Indexing for Multi-Sorted Effects] [ref:note-poly-kinded-indexing] -- -- Execution Phases: -- 1. Deconstruct Predicate Types:@@ -1154,11 +1188,33 @@ Nothing -> pure $ Right () -- Row tail is still open/unfixed: defer solving Nothing -> do -- Anonymous/positional field lookup by payload Type+ -- See Note [Poly-Kinded Row Indexing for Multi-Sorted Effects] [ref:note-poly-kinded-indexing] case findFieldIndexByType unwrapN rowTy of- Just i -> do- let iExpr = mkIntExpr i- dictExpr = evDataConApp (classDataCon cls) tys [iExpr]- pure $ Left ((EvExpr dictExpr, ct), [])+ Just i+ -- Accept exact type match+ | unwrapN `eqType` expectedATy -> do+ let iExpr = mkIntExpr i+ dictExpr = evDataConApp (classDataCon cls) tys [iExpr]+ pure $ Left ((EvExpr dictExpr, ct), [])+ -- If either type is open / uninstantiated, emit nominal equality constraint to unify them+ | not (isClosedType expectedATy) || not (isClosedType unwrapN) -> do+ let iExpr = mkIntExpr i+ dictExpr = evDataConApp (classDataCon cls) tys [iExpr]+ eqEv <- newWanted loc (mkEqPredRole Nominal expectedATy unwrapN)+ pure $ Left ((EvExpr dictExpr, ct), [mkNonCanonical eqEv])+ -- Terminal type discrepancy: emit diagnostic and safe dummy evidence+ | otherwise -> do+ let dummyExpr = mkIntExpr 0+ dummyDict = evDataConApp (classDataCon cls) tys [dummyExpr]+ diagLines =+ [ "Polytropos Record Error:"+ , " Matched field type:"+ , " " ++ showSDocUnsafe (ppr unwrapN)+ , " but expected:"+ , " " ++ showSDocUnsafe (ppr expectedATy)+ ]+ errCt <- mkTypeErrorCt state loc diagLines+ pure $ Left ((EvExpr dummyDict, ct), [errCt]) Nothing -> do case walkRowWithTypes_maybe rowTy of Just fields -> do@@ -1184,6 +1240,7 @@ -- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence] -- See Note [Human-Centric TypeError Diagnostics & Fuzzy Matching] [ref:note-typeerror-diagnostics] -- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+-- See Note [Poly-Kinded Row Indexing for Multi-Sorted Effects] [ref:note-poly-kinded-indexing] -- -- Execution Phases: -- 1. Deconstruct Constructor Predicate:@@ -1976,6 +2033,248 @@ , " in super-record." ] | otherwise -> findSubRowMismatch rest sFields++-------------------------------------------------------------------------------+-- KnownRowMorph solver+--+-- See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing]+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+-------------------------------------------------------------------------------++-- | Solves the 'KnownRowMorph r1 r2' constraint by synthesizing an unboxed 'RowMorph'+-- permutation array directly into Core AST.+--+-- Algorithmic Mechanics:+-- 1. Unpack Row Arguments:+-- Extracts source row 'r1Ty' and target row 'r2Ty'.+-- 2. Open-Tail Deferral:+-- Inspects both rows using 'walkRowWithTypes_maybe'. If either row contains an unfixed+-- type variable tail, returns 'Right ()' (defer), allowing GHC to ground row tails first.+-- 3. Field Matching & Permutation Vector Synthesis:+-- For each field in 'r1', searches 'r2' for a matching field name.+-- - If field types match under 'eqType': emits the target slot index.+-- - If field types differ and either is open: emits target slot index AND a new wanted+-- nominal equality constraint to unify them.+-- - If field types differ and both are closed: synthesizes custom 'TypeError' diagnostic+-- and safe dummy evidence.+-- - If field is missing: synthesizes custom 'TypeError' diagnostic with Levenshtein fuzzy+-- typo suggestions and safe dummy evidence.+-- 4. Direct Core AST Synthesis:+-- Emits Core call to 'unsafeMkRowMorph @tys [i_0, i_1, ...]' wrapped in the 'KnownRowMorph'+-- class dictionary constructor, producing an unboxed 'PrimArray Int' at runtime with+-- zero dictionary search.+solveKnownRowMorph+ :: PluginState+ -> Ct+ -> Class+ -> [Type]+ -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveKnownRowMorph state ct cls tys+ | length tys >= 2+ , let r1Ty = tys !! (length tys - 2)+ , let r2Ty = last tys+ , let loc = ctLoc ct+ , Just r1Fields <- walkRowWithTypes_maybe r1Ty+ , Just r2Fields <- walkRowWithTypes_maybe r2Ty+ = do+ matchResult <- matchRowMorphFields loc r1Fields r2Fields+ case matchResult of+ Right (idxs, newWanteds) -> do+ let idxExprs = map mkIntExpr idxs+ idxList = mkListExpr intTy idxExprs+ evExpr = mkCoreApps (Var (psUnsafeMkRowMorph state)) (map Type tys ++ [idxList])+ dictExpr = evDataConApp (classDataCon cls) tys [evExpr]+ pure $ Left ((EvExpr dictExpr, ct), newWanteds)+ Left diagLines -> do+ let dummyExpr = mkCoreApps (Var (psUnsafeMkRowMorph state)) (map Type tys ++ [mkListExpr intTy []])+ dummyDict = evDataConApp (classDataCon cls) tys [dummyExpr]+ errCt <- mkTypeErrorCt state loc diagLines+ pure $ Left ((EvExpr dummyDict, ct), [errCt])+ | otherwise = pure $ Right ()+ where+ matchRowMorphFields+ :: CtLoc+ -> [(Int, FastString, Type)]+ -> [(Int, FastString, Type)]+ -> TcPluginM 'Solve (Either [String] ([Int], [Ct]))+ matchRowMorphFields _loc [] _ = pure $ Right ([], [])+ matchRowMorphFields loc ((_, name, fieldTy) : rest) sFields =+ case [ (j, sFieldTy) | (j, sName, sFieldTy) <- sFields+ , if nullFS name || nullFS sName then True else sName == name ] of+ [] -> do+ let sNames = [ unpackFS n | (_, n, _) <- sFields, not (nullFS n) ]+ diag = [ "Polytropos RowMorph Error:"+ , " Cannot construct RowMorph: field '" ++ unpackFS name ++ "' is missing in target row:"+ , " " ++ formatRecordRow sFields+ , " " ++ formatSuggestion (unpackFS name) sNames+ ]+ pure $ Left diag+ ((j, sFieldTy) : _)+ | fieldTy `eqType` sFieldTy -> do+ restRes <- matchRowMorphFields loc rest sFields+ case restRes of+ Right (idxs, wts) -> pure $ Right (j : idxs, wts)+ Left diag -> pure $ Left diag+ | not (isClosedType fieldTy) || not (isClosedType sFieldTy) -> do+ eqEv <- newWanted loc (mkEqPredRole Nominal fieldTy sFieldTy)+ restRes <- matchRowMorphFields loc rest sFields+ case restRes of+ Right (idxs, wts) -> pure $ Right (j : idxs, mkNonCanonical eqEv : wts)+ Left diag -> pure $ Left diag+ | otherwise -> do+ let diag = [ "Polytropos RowMorph Error:"+ , " Field '" ++ unpackFS name ++ "' has incompatible types in source and target rows:"+ , " Source type: " ++ showSDocUnsafe (ppr fieldTy)+ , " Target type: " ++ showSDocUnsafe (ppr sFieldTy)+ ]+ pure $ Left diag++-------------------------------------------------------------------------------+-- FrameWire solver+--+-- See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring]+-- See Note [Literal Evidence Synthesis vs Type-Level Search] [ref:note-literal-evidence]+-- See Note [Row Type Anatomy: Open vs Closed Rows and Fixed vs Unfixed Tails] [ref:note-row-anatomy]+-- See Note [Diagnostic Recovery and Cascading Error Prevention] [ref:note-diagnostic-prevention]+-------------------------------------------------------------------------------++-- | Solves the 'FrameWire frameIn opIn opOut frameOut' constraint:+-- 1. Checks open-tail deferral on 'frameIn', 'opIn', and 'opOut'.+-- 2. Verifies 'opIn' is a sub-row of 'frameIn', mapping gather indices and+-- emitting nominal equality constraints for polymorphic port types.+-- 3. Computes the canonical overwritten row 'RowOverwrite frameIn opOut'.+-- 4. Computes 'baseIdxs' and 'opIdxs'.+-- 5. Synthesizes 'synthOutTy' and unifies with 'frameOutTy' via nominal equality.+-- 6. Emits Core call to 'unsafeMkFramePlan' wrapped in the 'FrameWire' dictionary.+solveFrameWire+ :: PluginState+ -> Ct+ -> Class+ -> [Type]+ -> TcPluginM 'Solve (Either ((EvTerm, Ct), [Ct]) ())+solveFrameWire state ct cls tys+ | length tys >= 4+ , let len = length tys+ frameInTy = tys !! (len - 4)+ opInTy = tys !! (len - 3)+ opOutTy = tys !! (len - 2)+ frameOutTy = last tys+ loc = ctLoc ct+ , Just fInFields <- walkRowWithTypes_maybe frameInTy+ , Just oInFields <- walkRowWithTypes_maybe opInTy+ , Just oOutFields <- walkRowWithTypes_maybe opOutTy+ = do+ matchResult <- matchFrameInPorts loc oInFields fInFields+ case matchResult of+ Right (gatherIdxs, inEqCts) -> do+ -- Compute canonical overwritten row:+ -- 1. Surviving frameIn fields updated with new types from opOut.+ -- 2. New opOut fields appended to the end.+ let updatedFIn =+ [ case [ oTy | (_, oName, oTy) <- oOutFields+ , if nullFS fName || nullFS oName then True else oName == fName ] of+ (newTy : _) -> (fName, newTy)+ [] -> (fName, fTy)+ | (_, fName, fTy) <- fInFields+ ]+ newOpOut =+ [ (oName, oTy)+ | (_, oName, oTy) <- oOutFields+ , null [ () | (_, fName, _) <- fInFields+ , if nullFS fName || nullFS oName then True else fName == oName ]+ ]+ mergedList = updatedFIn ++ newOpOut+ outSz = length mergedList++ baseIdxs = [0 .. length fInFields - 1]+ lookupSlot oName =+ case [ idx | (idx, (mName, _)) <- zip [0..] mergedList+ , if nullFS oName || nullFS mName then True else mName == oName ] of+ (idx : _) -> idx+ [] -> error "Polytropos.Plugin: impossible missing merged label in FrameWire"+ opIdxs = [ lookupSlot oName | (_, oName, _) <- oOutFields ]++ -- Reify the synthesized frameOut row type+ kTy = case (fInFields, oOutFields) of+ ((_, _, ty) : _, _) -> typeKind ty+ (_, (_, _, ty) : _) -> typeKind ty+ _ -> liftedTypeKind+ entryKind = mkTyConApp (psPairTyCon state) [typeSymbolKind, kTy]+ entries =+ [ mkTyConApp (psPromotedPair state)+ [ typeSymbolKind+ , typeKind ty+ , mkStrLitTy name+ , ty+ ]+ | (name, ty) <- mergedList+ ]+ synthOutTy = mkPromotedListTy entryKind entries++ -- Unify frameOut with synthesized row if not already syntactically equal+ outEqCts <- if frameOutTy `eqType` synthOutTy+ then pure []+ else do+ outEqEv <- newWanted loc (mkEqPredRole Nominal frameOutTy synthOutTy)+ pure [mkNonCanonical outEqEv]++ let outSzExpr = mkIntExpr outSz+ gatherExpr = mkListExpr intTy (map mkIntExpr gatherIdxs)+ baseExpr = mkListExpr intTy (map mkIntExpr baseIdxs)+ opExpr = mkListExpr intTy (map mkIntExpr opIdxs)+ evExpr = mkCoreApps (Var (psUnsafeMkFrame state))+ (map Type tys ++ [outSzExpr, gatherExpr, baseExpr, opExpr])+ dictExpr = evDataConApp (classDataCon cls) tys [evExpr]++ pure $ Left ((EvExpr dictExpr, ct), outEqCts ++ inEqCts)++ Left diagLines -> do+ -- Input port mismatch: synthesize custom diagnostic and dummy evidence+ let dummyExpr = mkCoreApps (Var (psUnsafeMkFrame state))+ (map Type tys ++ [mkIntExpr 0, mkListExpr intTy [], mkListExpr intTy [], mkListExpr intTy []])+ dummyDict = evDataConApp (classDataCon cls) tys [dummyExpr]+ errCt <- mkTypeErrorCt state loc diagLines+ pure $ Left ((EvExpr dummyDict, ct), [errCt])+ | otherwise = pure $ Right () -- Open tail deferral: wait until frameIn, opIn, and opOut are grounded+ where+ matchFrameInPorts+ :: CtLoc+ -> [(Int, FastString, Type)]+ -> [(Int, FastString, Type)]+ -> TcPluginM 'Solve (Either [String] ([Int], [Ct]))+ matchFrameInPorts _loc [] _ = pure $ Right ([], [])+ matchFrameInPorts loc ((_, inName, inTy) : rest) fFields =+ case [ (j, fTy) | (j, fName, fTy) <- fFields+ , if nullFS inName || nullFS fName then True else fName == inName ] of+ [] -> do+ let fNames = [ unpackFS n | (_, n, _) <- fFields, not (nullFS n) ]+ diag = [ "Polytropos FrameWire Error:"+ , " Cannot wire operation: input port '" ++ unpackFS inName ++ "' is missing in frame:"+ , " " ++ formatRecordRow fFields+ , " " ++ formatSuggestion (unpackFS inName) fNames+ ]+ pure $ Left diag+ ((j, fTy) : _)+ | inTy `eqType` fTy -> do+ restRes <- matchFrameInPorts loc rest fFields+ case restRes of+ Right (idxs, wts) -> pure $ Right (j : idxs, wts)+ Left diag -> pure $ Left diag+ | not (isClosedType inTy) || not (isClosedType fTy) -> do+ eqEv <- newWanted loc (mkEqPredRole Nominal inTy fTy)+ restRes <- matchFrameInPorts loc rest fFields+ case restRes of+ Right (idxs, wts) -> pure $ Right (j : idxs, mkNonCanonical eqEv : wts)+ Left diag -> pure $ Left diag+ | otherwise -> do+ let diag = [ "Polytropos FrameWire Error:"+ , " Input port '" ++ unpackFS inName ++ "' has incompatible types in operation and frame:"+ , " Operation input type: " ++ showSDocUnsafe (ppr inTy)+ , " Frame port type: " ++ showSDocUnsafe (ppr fTy)+ ]+ pure $ Left diag -- | Solves the 'SubSum sub super' constraint by synthesizing literal injection and narrowing arrays. --
tests/smoke/Main.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-}@@ -21,6 +22,7 @@ import Data.Functor.Identity (Identity(..)) import Data.Kind (Type) import Data.List (isInfixOf)+import Data.Primitive.PrimArray (sizeofPrimArray) import Data.Primitive.SmallArray (SmallArray, sizeofSmallArray, indexSmallArray) import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl))@@ -188,6 +190,112 @@ Nothing -> pure () Just _ -> error "expected Nothing in narrowVariant" ]+ , testGroup "RowMorph compile-time synthesis"+ [ testCase "KnownRowMorph solves for identity morphism" $ do+ let m = rowMorph @BigProd @BigProd+ sizeofPrimArray (unRowMorph m) @?= 3+ indexRowMorph m 0 @?= 0+ indexRowMorph m 1 @?= 1+ indexRowMorph m 2 @?= 2+ , testCase "KnownRowMorph solves for permutation and subrow projection" $ do+ let m = rowMorph @SmallProd @BigProd+ sizeofPrimArray (unRowMorph m) @?= 2+ indexRowMorph m 0 @?= 2+ indexRowMorph m 1 @?= 0+ , testCase "gatherRecord with plugin-solved rowMorph" $ do+ let full = REC { a = (100 :: Int), b = True, c = "test" } :: Record BigProd+ sub = gatherRecord (rowMorph @SmallProd @BigProd) full+ sub.c @?= Identity "test"+ sub.a @?= Identity (100 :: Int)+ , testCase "scatterRecord with plugin-solved rowMorph" $ do+ let full = REC { a = (100 :: Int), b = True, c = "test" } :: Record BigProd+ sub = REC { c = "updated", a = (999 :: Int) } :: Record SmallProd+ full' = scatterRecord (rowMorph @SmallProd @BigProd) sub full+ full'.a @?= Identity (999 :: Int)+ full'.b @?= Identity True+ full'.c @?= Identity "updated"+ , testCase "composeRowMorph with plugin-solved rowMorphs" $ do+ let m1 = rowMorph @'[ "c" := String ] @SmallProd+ m2 = rowMorph @SmallProd @BigProd+ mComposed = composeRowMorph m1 m2+ sizeofPrimArray (unRowMorph mComposed) @?= 1+ indexRowMorph mComposed 0 @?= 2+ ]+ , testGroup "FrameWire compile-time auto-wiring and row overwrite"+ [ testCase "FrameWire solves for concrete frames and computes correct slot maps" $ do+ let plan = framePlan @FWFrameIn @FWOpIn @FWOpOut @FWFrameOut+ fpOutSize plan @?= 3+ indexRowMorph (fpGatherIn plan) 0 @?= 1+ indexRowMorph (fpBaseScatter plan) 0 @?= 0+ indexRowMorph (fpBaseScatter plan) 1 @?= 1+ indexRowMorph (fpOpScatter plan) 0 @?= 1+ indexRowMorph (fpOpScatter plan) 1 @?= 2+ , testCase "FrameWire unifies uninstantiated frameOut type variable and runs executeFrameRecord" $ do+ let baseRec = REC { x = (42 :: Int), y = False }+ opRec = REC { y = 'Z', z = (3.14 :: Double) }+ outRec = executeFrameRecord (framePlan @FWFrameIn @FWOpIn @FWOpOut)+ baseRec+ opRec+ outRec.x @?= Identity (42 :: Int)+ outRec.y @?= Identity 'Z'+ outRec.z @?= Identity (3.14 :: Double)+ , testCase "FrameWire with non-overlapping opOut appends new ports" $ do+ let baseRec = REC { a = (10 :: Int), b = True }+ opRec = REC { c = "appended" }+ outRec = executeFrameRecord (framePlan @'[ "a" := Int, "b" := Bool ]+ @'[ "a" := Int ]+ @'[ "c" := String ])+ baseRec+ opRec+ outRec.a @?= Identity (10 :: Int)+ outRec.b @?= Identity True+ outRec.c @?= Identity "appended"+ ]+ , testGroup "Poly-Kinded Effect Row Indexing (PolyEffect, PolyHEffect)"+ [ testCase "FieldIndex by symbol on RowOf PolyEffect" $ do+ fieldIndex @_ @"state" @MyEf @StateEff @?= 0+ fieldIndex @_ @"log" @MyEf @LogEff @?= 1+ fieldIndex @_ @"http" @MyEf @HttpEff @?= 2+ , testCase "FieldIndex by symbol on RowOf PolyHEffect" $ do+ fieldIndex @_ @"async" @MyHEf @AsyncHEff @?= 0+ fieldIndex @_ @"catch" @MyHEf @CatchHEff @?= 1+ , testCase "ConstructorIndex by symbol on RowOf PolyEffect" $ do+ constructorIndex @_ @"state" @MyEf @?= 0+ constructorIndex @_ @"log" @MyEf @?= 1+ constructorIndex @_ @"http" @MyEf @?= 2+ , testCase "ConstructorIndex by symbol on RowOf PolyHEffect" $ do+ constructorIndex @_ @"async" @MyHEf @?= 0+ constructorIndex @_ @"catch" @MyHEf @?= 1+ , testCase "FieldIndex by type on labeled RowOf PolyEffect" $ do+ fieldIndex @_ @StateEff @MyEf @StateEff @?= 0+ fieldIndex @_ @LogEff @MyEf @LogEff @?= 1+ fieldIndex @_ @HttpEff @MyEf @HttpEff @?= 2+ , testCase "ConstructorIndex by type on labeled RowOf PolyEffect" $ do+ constructorIndex @_ @StateEff @MyEf @?= 0+ constructorIndex @_ @LogEff @MyEf @?= 1+ constructorIndex @_ @HttpEff @MyEf @?= 2+ , testCase "ConstructorIndex by type on labeled RowOf PolyHEffect" $ do+ constructorIndex @_ @AsyncHEff @MyHEf @?= 0+ constructorIndex @_ @CatchHEff @MyHEf @?= 1+ , testCase "FieldIndex by type on unlabeled [PolyEffect]" $ do+ fieldIndex @_ @StateEff @MyAnonEf @StateEff @?= 0+ fieldIndex @_ @LogEff @MyAnonEf @LogEff @?= 1+ fieldIndex @_ @HttpEff @MyAnonEf @HttpEff @?= 2+ , testCase "ConstructorIndex by type on unlabeled [PolyEffect]" $ do+ constructorIndex @_ @StateEff @MyAnonEf @?= 0+ constructorIndex @_ @LogEff @MyAnonEf @?= 1+ constructorIndex @_ @HttpEff @MyAnonEf @?= 2+ , testCase "ConstructorIndex by type on unlabeled [PolyHEffect]" $ do+ constructorIndex @_ @AsyncHEff @MyAnonHEf @?= 0+ constructorIndex @_ @CatchHEff @MyAnonHEf @?= 1+ , testCase "Inferred effect type variable resolution via nominal equality" $ do+ let idxState = getEffectIndex @"state" @MyEf+ idxLog = getEffectIndex @"log" @MyEf+ idxHttp = getEffectIndex @"http" @MyEf+ idxState @?= 0+ idxLog @?= 1+ idxHttp @?= 2+ ] , testGroup "Compile-time label hashing (KnownHash)" [ testCase "knownHash solves on literal symbols and matches fnv1a64" $ do knownHash @"x" @?= fnv1a64 "x"@@ -418,6 +526,72 @@ , "sub-variant payload: { x :: Int }" , "super-variant payload: { x :: String }" ]+ , testCase "RowMorph missing field diagnostic" $+ checkGhcDiag+ (unlines+ [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+ , "module Test where"+ , "import Polytropos"+ , "t = rowMorph @'[ \"missing\" := Int ] @'[ \"a\" := Int, \"b\" := Bool ]"+ ])+ [ "Polytropos RowMorph Error:"+ , "Cannot construct RowMorph: field 'missing' is missing in target row:"+ , "{ a :: Int, b :: Bool }"+ , "Available fields: 'a', 'b'"+ ]+ , testCase "RowMorph field type mismatch diagnostic" $+ checkGhcDiag+ (unlines+ [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+ , "module Test where"+ , "import Polytropos"+ , "t = rowMorph @'[ \"a\" := String ] @'[ \"a\" := Int, \"b\" := Bool ]"+ ])+ [ "Polytropos RowMorph Error:"+ , "Field 'a' has incompatible types in source and target rows:"+ ]+ , testCase "FrameWire missing input port diagnostic" $+ checkGhcDiag+ (unlines+ [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+ , "module Test where"+ , "import Polytropos"+ , "t = framePlan @'[ \"x\" := Int ] @'[ \"missing\" := Bool ] @'[ \"x\" := Int ]"+ ])+ [ "Polytropos FrameWire Error:"+ , "Cannot wire operation: input port 'missing' is missing in frame:"+ , "{ x :: Int }"+ ]+ , testCase "FrameWire input port type mismatch diagnostic" $+ checkGhcDiag+ (unlines+ [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+ , "module Test where"+ , "import Polytropos"+ , "t = framePlan @'[ \"x\" := Int ] @'[ \"x\" := Bool ] @'[ \"x\" := Int ]"+ ])+ [ "Polytropos FrameWire Error:"+ , "Input port 'x' has incompatible types in operation and frame:"+ , "Operation input type: Bool"+ , "Frame port type: Int"+ ]+ , testCase "missing constructor diagnostic on unlabeled effect row formats cleanly" $+ checkGhcDiag+ (unlines+ [ "{-# LANGUAGE DataKinds, TypeApplications, TypeOperators #-}"+ , "module Test where"+ , "import Data.Kind (Type)"+ , "import Polytropos"+ , "import Polytropos.Core"+ , "type PolyEffect = RowOf Type -> RowOf (RowOf Type) -> Type"+ , "data StateEff (ins :: RowOf Type) (outs :: RowOf (RowOf Type))"+ , "data LogEff (ins :: RowOf Type) (outs :: RowOf (RowOf Type))"+ , "t = constructorIndex @_ @\"missing\" @'[ StateEff, LogEff ]"+ ])+ [ "Polytropos Variant Error:"+ , "Constructor 'missing' is not a member of variant:"+ , "< StateEff | LogEff >"+ ] ] ] @@ -537,3 +711,35 @@ -- | Big sum and sub-sum for testing SubSum evidence. type BigSum = '[ "A" := '[], "B" := '[ "x" := Int ], "C" := '[ "y" := Bool ] ] type SmallSum = '[ "A" := '[], "C" := '[ "y" := Bool ] ]++-- | Frames for testing FrameWire evidence.+type FWFrameIn = '[ "x" := Int, "y" := Bool ]+type FWOpIn = '[ "y" := Bool ]+type FWOpOut = '[ "y" := Char, "z" := Double ]+type FWFrameOut = '[ "x" := Int, "y" := Char, "z" := Double ]++-- | Poly-kinded effect signatures and rows for testing Milestone 1.3+type PolyEffect = RowOf Type -> RowOf (RowOf Type) -> Type++data StateEff (ins :: RowOf Type) (outs :: RowOf (RowOf Type))+data LogEff (ins :: RowOf Type) (outs :: RowOf (RowOf Type))+data HttpEff (ins :: RowOf Type) (outs :: RowOf (RowOf Type))++data PortSig = PortSig (RowOf Type) (RowOf Type)+type PolyHEffect = (PortSig -> Type) -> RowOf PortSig -> RowOf Type -> RowOf (RowOf Type) -> Type++data AsyncHEff (m :: PortSig -> Type) (r :: RowOf PortSig) (ins :: RowOf Type) (outs :: RowOf (RowOf Type))+data CatchHEff (m :: PortSig -> Type) (r :: RowOf PortSig) (ins :: RowOf Type) (outs :: RowOf (RowOf Type))++type MyEffects = EffectRowOf PolyEffect+type MyEf = '[ "state" := StateEff, "log" := LogEff, "http" := HttpEff ] :: MyEffects++type MyHEffects = EffectRowOf PolyHEffect+type MyHEf = '[ "async" := AsyncHEff, "catch" := CatchHEff ] :: MyHEffects++type MyAnonEf = '[ StateEff, LogEff, HttpEff ]+type MyAnonHEf = '[ AsyncHEff, CatchHEff ]++-- | Helper function testing polymorphic type variable inference for FieldIndex+getEffectIndex :: forall (l :: Symbol) ef a. FieldIndex l ef a => Int+getEffectIndex = fieldIndex @_ @l @ef @a