diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/polytropos-plugin.cabal b/polytropos-plugin.cabal --- a/polytropos-plugin.cabal +++ b/polytropos-plugin.cabal @@ -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 @@ -68,7 +68,6 @@ , tasty-hunit >= 0.10 && < 0.11 , polytropos-plugin , process - , filepath , directory ghc-options: diff --git a/src/Polytropos/Plugin.hs b/src/Polytropos/Plugin.hs --- a/src/Polytropos/Plugin.hs +++ b/src/Polytropos/Plugin.hs @@ -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. -- diff --git a/tests/smoke/Main.hs b/tests/smoke/Main.hs --- a/tests/smoke/Main.hs +++ b/tests/smoke/Main.hs @@ -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