From 4c13415e3cea7a7166050815caec01bc4066b84f Mon Sep 17 00:00:00 2001 From: rodrigogribeiro Date: Sun, 14 Jun 2026 16:57:44 -0300 Subject: [PATCH 01/10] Fixing specialization and type inference for ABI encoding. --- src/Solcore/Backend/Specialise.hs | 85 +++++++++++++++++++- src/Solcore/Frontend/TypeInference/TcStmt.hs | 52 +++++++++++- 2 files changed, 133 insertions(+), 4 deletions(-) diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs index e9acbfa9..96fee2a8 100644 --- a/src/Solcore/Backend/Specialise.hs +++ b/src/Solcore/Backend/Specialise.hs @@ -347,10 +347,25 @@ specConApp i@(Id _n conTy) args ty = do let i' = applytv subst i let typedArgs = zip args argTypes' args' <- forM typedArgs (uncurry specExp) + -- Unify the constructor's result type (from the current subst-applied conTy) + -- with the target type ty. This resolves phantom type parameters that do + -- not appear in the constructor arguments (e.g. the 'ty' in + -- ABIDecoder(ty, reader) = ABIDecoder(reader)), whose type var may differ + -- from the caller's declared variable because the type checker used a + -- fresh meta-variable and did not fully substitute it before emitting the + -- typed AST. + let resultConTy = applytv subst (resultTy conTy) + case specmgu resultConTy ty of + Right phi -> extSpSubst phi + Left _ -> return () let conTy' = foldr (:->) ty argTypes' debug ["> specConApp: ", prettyId i, " : ", pretty conTy, " ~> ", prettyId i', " : ", pretty conTy'] debug ["< specConApp: ", prettyConApp i args, " ~> ", prettyConApp i' args'] return (i', args') + where + -- Extract the result type of a function type (strip all arrows) + resultTy (t :-> rest) = resultTy rest + resultTy t = t -- | Specialise a function call -- given actual arguments and the expected result type @@ -447,6 +462,11 @@ specFunDef fd0 = withLocalState do -- add a placeholder first to break loops let placeholder = FunDef (funIsPublic fd) sig' [] addSpecialisation name' placeholder + -- Resolve MPTC extra type parameters from constraints. + -- E.g. for forall a rep. a:Generic(rep) => f(x:a)... + -- when a is concrete (say Option(uint256)) but rep is still free, + -- look up a Generic method for Option(uint256) to determine rep. + resolveMPTCFromPreds (sigContext sig') body' <- specBody (funDefBody fd) let fd' = FunDef (funIsPublic fd) sig' {sigName = name'} body' debug ["+ specFunDef: adding specialisation ", show name', " : ", pretty ty'] @@ -456,6 +476,53 @@ specFunDef fd0 = withLocalState do specBody :: [Stmt Id] -> SM [Stmt Id] specBody = mapM specStmt +-- Resolve MPTC extra type parameters from function constraints. +-- When a constraint InCls cls mainTy [extra] has a concrete mainTy but +-- free extra type parameters, search the resolution table for a method of +-- cls whose stored type can be unified against patterns involving mainTy, +-- then extend the substitution with the discovered bindings. +-- This handles cases like forall a rep. a:Generic(rep) => ... where a +-- is determined from the call site but rep must come from the instance. +resolveMPTCFromPreds :: [Pred] -> SM () +resolveMPTCFromPreds preds = do + subst <- getSpSubst + forM_ preds $ \pred -> case pred of + InCls clsName mainTy extras -> do + let mainTy' = applytv subst mainTy + extras' = map (applytv subst) extras + when (null (freetv mainTy') && any (not . null . freetv) extras') $ + tryResolveMPTC clsName mainTy' extras' + _ -> return () + +tryResolveMPTC :: Name -> Ty -> [Ty] -> SM () +tryResolveMPTC clsName mainTy extras = do + resTable <- gets spResTable + forM_ (Map.toList resTable) $ \(methName, entries) -> + when (isMethodOf clsName methName) $ + forM_ entries $ \(storedTy, _) -> do + freshV <- TyVar . TVar <$> spNewName + -- Template A: method takes mainTy as first arg, returns rep + -- e.g. Generic.from : a -> rep + tryMPTCTemplate extras freshV storedTy (mainTy :-> freshV) + -- Template B: method takes rep as first arg, returns mainTy + -- e.g. Generic.to : rep -> a + tryMPTCTemplate extras freshV storedTy (freshV :-> mainTy) + where + isMethodOf cls (QualName cn _) = cn == cls + isMethodOf _ _ = False + +tryMPTCTemplate :: [Ty] -> Ty -> Ty -> Ty -> SM () +tryMPTCTemplate extras freshV storedTy template = + case specmgu storedTy template of + Left _ -> return () + Right phi -> do + let concrete = applytv phi freshV + when (null (freetv concrete)) $ + forM_ extras $ \extra -> + case specmgu extra concrete of + Left _ -> return () + Right phi2 -> extSpSubst phi2 + {- ensureSimple ty' stmt subst = case ty' of TyVar _ -> panics [ "specStmt(",pretty stmt,"): polymorphic return type: " @@ -525,7 +592,7 @@ specStmt stmt@(Var i := e) = do return $ Var i' := e' specStmt stmt@(Let ct i mty mexp) = do subst <- getSpSubst - debug ["> specStmt (Let): ", pretty i, " : ", pretty (idType i), " @ ", pretty subst] + debug ["> specStmt (Let): ", pretty i, " : ", pretty (idType i), " mty=", maybe "Nothing" pretty mty, " @ ", pretty subst] i' <- atCurrentSubst i let ty' = idType i' case mexp of @@ -541,7 +608,21 @@ specStmt stmt@(Let ct i mty mexp) = do e' <- specExp e ty' return $ Let ct i' mty' (Just e') else do - e' <- specExp e ty' + -- ty' still has free type variables. Try to resolve them from the + -- explicit type annotation (mty), which went through elabFunDef and + -- has the original forall-bound names (_g2, _h2, …) that are already + -- in the current substitution. This handles the case where the type + -- checker introduced a fresh meta-variable for a phantom type + -- parameter (e.g. the `ty` in `ABIDecoder(ty, reader)`) that was + -- never renamed to the function's forall variable. + ty_for_spec <- case mty of + Just ann -> do + ann' <- atCurrentSubst ann + case specmgu ty' ann' of + Right phi -> extSpSubst phi >> atCurrentSubst ty' + Left _ -> return ty' + Nothing -> return ty' + e' <- specExp e ty_for_spec subst' <- getSpSubst i'' <- atCurrentSubst i let ty'' = idType i'' diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs index 2a3ccecc..adc3a451 100644 --- a/src/Solcore/Frontend/TypeInference/TcStmt.hs +++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs @@ -753,15 +753,63 @@ elabFunDef :: Scheme -> -- function infered type Scheme -> -- function annotated type TcM (FunDef Id) -elabFunDef isPub vs sig bdy (Forall _ (_ :=> tinf)) ann@(Forall _ (_ :=> tann)) = +elabFunDef isPub vs sig bdy (Forall _ (pinf :=> tinf)) ann@(Forall _ (pann :=> tann)) = do let tinf' = everywhere (mkT toMeta) tinf tann' = everywhere (mkT toMeta) tann s <- unify tinf' tann' + -- Find bindings for phantom predicate variables (those appearing only in + -- predicates, not in the function type). sig2's context uses annotation + -- TyVars (e.g. "rep"), but the body uses body TyVars (e.g. "$106550"). + -- Build a TyVar-level renaming from the delta and patch sig2's context. + phantomDelta <- findPhantomPredBindings pann pinf + let tvs = [(gvar mv, gen ty) | (mv, ty) <- phantomDelta] + substTVPhantom t@(TyVar v) = fromMaybe t (lookup v tvs) + substTVPhantom t = t sig2 <- elabSignature vs sig ann - let fd2 = everywhere (mkT (apply @Ty s)) (FunDef isPub sig2 bdy) + let sig2' = everywhere (mkT substTVPhantom) sig2 + let fd2 = everywhere (mkT (apply @Ty s)) (FunDef isPub sig2' bdy) pure (everywhere (mkT gen) fd2) +-- Unify annotation predicates against inferred predicates locally to discover +-- mappings for phantom type variables (those absent from the function type). +-- Returns new (annotation_meta -> body_meta) bindings for phantom variables, +-- then restores the global substitution to its state on entry. +findPhantomPredBindings :: [Pred] -> [Pred] -> TcM [(MetaTv, Ty)] +findPhantomPredBindings pann pinf = do + s0 <- getSubst + let pann' = apply s0 (everywhere (mkT toMeta) pann) + pinf' = everywhere (mkT toMeta) pinf + dom_s0 = map fst (unSubst s0) + forM_ (phantomMatchingPreds dom_s0 pann' pinf') $ \(pa, pi_) -> + catchError (unifyPredExtras pa pi_) (\_ -> return ()) + s_full <- getSubst + let delta = filter (\(v,_) -> v `notElem` dom_s0) (unSubst s_full) + putSubst s0 -- restore global subst + return delta + +-- Match annotation preds against inferred preds, keeping only pairs where the +-- inferred pred contains at least one meta that is NOT in dom_s0 (i.e. phantom). +-- This avoids cross-product pairings for predicates with the same class name where +-- the body metas are already bound (non-phantom). +phantomMatchingPreds :: [MetaTv] -> [Pred] -> [Pred] -> [(Pred, Pred)] +phantomMatchingPreds dom_s0 pann pinf = + [ (pa, pi_) + | pa@(InCls cls _ _) <- pann + , pi_@(InCls cls' _ _) <- pinf + , cls == cls' + , hasPhantomMeta pi_ + ] + where + hasPhantomMeta (InCls _ mt exts) = any (`notElem` dom_s0) (mv mt `union` mv exts) + hasPhantomMeta _ = False + +unifyPredExtras :: Pred -> Pred -> TcM () +unifyPredExtras (InCls _ mt1 exts1) (InCls _ mt2 exts2) = do + void $ unify mt1 mt2 + zipWithM_ (\e1 e2 -> void $ unify e1 e2) exts1 exts2 +unifyPredExtras _ _ = return () + toMeta :: Ty -> Ty toMeta (TyVar (TVar n)) = Meta (MetaTv n) toMeta (TyCon n ts) = TyCon n (map toMeta ts) From d8964a53fc954fb9de5a5edb6b6337633fc7a044 Mon Sep 17 00:00:00 2001 From: rodrigogribeiro Date: Sun, 14 Jun 2026 17:05:36 -0300 Subject: [PATCH 02/10] Ormulu --- src/Solcore/Backend/Specialise.hs | 24 ++++++++++---------- src/Solcore/Frontend/TypeInference/TcStmt.hs | 18 +++++++-------- 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs index 96fee2a8..8d8dac3f 100644 --- a/src/Solcore/Backend/Specialise.hs +++ b/src/Solcore/Backend/Specialise.hs @@ -357,15 +357,15 @@ specConApp i@(Id _n conTy) args ty = do let resultConTy = applytv subst (resultTy conTy) case specmgu resultConTy ty of Right phi -> extSpSubst phi - Left _ -> return () + Left _ -> return () let conTy' = foldr (:->) ty argTypes' debug ["> specConApp: ", prettyId i, " : ", pretty conTy, " ~> ", prettyId i', " : ", pretty conTy'] debug ["< specConApp: ", prettyConApp i args, " ~> ", prettyConApp i' args'] return (i', args') where -- Extract the result type of a function type (strip all arrows) - resultTy (t :-> rest) = resultTy rest - resultTy t = t + resultTy (_ :-> rest) = resultTy rest + resultTy t = t -- | Specialise a function call -- given actual arguments and the expected result type @@ -486,16 +486,16 @@ specBody = mapM specStmt resolveMPTCFromPreds :: [Pred] -> SM () resolveMPTCFromPreds preds = do subst <- getSpSubst - forM_ preds $ \pred -> case pred of - InCls clsName mainTy extras -> do - let mainTy' = applytv subst mainTy + forM_ preds $ \pred' -> case pred' of + InCls clsName mainTy1 extras -> do + let mainTy' = applytv subst mainTy1 extras' = map (applytv subst) extras when (null (freetv mainTy') && any (not . null . freetv) extras') $ tryResolveMPTC clsName mainTy' extras' _ -> return () tryResolveMPTC :: Name -> Ty -> [Ty] -> SM () -tryResolveMPTC clsName mainTy extras = do +tryResolveMPTC clsName mainTy' extras = do resTable <- gets spResTable forM_ (Map.toList resTable) $ \(methName, entries) -> when (isMethodOf clsName methName) $ @@ -503,13 +503,13 @@ tryResolveMPTC clsName mainTy extras = do freshV <- TyVar . TVar <$> spNewName -- Template A: method takes mainTy as first arg, returns rep -- e.g. Generic.from : a -> rep - tryMPTCTemplate extras freshV storedTy (mainTy :-> freshV) + tryMPTCTemplate extras freshV storedTy (mainTy' :-> freshV) -- Template B: method takes rep as first arg, returns mainTy -- e.g. Generic.to : rep -> a - tryMPTCTemplate extras freshV storedTy (freshV :-> mainTy) + tryMPTCTemplate extras freshV storedTy (freshV :-> mainTy') where isMethodOf cls (QualName cn _) = cn == cls - isMethodOf _ _ = False + isMethodOf _ _ = False tryMPTCTemplate :: [Ty] -> Ty -> Ty -> Ty -> SM () tryMPTCTemplate extras freshV storedTy template = @@ -520,7 +520,7 @@ tryMPTCTemplate extras freshV storedTy template = when (null (freetv concrete)) $ forM_ extras $ \extra -> case specmgu extra concrete of - Left _ -> return () + Left _ -> return () Right phi2 -> extSpSubst phi2 {- @@ -620,7 +620,7 @@ specStmt stmt@(Let ct i mty mexp) = do ann' <- atCurrentSubst ann case specmgu ty' ann' of Right phi -> extSpSubst phi >> atCurrentSubst ty' - Left _ -> return ty' + Left _ -> return ty' Nothing -> return ty' e' <- specExp e ty_for_spec subst' <- getSpSubst diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs index adc3a451..4f3ad739 100644 --- a/src/Solcore/Frontend/TypeInference/TcStmt.hs +++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs @@ -763,9 +763,9 @@ elabFunDef isPub vs sig bdy (Forall _ (pinf :=> tinf)) ann@(Forall _ (pann :=> t -- TyVars (e.g. "rep"), but the body uses body TyVars (e.g. "$106550"). -- Build a TyVar-level renaming from the delta and patch sig2's context. phantomDelta <- findPhantomPredBindings pann pinf - let tvs = [(gvar mv, gen ty) | (mv, ty) <- phantomDelta] + let tvs = [(gvar mv', gen ty) | (mv', ty) <- phantomDelta] substTVPhantom t@(TyVar v) = fromMaybe t (lookup v tvs) - substTVPhantom t = t + substTVPhantom t = t sig2 <- elabSignature vs sig ann let sig2' = everywhere (mkT substTVPhantom) sig2 let fd2 = everywhere (mkT (apply @Ty s)) (FunDef isPub sig2' bdy) @@ -784,8 +784,8 @@ findPhantomPredBindings pann pinf = do forM_ (phantomMatchingPreds dom_s0 pann' pinf') $ \(pa, pi_) -> catchError (unifyPredExtras pa pi_) (\_ -> return ()) s_full <- getSubst - let delta = filter (\(v,_) -> v `notElem` dom_s0) (unSubst s_full) - putSubst s0 -- restore global subst + let delta = filter (\(v, _) -> v `notElem` dom_s0) (unSubst s_full) + putSubst s0 -- restore global subst return delta -- Match annotation preds against inferred preds, keeping only pairs where the @@ -795,14 +795,14 @@ findPhantomPredBindings pann pinf = do phantomMatchingPreds :: [MetaTv] -> [Pred] -> [Pred] -> [(Pred, Pred)] phantomMatchingPreds dom_s0 pann pinf = [ (pa, pi_) - | pa@(InCls cls _ _) <- pann - , pi_@(InCls cls' _ _) <- pinf - , cls == cls' - , hasPhantomMeta pi_ + | pa@(InCls cls _ _) <- pann, + pi_@(InCls cls' _ _) <- pinf, + cls == cls', + hasPhantomMeta pi_ ] where hasPhantomMeta (InCls _ mt exts) = any (`notElem` dom_s0) (mv mt `union` mv exts) - hasPhantomMeta _ = False + hasPhantomMeta _ = False unifyPredExtras :: Pred -> Pred -> TcM () unifyPredExtras (InCls _ mt1 exts1) (InCls _ mt2 exts2) = do From 76effcf51cfe98a684b8fb54bad92123efab50a0 Mon Sep 17 00:00:00 2001 From: Marcin Benke Date: Mon, 15 Jun 2026 15:30:14 +0200 Subject: [PATCH 03/10] fix trailing comma in Generic.solc --- std/Generic.solc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/std/Generic.solc b/std/Generic.solc index 3f4ea5ad..18b180bc 100644 --- a/std/Generic.solc +++ b/std/Generic.solc @@ -3,7 +3,7 @@ pragma no-bounded-variable-condition ABIAttribs, ABIEncode; export { Sum(*), - Generic, + Generic }; import std.{*}; From 50e2227b95be804514f58e2aff5da66138d345e7 Mon Sep 17 00:00:00 2001 From: rodrigogribeiro Date: Tue, 16 Jun 2026 07:24:16 -0300 Subject: [PATCH 04/10] Adding instance environment and matching in specialization --- src/Solcore/Backend/Specialise.hs | 135 +++++++++++++----- src/Solcore/Frontend/TypeInference/TcStmt.hs | 22 ++- test/Cases.hs | 8 ++ test/examples/cases/encoder.solc | 35 +++++ test/examples/cases/encoder1.solc | 26 ++++ test/examples/cases/mptc-both-templates.solc | 34 +++++ .../cases/mptc-guard-extras-concrete.solc | 29 ++++ test/examples/cases/mptc-multi-instance.solc | 41 ++++++ test/examples/cases/mptc-template-a-only.solc | 29 ++++ test/examples/cases/mptc-template-b-only.solc | 31 ++++ test/examples/cases/spec-fail-ungrounded.solc | 29 ++++ 11 files changed, 382 insertions(+), 37 deletions(-) create mode 100644 test/examples/cases/encoder.solc create mode 100644 test/examples/cases/encoder1.solc create mode 100644 test/examples/cases/mptc-both-templates.solc create mode 100644 test/examples/cases/mptc-guard-extras-concrete.solc create mode 100644 test/examples/cases/mptc-multi-instance.solc create mode 100644 test/examples/cases/mptc-template-a-only.solc create mode 100644 test/examples/cases/mptc-template-b-only.solc create mode 100644 test/examples/cases/spec-fail-ungrounded.solc diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs index 8d8dac3f..0484007b 100644 --- a/src/Solcore/Backend/Specialise.hs +++ b/src/Solcore/Backend/Specialise.hs @@ -20,7 +20,7 @@ import Solcore.Frontend.Pretty.SolcorePretty import Solcore.Frontend.Syntax hiding (decls, name) import Solcore.Frontend.TypeInference.Id (Id (..)) import Solcore.Frontend.TypeInference.NameSupply -import Solcore.Frontend.TypeInference.TcEnv (TcEnv (typeTable), TypeInfo (..)) +import Solcore.Frontend.TypeInference.TcEnv (TcEnv (instEnv, typeTable), TypeInfo (..)) import Solcore.Frontend.TypeInference.TcUnify (typesDoNotUnify) import Solcore.Primitives.Primitives hiding (integer) import Solcore.Primitives.Primitives qualified as Prim @@ -476,13 +476,21 @@ specFunDef fd0 = withLocalState do specBody :: [Stmt Id] -> SM [Stmt Id] specBody = mapM specStmt --- Resolve MPTC extra type parameters from function constraints. --- When a constraint InCls cls mainTy [extra] has a concrete mainTy but --- free extra type parameters, search the resolution table for a method of --- cls whose stored type can be unified against patterns involving mainTy, --- then extend the substitution with the discovered bindings. --- This handles cases like forall a rep. a:Generic(rep) => ... where a --- is determined from the call site but rep must come from the instance. +-- Recover concrete bindings for MPTC extra type parameters that are still free +-- after the call-site types have been applied. +-- +-- A constraint InCls cls mainTy [extra] has two groups of type parameters: +-- 1. mainTy: the "self" type, determined directly from the call-site argument +-- or return type (e.g. the concrete type passed to a polymorphic fn) +-- 2. extras: additional class parameters that may not appear in the function +-- type at all (phantom parameters), so they cannot be read off the +-- call site; they must be inferred from the instance. +-- +-- The guard null (freetv mainTy') && any (not . null . freetv) extras' +-- captures exactly the interesting case: mainTy is fully concrete (we know +-- which instance to look at) but at least one extra is still open (we need to +-- read the instance to close it). When all extras are already concrete, or +-- when mainTy itself is still abstract, there is nothing for this function to do. resolveMPTCFromPreds :: [Pred] -> SM () resolveMPTCFromPreds preds = do subst <- getSpSubst @@ -494,34 +502,71 @@ resolveMPTCFromPreds preds = do tryResolveMPTC clsName mainTy' extras' _ -> return () +-- tryResolveMPTC deduces concrete types for the extra parameters of a +-- multi-parameter type class (MPTC) constraint when the "self" (main) type is +-- already fully concrete but some extra parameters are still free type variables. +-- +-- The strategy is to search the type-checker's instance environment for the +-- unique instance of C whose main type matches mainTy', then read the extras +-- directly from the instance head. +-- +-- Soundness: the instance environment is produced and verified by the type +-- checker. Every entry (ctx :=> InCls C instMainTy instExtras) is a +-- certified fact: the type checker has established that instMainTy is an +-- instance of C with extra parameters instExtras. When specmatch confirms that +-- instMainTy matches the concrete mainTy', we have that instExtras is a valid +-- deduction, it recovers exactly what the type checker already knew. +-- +-- Two guards prevent incorrect extensions: +-- +-- 1. all (null . freetv) concreteExtras +-- Only propagate fully ground types. If the matched instance is itself +-- parametric in a variable not pinned by mainTy', we cannot determine a +-- unique concrete type for the extra and skip to avoid a partial binding. +-- +-- 2. specmatch extra concrete returns Left +-- If a call-site extra is already bound to a different type, specmatch +-- fails and the no-op branch preserves the earlier authoritative binding. +-- +-- Note: specmatch (not specmgu) is used throughout because both operations are +-- inherently one-directional. mainTy' is guaranteed ground (no free variables) +-- by the caller, so the instance head is the pattern and the call-site type is +-- the fixed target; there is no need to bind variables on the right-hand side. +-- Using matching rather than unification makes this asymmetry explicit and +-- rules out accidental bindings on the call-site side. tryResolveMPTC :: Name -> Ty -> [Ty] -> SM () tryResolveMPTC clsName mainTy' extras = do - resTable <- gets spResTable - forM_ (Map.toList resTable) $ \(methName, entries) -> - when (isMethodOf clsName methName) $ - forM_ entries $ \(storedTy, _) -> do - freshV <- TyVar . TVar <$> spNewName - -- Template A: method takes mainTy as first arg, returns rep - -- e.g. Generic.from : a -> rep - tryMPTCTemplate extras freshV storedTy (mainTy' :-> freshV) - -- Template B: method takes rep as first arg, returns mainTy - -- e.g. Generic.to : rep -> a - tryMPTCTemplate extras freshV storedTy (freshV :-> mainTy') - where - isMethodOf cls (QualName cn _) = cn == cls - isMethodOf _ _ = False - -tryMPTCTemplate :: [Ty] -> Ty -> Ty -> Ty -> SM () -tryMPTCTemplate extras freshV storedTy template = - case specmgu storedTy template of - Left _ -> return () - Right phi -> do - let concrete = applytv phi freshV - when (null (freetv concrete)) $ - forM_ extras $ \extra -> - case specmgu extra concrete of - Left _ -> return () - Right phi2 -> extSpSubst phi2 + -- The instance environment was produced by the type checker and maps each + -- class name to its list of verified instances. + instTable <- gets (instEnv . spGlobalEnv) + let clsInsts = fromMaybe [] (Map.lookup clsName instTable) + forM_ clsInsts $ \inst -> + case inst of + -- Only class constraint heads are relevant; skip equality constraints. + (_ :=> InCls _ instMainTy instExtras) -> + -- Match the instance's main type (pattern) against the call-site's + -- concrete main type (target). specmatch binds the instance's + -- quantified type variables (TVar) as needed and never touches + -- variables on the target side. Failure means this instance is for + -- a different concrete type; skip silently. + case specmatch instMainTy mainTy' of + Left _ -> return () + Right phi -> do + -- Substitute to obtain the concrete extra types for this instance. + let concreteExtras = map (applytv phi) instExtras + -- If any extra is still abstract, the instance is parametric in a + -- way that mainTy' alone does not determine; skip to stay sound. + when (all (null . freetv) concreteExtras) $ + forM_ (zip extras concreteExtras) $ \(extra, concrete) -> + -- Match the call-site free extra (pattern) against the + -- instance's concrete extra (target). If extra is already + -- bound to the same type this is a no-op (phi = mempty). + -- If bound to a different type specmatch returns Left and the + -- earlier authoritative binding is preserved. + case specmatch extra concrete of + Left _ -> return () + Right phi2 -> extSpSubst phi2 + _ -> return () {- ensureSimple ty' stmt subst = case ty' of @@ -791,6 +836,28 @@ specmgu (TyVar v) t = varBind v t specmgu t (TyVar v) = varBind v t specmgu t1 t2 = typesDoNotUnify t1 t2 +-- | One-directional matching: find a substitution @phi@ such that +-- @applytv phi pat == tgt@, binding only variables that appear in @pat@. +-- Unlike 'specmgu', a type variable on the right-hand side (@tgt@) is never +-- bound; if @tgt@ contains a free variable the match fails. This is the +-- correct operation for instance-head lookup: the instance type is the pattern +-- (may contain quantified variables) and the call-site type is the target +-- (must be fully concrete). +specmatch :: Ty -> Ty -> Either String TVSubst +specmatch (TyCon n ts) (TyCon n' ts') + | n == n' && length ts == length ts' = + matchsolve (zip ts ts') mempty +specmatch (TyVar v) t = varBind v t +specmatch t1 t2 = typesDoNotUnify t1 t2 + +matchsolve :: [(Ty, Ty)] -> TVSubst -> Either String TVSubst +matchsolve [] s = pure s +matchsolve ((pat, tgt) : rest) s = + do + s1 <- specmatch (applytv s pat) tgt + s2 <- matchsolve rest s1 + pure (s2 <> s1) + varBind :: (MonadError String m) => Tyvar -> Ty -> m TVSubst varBind v t | t == TyVar v = return mempty diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs index 4f3ad739..5030b57d 100644 --- a/src/Solcore/Frontend/TypeInference/TcStmt.hs +++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs @@ -775,6 +775,20 @@ elabFunDef isPub vs sig bdy (Forall _ (pinf :=> tinf)) ann@(Forall _ (pann :=> t -- mappings for phantom type variables (those absent from the function type). -- Returns new (annotation_meta -> body_meta) bindings for phantom variables, -- then restores the global substitution to its state on entry. +-- +-- Soundness: it is correct for this function to leave some phantom variables +-- without a binding. A variable like rep2 in +-- forall a b rep1 rep2 . a:Tag(rep1), b:Tag(rep2) => f : a -> b -> rep1 +-- never appears in the function body, so type-checking the body produces no +-- inferred constraint that mentions it; the returned delta simply says nothing +-- about rep2. This is safe because the specialiser resolves phantom variables +-- later, at each concrete call site: when b is instantiated to TypeB, instance +-- resolution against TypeB:Tag(TagB) immediately yields rep2 = TagB without +-- any information from this phase. +-- What would be unsound is a spurious unification of distinct type variables +-- (e.g. a ≡ b) produced by mismatched predicate pairing, because that would +-- corrupt the elaborated function signature and make specialisation impossible. +-- The guards in phantomMatchingPreds prevent exactly that. findPhantomPredBindings :: [Pred] -> [Pred] -> TcM [(MetaTv, Ty)] findPhantomPredBindings pann pinf = do s0 <- getSubst @@ -795,10 +809,12 @@ findPhantomPredBindings pann pinf = do phantomMatchingPreds :: [MetaTv] -> [Pred] -> [Pred] -> [(Pred, Pred)] phantomMatchingPreds dom_s0 pann pinf = [ (pa, pi_) - | pa@(InCls cls _ _) <- pann, - pi_@(InCls cls' _ _) <- pinf, + | pa@(InCls cls mt_a _) <- pann, + hasPhantomMeta pa, -- skip annotation preds already fully resolved in s0 + pi_@(InCls cls' mt_i _) <- pinf, cls == cls', - hasPhantomMeta pi_ + hasPhantomMeta pi_, + mt_a == mt_i -- self-types must agree to avoid cross-pairing same-class constraints ] where hasPhantomMeta (InCls _ mt exts) = any (`notElem` dom_s0) (mv mt `union` mv exts) diff --git a/test/Cases.hs b/test/Cases.hs index caf2b17c..c77e1aff 100644 --- a/test/Cases.hs +++ b/test/Cases.hs @@ -309,6 +309,8 @@ cases = runTestExpectingFailure "DupFun.solc" caseFolder, runTestForFile "EitherModule.solc" caseFolder, runTestForFile "empty-asm.solc" caseFolder, + runTestForFile "encoder.solc" caseFolder, + runTestForFile "encoder1.solc" caseFolder, runTestExpectingFailure "Enum.solc" caseFolder, runTestExpectingFailure "Eq.solc" caseFolder, runTestForFile "EqQual.solc" caseFolder, @@ -358,6 +360,11 @@ cases = runTestForFile "Memory2.solc" caseFolder, runTestExpectingFailure "missing-instance.solc" caseFolder, runTestForFile "modifier.solc" caseFolder, + runTestForFile "mptc-both-templates.solc" caseFolder, + runTestForFile "mptc-guard-extras-concrete.solc" caseFolder, + runTestForFile "mptc-multi-instance.solc" caseFolder, + runTestForFile "mptc-template-a-only.solc" caseFolder, + runTestForFile "mptc-template-b-only.solc" caseFolder, runTestForFile "monomorphic-require.solc" caseFolder, runTestForFile "morefun.solc" caseFolder, runTestForFile "Mutuals.solc" caseFolder, @@ -421,6 +428,7 @@ cases = runTestExpectingFailure "synonym-long-cycle.solc" caseFolder, runTestExpectingFailure "synonym-arity-mismatch.solc" caseFolder, runTestExpectingFailure "signature.solc" caseFolder, + runTestExpectingFailure "spec-fail-ungrounded.solc" caseFolder, runTestExpectingFailure "SillyReturn.solc" caseFolder, runTestExpectingFailure "SimpleInvoke.solc" caseFolder, runTestExpectingFailure "string-const.solc" caseFolder, diff --git a/test/examples/cases/encoder.solc b/test/examples/cases/encoder.solc new file mode 100644 index 00000000..bc470ddd --- /dev/null +++ b/test/examples/cases/encoder.solc @@ -0,0 +1,35 @@ +data TagA = TagA(word); +data TagB = TagB(word); + +forall self rep. +class self:Tag(rep) { + function getTag(x:self) -> rep; +} + +data TypeA = TypeA(word); +instance TypeA:Tag(TagA) { + function getTag(x:TypeA) -> TagA { + match x { | TypeA(w) => return TagA(w); } + } +} + +data TypeB = TypeB(word); +instance TypeB:Tag(TagB) { + function getTag(x:TypeB) -> TagB { + match x { | TypeB(w) => return TagB(w); } + } +} + +forall a b rep1 rep2 . a:Tag(rep1), b:Tag(rep2) => +function tagFirst(x:a, y:b) -> rep1 { + return Tag.getTag(x); +} + +contract C { + constructor() {} + + public function main() -> word { + let r : TagA = tagFirst(TypeA(42), TypeB(7)); + match r { | TagA(w) => return w; } + } +} diff --git a/test/examples/cases/encoder1.solc b/test/examples/cases/encoder1.solc new file mode 100644 index 00000000..ac418562 --- /dev/null +++ b/test/examples/cases/encoder1.solc @@ -0,0 +1,26 @@ +import std.{*}; + +forall self rep. +class self:Encoder(rep) { + function encode(x:self, hint:word) -> rep; +} + +data Foo = Foo(word); +instance Foo:Encoder(word) { + function encode(x:Foo, hint:word) -> word { + match x { | Foo(w) => return w; } + } +} + +forall a rep . a:Encoder(rep) => +function encodeAndDiscard(x:a) -> () { + let enc : rep = Encoder.encode(x, 0); + return (); +} + +contract C { + public function main() -> word { + encodeAndDiscard(Foo(42)); + return 0; + } +} diff --git a/test/examples/cases/mptc-both-templates.solc b/test/examples/cases/mptc-both-templates.solc new file mode 100644 index 00000000..222c102a --- /dev/null +++ b/test/examples/cases/mptc-both-templates.solc @@ -0,0 +1,34 @@ +// Tests that both Template A and Template B fire when the class has methods in +// both directions. Both should discover the same binding rep=word; the second +// application is idempotent (extSpSubst with the same binding is a no-op). + +data Box = Box(word); + +forall self rep. +class self:Convert(rep) { + function toRep(x:self) -> rep; + function fromRep(x:rep) -> self; +} + +instance Box:Convert(word) { + function toRep(x:Box) -> word { + match x { | Box(w) => return w; } + } + function fromRep(x:word) -> Box { + return Box(x); + } +} + +forall a rep . a:Convert(rep) => +function roundtrip(x:a) -> a { + let r : rep = Convert.toRep(x); + return Convert.fromRep(r); +} + +contract C { + constructor() {} + public function main() -> word { + let b : Box = roundtrip(Box(99)); + match b { | Box(w) => return w; } + } +} diff --git a/test/examples/cases/mptc-guard-extras-concrete.solc b/test/examples/cases/mptc-guard-extras-concrete.solc new file mode 100644 index 00000000..588af17f --- /dev/null +++ b/test/examples/cases/mptc-guard-extras-concrete.solc @@ -0,0 +1,29 @@ +// Tests the guard in resolveMPTCFromPreds that skips tryResolveMPTC when all +// extras are already fully concrete. Here rep is written as the concrete type +// `word` directly in the constraint, so freetv extras = [] and the function +// compiles through normal type inference without phantom variable discovery. + +data Box = Box(word); + +forall self rep. +class self:Unbox(rep) { + function unbox(x:self) -> rep; +} + +instance Box:Unbox(word) { + function unbox(x:Box) -> word { + match x { | Box(w) => return w; } + } +} + +forall a . a:Unbox(word) => +function extractWord(x:a) -> word { + return Unbox.unbox(x); +} + +contract C { + constructor() {} + public function main() -> word { + return extractWord(Box(42)); + } +} diff --git a/test/examples/cases/mptc-multi-instance.solc b/test/examples/cases/mptc-multi-instance.solc new file mode 100644 index 00000000..20d74d23 --- /dev/null +++ b/test/examples/cases/mptc-multi-instance.solc @@ -0,0 +1,41 @@ +// Tests that tryResolveMPTC selects the correct instance when multiple instances +// of the same class are registered in the resolution table. +// For getTag(Foo(1)): specmgu (Bar -> RepBar) (Foo -> freshV) fails (Bar != Foo), +// so only the Foo entry fires and rep is resolved to RepFoo. +// Similarly for getTag(Bar(2)) rep resolves to RepBar. + +data Foo = Foo(word); +data Bar = Bar(word); +data RepFoo = RepFoo(word); +data RepBar = RepBar(word); + +forall self rep. +class self:Tagged(rep) { + function tag(x:self) -> rep; +} + +instance Foo:Tagged(RepFoo) { + function tag(x:Foo) -> RepFoo { + match x { | Foo(w) => return RepFoo(w); } + } +} + +instance Bar:Tagged(RepBar) { + function tag(x:Bar) -> RepBar { + match x { | Bar(w) => return RepBar(w); } + } +} + +forall a rep . a:Tagged(rep) => +function getTag(x:a) -> rep { + return Tagged.tag(x); +} + +contract C { + constructor() {} + public function main() -> word { + let rf : RepFoo = getTag(Foo(1)); + let rb : RepBar = getTag(Bar(2)); + match rf { | RepFoo(w) => return w; } + } +} diff --git a/test/examples/cases/mptc-template-a-only.solc b/test/examples/cases/mptc-template-a-only.solc new file mode 100644 index 00000000..c42458eb --- /dev/null +++ b/test/examples/cases/mptc-template-a-only.solc @@ -0,0 +1,29 @@ +// Tests tryResolveMPTC Template A path. +// The class has only a method of the form (self -> rep), so Template B cannot +// fire. The specialiser must discover rep=word solely via Template A: +// specmgu (Box -> word) (Box -> freshV) => freshV = word => rep = word + +data Box = Box(word); + +forall self rep. +class self:Unbox(rep) { + function unbox(x:self) -> rep; +} + +instance Box:Unbox(word) { + function unbox(x:Box) -> word { + match x { | Box(w) => return w; } + } +} + +forall a rep . a:Unbox(rep) => +function extract(x:a) -> rep { + return Unbox.unbox(x); +} + +contract C { + constructor() {} + public function main() -> word { + return extract(Box(42)); + } +} diff --git a/test/examples/cases/mptc-template-b-only.solc b/test/examples/cases/mptc-template-b-only.solc new file mode 100644 index 00000000..07ac91c8 --- /dev/null +++ b/test/examples/cases/mptc-template-b-only.solc @@ -0,0 +1,31 @@ +// Tests tryResolveMPTC Template B path. +// The class has only a method of the form (rep -> self), so Template A cannot +// fire. The specialiser must discover rep=word solely via Template B: +// specmgu (word -> Box) (freshV -> Box) => freshV = word => rep = word +// The `hint:a` argument makes a=Box concrete at the call site. + +data Box = Box(word); + +forall self rep. +class self:Rebox(rep) { + function rebox(x:rep) -> self; +} + +instance Box:Rebox(word) { + function rebox(x:word) -> Box { + return Box(x); + } +} + +forall a rep . a:Rebox(rep) => +function rewrap(val:rep, hint:a) -> a { + return Rebox.rebox(val); +} + +contract C { + constructor() {} + public function main() -> word { + let b : Box = rewrap(7, Box(0)); + match b { | Box(w) => return w; } + } +} diff --git a/test/examples/cases/spec-fail-ungrounded.solc b/test/examples/cases/spec-fail-ungrounded.solc new file mode 100644 index 00000000..dde3745a --- /dev/null +++ b/test/examples/cases/spec-fail-ungrounded.solc @@ -0,0 +1,29 @@ +// Specialiser rejects this program even though the type checker accepts it. +// +// abort_ : word -> a has a polymorphic return type (it diverges). +// sink_ : b -> word accepts any argument and discards it. +// +// At the call sink_(abort_(0)) the intermediate type 'a' (= 'b') is never +// pinned to a concrete type: +// - The type checker is satisfied because a type 'a' EXISTS that makes the +// program consistent (any type works); the overall expression has type word. +// - The specialiser needs a CONCRETE 'a' to emit code for abort_. It finds +// no constraint, no instance, and no return-type context to fix 'a', so +// ensureClosed reports a free type variable and aborts. + +forall a. +function abort_(x:word) -> a { + return abort_(x); +} + +forall b. +function sink_(y:b) -> word { + return 0; +} + +contract C { + constructor() {} + public function main() -> word { + return sink_(abort_(0)); + } +} From 4c1a05eff6a5923c12856ad23b8bc889fc4081ce Mon Sep 17 00:00:00 2001 From: rodrigogribeiro Date: Tue, 16 Jun 2026 16:52:45 -0300 Subject: [PATCH 05/10] Adding more tests --- sol-core.cabal | 1 + src/Solcore/Backend/Specialise.hs | 20 ++- test/Cases.hs | 3 + test/Main.hs | 4 +- test/SpecialiseTests.hs | 152 ++++++++++++++++++ test/examples/cases/mptc-chain-phantom.solc | 51 ++++++ test/examples/cases/mptc-nop-mainty-free.solc | 39 +++++ .../examples/cases/mptc-partial-instance.solc | 37 +++++ 8 files changed, 305 insertions(+), 2 deletions(-) create mode 100644 test/SpecialiseTests.hs create mode 100644 test/examples/cases/mptc-chain-phantom.solc create mode 100644 test/examples/cases/mptc-nop-mainty-free.solc create mode 100644 test/examples/cases/mptc-partial-instance.solc diff --git a/sol-core.cabal b/sol-core.cabal index 07eb320a..1f4565cc 100644 --- a/sol-core.cabal +++ b/sol-core.cabal @@ -174,6 +174,7 @@ test-suite sol-core-tests HullCases MatchCompilerTests ModuleTypeCheckTests + SpecialiseTests YulEvalTests ParserTests diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs index 0484007b..ec903e51 100644 --- a/src/Solcore/Backend/Specialise.hs +++ b/src/Solcore/Backend/Specialise.hs @@ -1,4 +1,13 @@ -module Solcore.Backend.Specialise (specialiseCompUnit, typeOfTcExp) where +module Solcore.Backend.Specialise + ( -- core API + specialiseCompUnit + , typeOfTcExp + -- testing API + , TVSubst (..) + , emptyTVSubst + , (|->) + , runResolveMPTCTest + ) where -- \* Specialisation -- Create specialised versions of polymorphic and overloaded functions. @@ -502,6 +511,15 @@ resolveMPTCFromPreds preds = do tryResolveMPTC clsName mainTy' extras' _ -> return () +-- | Testing entry point: run resolveMPTCFromPreds in an isolated SM environment. +-- Sets the initial substitution to @s0@, runs @resolveMPTCFromPreds preds@, and +-- returns the resulting substitution. The @TcEnv@ supplies the instance table. +runResolveMPTCTest :: TcEnv -> TVSubst -> [Pred] -> IO TVSubst +runResolveMPTCTest env s0 preds = runSM False env $ do + putSpSubst s0 + resolveMPTCFromPreds preds + getSpSubst + -- tryResolveMPTC deduces concrete types for the extra parameters of a -- multi-parameter type class (MPTC) constraint when the "self" (main) type is -- already fully concrete but some extra parameters are still free type variables. diff --git a/test/Cases.hs b/test/Cases.hs index c77e1aff..dc50b1eb 100644 --- a/test/Cases.hs +++ b/test/Cases.hs @@ -361,8 +361,11 @@ cases = runTestExpectingFailure "missing-instance.solc" caseFolder, runTestForFile "modifier.solc" caseFolder, runTestForFile "mptc-both-templates.solc" caseFolder, + runTestForFile "mptc-chain-phantom.solc" caseFolder, runTestForFile "mptc-guard-extras-concrete.solc" caseFolder, runTestForFile "mptc-multi-instance.solc" caseFolder, + runTestForFile "mptc-nop-mainty-free.solc" caseFolder, + runTestForFile "mptc-partial-instance.solc" caseFolder, runTestForFile "mptc-template-a-only.solc" caseFolder, runTestForFile "mptc-template-b-only.solc" caseFolder, runTestForFile "monomorphic-require.solc" caseFolder, diff --git a/test/Main.hs b/test/Main.hs index d04a27e2..84b29775 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -5,6 +5,7 @@ import HullCases import MatchCompilerTests import ModuleTypeCheckTests import ParserTests +import SpecialiseTests import Test.Tasty import YulEvalTests @@ -27,5 +28,6 @@ tests = dispatches, matchTests, yulEvalTests, - hullTests + hullTests, + specialiseTests ] diff --git a/test/SpecialiseTests.hs b/test/SpecialiseTests.hs new file mode 100644 index 00000000..aa2f0608 --- /dev/null +++ b/test/SpecialiseTests.hs @@ -0,0 +1,152 @@ +module SpecialiseTests (specialiseTests) where + +import Data.Map.Strict qualified as Map +import Solcore.Backend.Specialise (TVSubst (..), emptyTVSubst, runResolveMPTCTest, (|->)) +import Solcore.Frontend.Syntax.Name (Name (..)) +import Solcore.Frontend.Syntax.Ty (Pred (..), Qual (..), Ty (..), Tyvar (..)) +import Solcore.Frontend.TypeInference.TcEnv (TcEnv (..), initTcEnv) +import Solcore.Pipeline.Options (stdOpt) +import Test.Tasty +import Test.Tasty.HUnit + +-- --------------------------------------------------------------------------- +-- Helpers + +word :: Ty +word = TyCon (Name "word") [] + +foo :: Ty +foo = TyCon (Name "Foo") [] + +bar :: Ty +bar = TyCon (Name "Bar") [] + +bool :: Ty +bool = TyCon (Name "bool") [] + +tv :: String -> Ty +tv s = TyVar (TVar (Name s)) + +inCls :: String -> Ty -> [Ty] -> Pred +inCls cls main extras = InCls (Name cls) main extras + +-- | Build a test TcEnv whose instance table is exactly the given mapping. +-- The rest of the environment uses stdOpt defaults. +mkTestEnv :: [(Name, [Qual Pred])] -> TcEnv +mkTestEnv insts = (initTcEnv stdOpt) {instEnv = Map.fromList insts} + +-- | Check whether (v, t) appears in a substitution. +hasBind :: Tyvar -> Ty -> TVSubst -> Bool +hasBind v t s = (v, t) `elem` unTVSubst s + +-- --------------------------------------------------------------------------- +-- Test suite + +specialiseTests :: TestTree +specialiseTests = + testGroup + "Specialise.resolveMPTCsFromPreds" + [ testBind + , testNopAFreeMain + , testNopBExtrasAlreadyConcrete + , testWrongInstance + , testPartialInstance + , testMultiExtraOnlyFreeOneGetsResolved + ] + +-- --------------------------------------------------------------------------- +-- BIND path: the happy path + +-- | When mainTy is concrete and at least one extra is a free TyVar, +-- tryResolveMPTC should look up the matching instance and bind the extra. +testBind :: TestTree +testBind = testCase "BIND: concrete mainTy + free extra → binds extra to instance value" $ do + let inst = [] :=> inCls "Encoder" foo [word] + env = mkTestEnv [(Name "Encoder", [inst])] + s0 = TVar (Name "a") |-> foo + pred_ = inCls "Encoder" foo [tv "rep"] + s1 <- runResolveMPTCTest env s0 [pred_] + assertBool "rep should be bound to word after resolution" + (hasBind (TVar (Name "rep")) word s1) + +-- --------------------------------------------------------------------------- +-- NOP-A path: mainTy still free → guard fails, nothing happens + +-- | When mainTy has free type variables the guard +-- null (freetv mainTy') is False and tryResolveMPTC is NOT called. +testNopAFreeMain :: TestTree +testNopAFreeMain = testCase "NOP-A: free mainTy → does nothing" $ do + let inst = [] :=> inCls "Encoder" foo [word] + env = mkTestEnv [(Name "Encoder", [inst])] + s0 = emptyTVSubst + pred_ = inCls "Encoder" (tv "a") [tv "rep"] -- 'a' is still free + s1 <- runResolveMPTCTest env s0 [pred_] + assertEqual "substitution should be unchanged when mainTy is free" s0 s1 + +-- --------------------------------------------------------------------------- +-- NOP-B path: extras already concrete after applying the SM substitution + +-- | When the SM substitution already maps every extra to a concrete type, +-- any (not . null . freetv) extras' is False and tryResolveMPTC is NOT called. +testNopBExtrasAlreadyConcrete :: TestTree +testNopBExtrasAlreadyConcrete = testCase "NOP-B: extras already concrete in SM subst → does nothing" $ do + let inst = [] :=> inCls "Encoder" foo [word] + env = mkTestEnv [(Name "Encoder", [inst])] + s0 = TVar (Name "a") |-> foo <> TVar (Name "rep") |-> word + pred_ = inCls "Encoder" foo [tv "rep"] -- 'rep' is free in pred but bound in s0 + s1 <- runResolveMPTCTest env s0 [pred_] + -- s0 applied to [TyVar rep] gives [word] (concrete) → guard is false → s1 == s0 + assertEqual "substitution should be unchanged when all extras are already concrete" s0 s1 + +-- --------------------------------------------------------------------------- +-- WRONG-INSTANCE path: no matching instance → nothing changes + +-- | When the instance table only contains an instance for Bar (not Foo), +-- specmatch fails for every instance and no binding is added. +testWrongInstance :: TestTree +testWrongInstance = testCase "WRONG-INSTANCE: no matching instance → does nothing" $ do + let inst = [] :=> inCls "Encoder" bar [bool] -- instance for Bar, not Foo + env = mkTestEnv [(Name "Encoder", [inst])] + s0 = emptyTVSubst + pred_ = inCls "Encoder" foo [tv "rep"] + s1 <- runResolveMPTCTest env s0 [pred_] + assertEqual "substitution should be unchanged when no instance matches" s0 s1 + +-- --------------------------------------------------------------------------- +-- PARTIAL path: matching instance has free vars in its extra → skipped + +-- | Instance head Foo : C(x, word) has a free type variable x. +-- After matching Foo against the concrete mainTy we get an empty substitution, +-- so concreteExtras = [TyVar x, word]. The guard +-- all (null . freetv) concreteExtras +-- is False → the instance is skipped and nothing is bound. +testPartialInstance :: TestTree +testPartialInstance = testCase "PARTIAL: instance extras have free vars → skipped" $ do + let instExtra1 = TyVar (TVar (Name "x")) -- free variable inside instance + instExtra2 = word + inst = [] :=> inCls "C" foo [instExtra1, instExtra2] + env = mkTestEnv [(Name "C", [inst])] + s0 = emptyTVSubst + pred_ = inCls "C" foo [tv "r1", tv "r2"] + s1 <- runResolveMPTCTest env s0 [pred_] + assertEqual "substitution should be unchanged when instance extras have free vars" s0 s1 + +-- --------------------------------------------------------------------------- +-- Multi-extra: only the free extra gets resolved, the concrete one is untouched + +-- | Pred has two extras: one already concrete (word), one free (rep). +-- The guard fires because at least one extra is free. +-- tryResolveMPTC should bind rep = bool from the instance. +testMultiExtraOnlyFreeOneGetsResolved :: TestTree +testMultiExtraOnlyFreeOneGetsResolved = + testCase "MULTI-EXTRA: only the free extra is bound, concrete one is left alone" $ do + let inst = [] :=> inCls "C2" foo [word, bool] + env = mkTestEnv [(Name "C2", [inst])] + s0 = emptyTVSubst + pred_ = inCls "C2" foo [word, tv "rep"] -- word is concrete, rep is free + s1 <- runResolveMPTCTest env s0 [pred_] + assertBool "rep should be bound to bool after resolution" + (hasBind (TVar (Name "rep")) bool s1) + -- word is already concrete in the pred, specmatch (word, word) = Right {} → no change + assertBool "no spurious bindings for the already-concrete extra" + (not (hasBind (TVar (Name "word")) bool s1)) diff --git a/test/examples/cases/mptc-chain-phantom.solc b/test/examples/cases/mptc-chain-phantom.solc new file mode 100644 index 00000000..f5822c36 --- /dev/null +++ b/test/examples/cases/mptc-chain-phantom.solc @@ -0,0 +1,51 @@ +// Tests resolveMPTCsFromPreds in a "chain" scenario: +// - f has phantom rep in its monotype (Foo -> ()) +// - inside f, encode returns a value of type rep +// - that value is passed to sink whose monotype is rep -> () +// +// Without resolveMPTCsFromPreds the SM substitution lacks rep=word when +// sink's specialisation name is being built, which would produce sink$rep +// (wrong) instead of sink$word (correct). + +data Foo = Foo(word); + +forall self rep. +class self:Encoder(rep) { + function encode(x:self, hint:word) -> rep; +} + +forall rep r. +class rep:Sink(r) { + function sink(x:rep) -> (); +} + +instance Foo:Encoder(word) { + function encode(x:Foo, hint:word) -> word { + match x { | Foo(v) => return v; } + } +} + +instance word:Sink(word) { + function sink(x:word) -> () { + return (); + } +} + +// phantom rep: rep does not appear in f's argument or return type. +// Inside the body, encode returns rep and sink consumes rep. +// resolveMPTCsFromPreds must bind rep=word so that sink specialises +// to sink$word (not sink$rep). +forall a rep . a:Encoder(rep), rep:Sink(word) => +function f(x:a) -> () { + let r : rep = Encoder.encode(x, 0); + Sink.sink(r); + return (); +} + +contract C { + constructor() {} + public function main() -> word { + f(Foo(42)); + return 0; + } +} diff --git a/test/examples/cases/mptc-nop-mainty-free.solc b/test/examples/cases/mptc-nop-mainty-free.solc new file mode 100644 index 00000000..0ddc08e2 --- /dev/null +++ b/test/examples/cases/mptc-nop-mainty-free.solc @@ -0,0 +1,39 @@ +// Documents the NOP-A guard in resolveMPTCsFromPreds. +// +// The guard `null (freetv mainTy')` is false when the main type variable +// is not yet bound in the SM substitution. This happens for higher-order +// polymorphic functions that are specialised from the outside. +// +// Here `mapEncode` is only ever called with a concrete `a=Foo`, so at every +// call site the SM substitution has a=Foo before the body is processed. +// However, if `mapEncode` were called with an unresolved type the guard +// would fire and tryResolveMPTC would be skipped. +// +// This is a compile-only test: it verifies that the NOP-A guard does NOT +// interfere with the normal specialisation of `mapEncode` when called +// from a concrete call site. + +data Foo = Foo(word); + +forall self rep. +class self:Encoder(rep) { + function encode(x:self, hint:word) -> rep; +} + +instance Foo:Encoder(word) { + function encode(x:Foo, hint:word) -> word { + match x { | Foo(v) => return v; } + } +} + +forall a rep. a:Encoder(rep) => +function extractVal(x:a) -> rep { + return Encoder.encode(x, 0); +} + +contract C { + constructor() {} + public function main() -> word { + return extractVal(Foo(7)); + } +} diff --git a/test/examples/cases/mptc-partial-instance.solc b/test/examples/cases/mptc-partial-instance.solc new file mode 100644 index 00000000..ac1f8743 --- /dev/null +++ b/test/examples/cases/mptc-partial-instance.solc @@ -0,0 +1,37 @@ +// Exercises the PARTIAL guard in tryResolveMPTC. +// +// The instance forall a b. instance Zero:Nth((a,b), a) has free type variables +// in its extras even after successfully matching Zero against the concrete main type. +// resolveMPTCsFromPreds detects this (concreteExtras still has free vars) and skips +// the instance, letting normal type inference determine the extra type instead. + +pragma no-coverage-condition Nth; + +data Zero; +data Succ(a); +data Proxy(a) = Proxy; + +forall a b c. class a:Nth(b, c) { + function nth(x:Proxy(a), y:b) -> c; +} + +forall a b. instance Zero:Nth((a,b), a) { + function nth(x:Proxy(Zero), y:(a,b)) -> a { + match y { | (a, b) => return a; } + } +} + +forall n a b c. n:Nth(b,c) => instance Succ(n):Nth((a,b), c) { + function nth(x:Proxy(Succ(n)), y:(a,b)) -> c { + match y { | (a, b) => return Nth.nth(Proxy : Proxy(n), b); } + } +} + +contract C { + constructor() {} + public function main() -> word { + let p : (word, word, word) = (1, 2, 3); + let x : word = Nth.nth(Proxy : Proxy(Zero), p); + return x; + } +} From d2103a78e6d4cef6079851e51a80a2166515759e Mon Sep 17 00:00:00 2001 From: rodrigogribeiro Date: Tue, 16 Jun 2026 19:25:28 -0300 Subject: [PATCH 06/10] Minor fixes on instance imports and adds more tests --- src/Solcore/Frontend/Module/Loader.hs | 2 + test/Cases.hs | 7 +- test/SpecialiseTests.hs | 338 ++++++++++++++---- test/examples/cases/abigeneric.solc | 127 +++++++ .../cases/bug-import-default-inst-shadow.solc | 32 ++ 5 files changed, 432 insertions(+), 74 deletions(-) create mode 100644 test/examples/cases/abigeneric.solc create mode 100644 test/examples/cases/bug-import-default-inst-shadow.solc diff --git a/src/Solcore/Frontend/Module/Loader.hs b/src/Solcore/Frontend/Module/Loader.hs index b9341b29..17c9b2f0 100644 --- a/src/Solcore/Frontend/Module/Loader.hs +++ b/src/Solcore/Frontend/Module/Loader.hs @@ -1880,9 +1880,11 @@ filterImportedInstanceConflicts localDecls = mapMaybe keepImportedDecl where localClassNames = concatMap topDeclClassNames localDecls + localInstanceHeads = [instanceDeclHeadKey inst | TInstDef inst <- localDecls] keepImportedDecl d@(TInstDef inst) | instName inst `elem` localClassNames = Nothing + | instanceDeclHeadKey inst `elem` localInstanceHeads = Nothing | otherwise = Just d keepImportedDecl d = Just d diff --git a/test/Cases.hs b/test/Cases.hs index dc50b1eb..83f875fa 100644 --- a/test/Cases.hs +++ b/test/Cases.hs @@ -251,7 +251,8 @@ cases :: TestTree cases = testGroup "Files for folder cases" - [ runTestForFile "Ackermann.solc" caseFolder, + [ runTestForFile "abigeneric.solc" caseFolder, + runTestForFile "Ackermann.solc" caseFolder, runTestForFile "Add1.solc" caseFolder, runTestExpectingFailure "add-moritz.solc" caseFolder, runTestForFile "another-subst.solc" caseFolder, @@ -515,7 +516,9 @@ cases = runTestExpectingFailure "class-return-type-miss.solc" caseFolder, runTestExpectingFailure "catenable-err.solc" caseFolder, runTestForFile "pars.solc" caseFolder, - runTestForFile "bug-rep-name-capture.solc" caseFolder + runTestForFile "bug-rep-name-capture.solc" caseFolder, + runTestForFile "bug-import-default-inst-shadow.solc" caseFolder, + runTestForFile "abigeneric.solc" caseFolder ] where caseFolder = "./test/examples/cases" diff --git a/test/SpecialiseTests.hs b/test/SpecialiseTests.hs index aa2f0608..62cac9d8 100644 --- a/test/SpecialiseTests.hs +++ b/test/SpecialiseTests.hs @@ -39,6 +39,10 @@ mkTestEnv insts = (initTcEnv stdOpt) {instEnv = Map.fromList insts} hasBind :: Tyvar -> Ty -> TVSubst -> Bool hasBind v t s = (v, t) `elem` unTVSubst s +-- | Check whether a given type variable name has any binding in the subst. +hasAnyBind :: String -> TVSubst -> Bool +hasAnyBind name s = any (\(v, _) -> v == TVar (Name name)) (unTVSubst s) + -- --------------------------------------------------------------------------- -- Test suite @@ -46,107 +50,297 @@ specialiseTests :: TestTree specialiseTests = testGroup "Specialise.resolveMPTCsFromPreds" - [ testBind - , testNopAFreeMain - , testNopBExtrasAlreadyConcrete - , testWrongInstance - , testPartialInstance - , testMultiExtraOnlyFreeOneGetsResolved + [ testBind, + testTwoBothPhantomExtras, + testNopAFreeMain, + testNopBIdempotent, + testWrongInstance, + testPartialInstance, + testMixedConcreteAndPhantomExtra, + testEmptyPredList, + testMultiplePreds, + testFirstWrongSecondBind, + testPhantomChainSnapshot, + testPhantomChainTwoCalls, + testUnknownClass, + testParameterisedMainTy ] -- --------------------------------------------------------------------------- --- BIND path: the happy path +-- BIND path: the core phantom-variable use case +-- +-- Setting: function forall a rep. a:Encoder(rep) => f(x:a) -> () +-- 'a' is visible — it appears in the argument type, so the call site +-- determines it: s0 = {a = Foo}. +-- 'rep' is phantom — it does NOT appear in the function's monotype (a -> ()), +-- so the call site gives no information about it. +-- resolveMPTCFromPreds must discover rep = word from the instance Foo:Encoder(word). --- | When mainTy is concrete and at least one extra is a free TyVar, --- tryResolveMPTC should look up the matching instance and bind the extra. testBind :: TestTree -testBind = testCase "BIND: concrete mainTy + free extra → binds extra to instance value" $ do - let inst = [] :=> inCls "Encoder" foo [word] - env = mkTestEnv [(Name "Encoder", [inst])] - s0 = TVar (Name "a") |-> foo - pred_ = inCls "Encoder" foo [tv "rep"] +testBind = testCase "BIND: phantom extra bound from matching instance" $ do + let inst = [] :=> inCls "Encoder" foo [word] + env = mkTestEnv [(Name "Encoder", [inst])] + s0 = TVar (Name "a") |-> foo -- only the visible param is in the subst + pred_ = inCls "Encoder" (tv "a") [tv "rep"] s1 <- runResolveMPTCTest env s0 [pred_] - assertBool "rep should be bound to word after resolution" - (hasBind (TVar (Name "rep")) word s1) + assertBool "rep should be bound to word" (hasBind (TVar (Name "rep")) word s1) + +-- --------------------------------------------------------------------------- +-- Two phantom extras — both free TyVars, both bound in one pass. +-- +-- Setting: forall a out1 out2. a:BiEnc(out1, out2) => f(x:a) -> () +-- Neither out1 nor out2 appears in the function type; both are phantom. +-- The single instance Foo:BiEnc(word, bool) pins both at once. + +testTwoBothPhantomExtras :: TestTree +testTwoBothPhantomExtras = + testCase "TWO-PHANTOM: two phantom extras both bound in one pass" $ do + let inst = [] :=> inCls "BiEnc" foo [word, bool] + env = mkTestEnv [(Name "BiEnc", [inst])] + s0 = TVar (Name "a") |-> foo + pred_ = inCls "BiEnc" (tv "a") [tv "out1", tv "out2"] + s1 <- runResolveMPTCTest env s0 [pred_] + assertBool "out1 should be bound to word" (hasBind (TVar (Name "out1")) word s1) + assertBool "out2 should be bound to bool" (hasBind (TVar (Name "out2")) bool s1) -- --------------------------------------------------------------------------- --- NOP-A path: mainTy still free → guard fails, nothing happens +-- NOP-A: main type still free → guard fails, nothing happens +-- +-- Setting: the specialiser hasn't yet determined which concrete type 'a' is, +-- so the pred's main type is still a free TyVar after applying the current subst. +-- Without knowing the concrete self type, we can't look up the right instance. --- | When mainTy has free type variables the guard --- null (freetv mainTy') is False and tryResolveMPTC is NOT called. testNopAFreeMain :: TestTree testNopAFreeMain = testCase "NOP-A: free mainTy → does nothing" $ do - let inst = [] :=> inCls "Encoder" foo [word] - env = mkTestEnv [(Name "Encoder", [inst])] - s0 = emptyTVSubst - pred_ = inCls "Encoder" (tv "a") [tv "rep"] -- 'a' is still free + let inst = [] :=> inCls "Encoder" foo [word] + env = mkTestEnv [(Name "Encoder", [inst])] + s0 = emptyTVSubst -- 'a' is not yet determined + pred_ = inCls "Encoder" (tv "a") [tv "rep"] s1 <- runResolveMPTCTest env s0 [pred_] - assertEqual "substitution should be unchanged when mainTy is free" s0 s1 + assertEqual "substitution unchanged when mainTy is free" s0 s1 -- --------------------------------------------------------------------------- --- NOP-B path: extras already concrete after applying the SM substitution +-- NOP-B: idempotency — phantom already bound in an earlier pass +-- +-- Setting: resolveMPTCFromPreds was already called once and bound rep=word. +-- A second call with the same preds and the updated subst must be a no-op: +-- the guard any (not . null . freetv) extras' is False because +-- applytv {a=Foo, rep=word} [TyVar rep] = [word] (all concrete). --- | When the SM substitution already maps every extra to a concrete type, --- any (not . null . freetv) extras' is False and tryResolveMPTC is NOT called. -testNopBExtrasAlreadyConcrete :: TestTree -testNopBExtrasAlreadyConcrete = testCase "NOP-B: extras already concrete in SM subst → does nothing" $ do - let inst = [] :=> inCls "Encoder" foo [word] - env = mkTestEnv [(Name "Encoder", [inst])] - s0 = TVar (Name "a") |-> foo <> TVar (Name "rep") |-> word - pred_ = inCls "Encoder" foo [tv "rep"] -- 'rep' is free in pred but bound in s0 +testNopBIdempotent :: TestTree +testNopBIdempotent = testCase "NOP-B: phantom already bound → idempotent, no change" $ do + let inst = [] :=> inCls "Encoder" foo [word] + env = mkTestEnv [(Name "Encoder", [inst])] + s0 = TVar (Name "a") |-> foo <> TVar (Name "rep") |-> word + pred_ = inCls "Encoder" (tv "a") [tv "rep"] s1 <- runResolveMPTCTest env s0 [pred_] - -- s0 applied to [TyVar rep] gives [word] (concrete) → guard is false → s1 == s0 - assertEqual "substitution should be unchanged when all extras are already concrete" s0 s1 + assertEqual "substitution unchanged when phantom is already resolved" s0 s1 -- --------------------------------------------------------------------------- --- WRONG-INSTANCE path: no matching instance → nothing changes +-- WRONG-INSTANCE: no instance for the concrete self type → phantom stays free --- | When the instance table only contains an instance for Bar (not Foo), --- specmatch fails for every instance and no binding is added. testWrongInstance :: TestTree -testWrongInstance = testCase "WRONG-INSTANCE: no matching instance → does nothing" $ do - let inst = [] :=> inCls "Encoder" bar [bool] -- instance for Bar, not Foo - env = mkTestEnv [(Name "Encoder", [inst])] - s0 = emptyTVSubst - pred_ = inCls "Encoder" foo [tv "rep"] +testWrongInstance = testCase "WRONG-INSTANCE: no matching instance → phantom stays free" $ do + let inst = [] :=> inCls "Encoder" bar [bool] -- instance for Bar, not Foo + env = mkTestEnv [(Name "Encoder", [inst])] + s0 = TVar (Name "a") |-> foo + pred_ = inCls "Encoder" (tv "a") [tv "rep"] s1 <- runResolveMPTCTest env s0 [pred_] - assertEqual "substitution should be unchanged when no instance matches" s0 s1 + assertBool + "rep should remain unbound when no instance matches" + (not (hasAnyBind "rep" s1)) -- --------------------------------------------------------------------------- --- PARTIAL path: matching instance has free vars in its extra → skipped +-- PARTIAL: the matching instance is parametric in its extra → skipped +-- +-- Instance Foo : C(x, word) has a free type variable x. +-- After specmatch succeeds for Foo, concreteExtras = [TyVar x, word] — x is still +-- free. The guard all (null . freetv) concreteExtras fails → skipped. +-- We cannot deduce a unique concrete type for r1. --- | Instance head Foo : C(x, word) has a free type variable x. --- After matching Foo against the concrete mainTy we get an empty substitution, --- so concreteExtras = [TyVar x, word]. The guard --- all (null . freetv) concreteExtras --- is False → the instance is skipped and nothing is bound. testPartialInstance :: TestTree -testPartialInstance = testCase "PARTIAL: instance extras have free vars → skipped" $ do - let instExtra1 = TyVar (TVar (Name "x")) -- free variable inside instance +testPartialInstance = testCase "PARTIAL: parametric instance skipped, phantom stays free" $ do + let instExtra1 = TyVar (TVar (Name "x")) instExtra2 = word - inst = [] :=> inCls "C" foo [instExtra1, instExtra2] - env = mkTestEnv [(Name "C", [inst])] - s0 = emptyTVSubst - pred_ = inCls "C" foo [tv "r1", tv "r2"] + inst = [] :=> inCls "C" foo [instExtra1, instExtra2] + env = mkTestEnv [(Name "C", [inst])] + s0 = TVar (Name "a") |-> foo + pred_ = inCls "C" (tv "a") [tv "r1", tv "r2"] s1 <- runResolveMPTCTest env s0 [pred_] - assertEqual "substitution should be unchanged when instance extras have free vars" s0 s1 + assertBool + "r1 should remain unbound (parametric instance skipped)" + (not (hasAnyBind "r1" s1)) + assertBool + "r2 should remain unbound (whole instance skipped)" + (not (hasAnyBind "r2" s1)) -- --------------------------------------------------------------------------- --- Multi-extra: only the free extra gets resolved, the concrete one is untouched +-- Mixed: one extra fixed in the signature, one phantom +-- +-- Setting: forall a rep. a:BiEnc(word, rep) => f(x:a) -> () +-- The first extra is the concrete type 'word' written directly in the function's +-- constraint — it is not a phantom variable. Only 'rep' is phantom. +-- The guard fires because extras' = [word, TyVar rep] has a free element. +-- The instance Foo:BiEnc(word, bool) provides rep = bool. --- | Pred has two extras: one already concrete (word), one free (rep). --- The guard fires because at least one extra is free. --- tryResolveMPTC should bind rep = bool from the instance. -testMultiExtraOnlyFreeOneGetsResolved :: TestTree -testMultiExtraOnlyFreeOneGetsResolved = - testCase "MULTI-EXTRA: only the free extra is bound, concrete one is left alone" $ do - let inst = [] :=> inCls "C2" foo [word, bool] - env = mkTestEnv [(Name "C2", [inst])] - s0 = emptyTVSubst - pred_ = inCls "C2" foo [word, tv "rep"] -- word is concrete, rep is free +testMixedConcreteAndPhantomExtra :: TestTree +testMixedConcreteAndPhantomExtra = + testCase "MIXED-EXTRA: fixed extra + phantom extra → only phantom bound" $ do + let inst = [] :=> inCls "BiEnc" foo [word, bool] + env = mkTestEnv [(Name "BiEnc", [inst])] + s0 = TVar (Name "a") |-> foo + pred_ = inCls "BiEnc" (tv "a") [word, tv "rep"] s1 <- runResolveMPTCTest env s0 [pred_] - assertBool "rep should be bound to bool after resolution" - (hasBind (TVar (Name "rep")) bool s1) - -- word is already concrete in the pred, specmatch (word, word) = Right {} → no change - assertBool "no spurious bindings for the already-concrete extra" + assertBool "rep should be bound to bool" (hasBind (TVar (Name "rep")) bool s1) + assertBool + "no spurious new binding introduced for word" (not (hasBind (TVar (Name "word")) bool s1)) + +-- --------------------------------------------------------------------------- +-- Empty pred list: trivial no-op + +testEmptyPredList :: TestTree +testEmptyPredList = testCase "EMPTY: empty pred list → substitution unchanged" $ do + let env = mkTestEnv [] + s0 = TVar (Name "a") |-> foo + s1 <- runResolveMPTCTest env s0 [] + assertEqual "empty pred list leaves substitution unchanged" s0 s1 + +-- --------------------------------------------------------------------------- +-- Multiple preds: each phantom is bound from its own class +-- +-- Setting: forall a b rep out. a:Encoder(rep), b:Decoder(out) => f(x:a, y:b) -> () +-- a and b are visible; rep and out are both phantom. +-- After the call site pins a=Foo and b=Bar, one pass resolves both phantoms. + +testMultiplePreds :: TestTree +testMultiplePreds = testCase "MULTI-PRED: independent phantoms across two preds both bound" $ do + let instE = [] :=> inCls "Encoder" foo [word] + instD = [] :=> inCls "Decoder" bar [bool] + env = mkTestEnv [(Name "Encoder", [instE]), (Name "Decoder", [instD])] + s0 = TVar (Name "a") |-> foo <> TVar (Name "b") |-> bar + preds = + [ inCls "Encoder" (tv "a") [tv "rep"], + inCls "Decoder" (tv "b") [tv "out"] + ] + s1 <- runResolveMPTCTest env s0 preds + assertBool "rep should be bound to word" (hasBind (TVar (Name "rep")) word s1) + assertBool "out should be bound to bool" (hasBind (TVar (Name "out")) bool s1) + +-- --------------------------------------------------------------------------- +-- Instance list iteration: first instance wrong, second correct +-- +-- The class has two registered instances. The first does not match the concrete +-- self type so specmatch returns Left and it is skipped. The second matches and +-- the phantom extra is bound. + +testFirstWrongSecondBind :: TestTree +testFirstWrongSecondBind = + testCase "ITERATE: first instance wrong, second matches → phantom bound" $ do + let instWrong = [] :=> inCls "Tagged" bar [bool] -- Bar ≠ Foo + instRight = [] :=> inCls "Tagged" foo [word] -- Foo = Foo ✓ + env = mkTestEnv [(Name "Tagged", [instWrong, instRight])] + s0 = TVar (Name "a") |-> foo + pred_ = inCls "Tagged" (tv "a") [tv "rep"] + s1 <- runResolveMPTCTest env s0 [pred_] + assertBool + "rep should be bound to word by the second instance" + (hasBind (TVar (Name "rep")) word s1) + +-- --------------------------------------------------------------------------- +-- Phantom chain — snapshot behaviour +-- +-- Setting: forall a rep out. a:Encoder(rep), rep:Sink(out) => f(x:a) -> () +-- 'a' is visible; 'rep' and 'out' are BOTH phantom. +-- 'rep' is the phantom extra of the first pred AND the phantom main type of +-- the second pred — they form a dependency chain. +-- +-- resolveMPTCFromPreds captures a SNAPSHOT of the SM substitution at entry and +-- uses it for ALL preds in the same call. Processing order: +-- +-- pred1 Encoder (TyVar a) [TyVar rep] +-- snapshot applies: mainTy' = Foo (concrete) → BIND: rep = word +-- SM subst updated to {a=Foo, rep=word} +-- +-- pred2 Sink (TyVar rep) [TyVar out] +-- snapshot still = {a=Foo} (captured before the loop) +-- mainTy' = applytv {a=Foo} (TyVar rep) = TyVar rep (still free!) +-- NOP-A fires → out stays unbound +-- +-- Consequence: a single call resolves rep but NOT out. + +testPhantomChainSnapshot :: TestTree +testPhantomChainSnapshot = + testCase "CHAIN-SNAPSHOT: chained phantom not resolved in one pass (snapshot)" $ do + let instEnc = [] :=> inCls "Encoder" foo [word] + instSink = [] :=> inCls "Sink" word [bool] + env = mkTestEnv [(Name "Encoder", [instEnc]), (Name "Sink", [instSink])] + s0 = TVar (Name "a") |-> foo + preds = + [ inCls "Encoder" (tv "a") [tv "rep"], + inCls "Sink" (tv "rep") [tv "out"] + ] + s1 <- runResolveMPTCTest env s0 preds + assertBool "rep resolved from pred1" (hasBind (TVar (Name "rep")) word s1) + assertBool + "out NOT resolved in one pass (snapshot does not see rep=word)" + (not (hasAnyBind "out" s1)) + +-- --------------------------------------------------------------------------- +-- Phantom chain — two calls resolve the full chain +-- +-- A second call with the updated substitution now sees rep=word in the snapshot, +-- so pred2's mainTy' becomes 'word' (concrete) and out = bool is bound. + +testPhantomChainTwoCalls :: TestTree +testPhantomChainTwoCalls = + testCase "CHAIN-TWO-CALLS: second pass resolves the chained phantom" $ do + let instEnc = [] :=> inCls "Encoder" foo [word] + instSink = [] :=> inCls "Sink" word [bool] + env = mkTestEnv [(Name "Encoder", [instEnc]), (Name "Sink", [instSink])] + s0 = TVar (Name "a") |-> foo + preds = + [ inCls "Encoder" (tv "a") [tv "rep"], + inCls "Sink" (tv "rep") [tv "out"] + ] + s1 <- runResolveMPTCTest env s0 preds -- first pass: binds rep=word + s2 <- runResolveMPTCTest env s1 preds -- second pass: now rep is in snapshot → binds out=bool + assertBool + "out should be bound to bool after the second pass" + (hasBind (TVar (Name "out")) bool s2) + +-- --------------------------------------------------------------------------- +-- Unknown class: class absent from instEnv → no-op + +testUnknownClass :: TestTree +testUnknownClass = testCase "UNKNOWN-CLASS: class not in instEnv → phantom stays free" $ do + let env = mkTestEnv [] + s0 = TVar (Name "a") |-> foo + pred_ = inCls "UnknownClass" (tv "a") [tv "rep"] + s1 <- runResolveMPTCTest env s0 [pred_] + assertBool + "rep should remain unbound when class has no instances" + (not (hasAnyBind "rep" s1)) + +-- --------------------------------------------------------------------------- +-- Parameterised self type +-- +-- The self type is List(word) — a parameterised TyCon, not a nullary one. +-- The instance is forall a. List(a):Container(bool), stored as +-- instMainTy = List(TyVar a), instExtras = [bool]. +-- specmatch (List(TyVar a)) (List(word)) = Right {a=word}, concreteExtras = [bool], +-- then specmatch (TyVar rep) bool = Right {rep=bool}. + +testParameterisedMainTy :: TestTree +testParameterisedMainTy = + testCase "PARAM-MAIN: parameterised self type → phantom bound" $ do + let listWord = TyCon (Name "List") [word] + listA = TyCon (Name "List") [tv "a"] + inst = [] :=> inCls "Container" listA [bool] + env = mkTestEnv [(Name "Container", [inst])] + s0 = TVar (Name "self") |-> listWord + pred_ = inCls "Container" (tv "self") [tv "rep"] + s1 <- runResolveMPTCTest env s0 [pred_] + assertBool + "rep should be bound to bool via List(a):Container(bool) instance" + (hasBind (TVar (Name "rep")) bool s1) diff --git a/test/examples/cases/abigeneric.solc b/test/examples/cases/abigeneric.solc new file mode 100644 index 00000000..ad87ac70 --- /dev/null +++ b/test/examples/cases/abigeneric.solc @@ -0,0 +1,127 @@ +pragma no-patterson-condition ABIAttribs, ABIEncode, ABIDecode; +pragma no-bounded-variable-condition ABIAttribs, ABIEncode, ABIDecode; +pragma no-coverage-condition ABIDecode; + +export { + encode, + decode +}; + +import std.{*}; +import std.Generic.{*}; + +function maxWord(a : word, b : word) -> word { + match gtWord(a, b) { + | true => return a; + | false => return b; + } +} + +// ─── ABIAttribs for the primitive sum(f, g) type ───────────────────────── +// headSize = 32 (tag word) + max(headSize(f), headSize(g)) + +forall f g . f:ABIAttribs, g:ABIAttribs => +instance sum(f, g) : ABIAttribs { + function headSize(ty : Proxy(sum(f, g))) -> word { + let pf : Proxy(f); + let pg : Proxy(g); + return 32 + maxWord(ABIAttribs.headSize(pf), ABIAttribs.headSize(pg)); + } + function isStatic(ty : Proxy(sum(f, g))) -> bool { + let pf : Proxy(f); + let pg : Proxy(g); + return and(ABIAttribs.isStatic(pf), ABIAttribs.isStatic(pg)); + } +} + +// ─── ABIEncode for sum(f, g) ───────────────────────────────────────────── +// Wire layout (static sums only): +// [offset + 0 .. offset + 31] : tag word (0 = inl, 1 = inr) +// [offset + 32 .. ] : encoded branch payload + +forall f g . f:ABIAttribs, f:ABIEncode, g:ABIAttribs, g:ABIEncode => +instance sum(f, g) : ABIEncode { + function encodeInto(x : sum(f, g), basePtr : word, offset : word, tail : word) -> word { + match x { + | inl(v) => + mstore(basePtr + offset, 0); + return ABIEncode.encodeInto(v, basePtr, offset + 32, tail); + | inr(v) => + mstore(basePtr + offset, 1); + return ABIEncode.encodeInto(v, basePtr, offset + 32, tail); + } + } +} + +// ─── ABIDecode for sum(f, g) ───────────────────────────────────────────── +// Reads the tag word at headOffset; dispatches to f or g decoder at headOffset + 32. + +forall f g reader . + reader : WordReader, + f : ABIAttribs, + ABIDecoder(f, reader) : ABIDecode(f), + ABIDecoder(g, reader) : ABIDecode(g) => +instance ABIDecoder(sum(f, g), reader) : ABIDecode(sum(f, g)) { + function decode(ptr : ABIDecoder(sum(f, g), reader), headOffset : word) -> sum(f, g) { + match ptr { + | ABIDecoder(rdr) => + let tag = WordReader.read(WordReader.advance(rdr, headOffset)); + match tag { + | 0 => + let dec_f : ABIDecoder(f, reader) = ABIDecoder(rdr); + return inl(ABIDecode.decode(dec_f, headOffset + 32)); + | _ => + let dec_g : ABIDecoder(g, reader) = ABIDecoder(rdr); + return inr(ABIDecode.decode(dec_g, headOffset + 32)); + } + } + } +} + +// ─── Default bridges: ABIAttribs and ABIEncode via Generic ─────────────── +// Any type 'a' with Generic(rep) inherits its ABI layout from rep. + +forall a rep . a:Generic(rep), rep:ABIAttribs => +default instance a : ABIAttribs { + function headSize(ty : Proxy(a)) -> word { + let prx : Proxy(rep); + return ABIAttribs.headSize(prx); + } + function isStatic(ty : Proxy(a)) -> bool { + let prx : Proxy(rep); + return ABIAttribs.isStatic(prx); + } +} + +forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode => +default instance a : ABIEncode { + function encodeInto(x : a, basePtr : word, offset : word, tail : word) -> word { + return ABIEncode.encodeInto(Generic.from(x), basePtr, offset, tail); + } +} + +// ─── Top-level generic encode function ─────────────────────────────────── +// Serialises any 'a' that has a Generic(rep) instance. +// Only the Generic instance is required — ABIEncode is resolved via the bridge. + +forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode => +function encode(x : a, basePtr : word, offset : word, tail : word) -> word { + let xrep : rep = Generic.from(x); + return ABIEncode.encodeInto(xrep, basePtr, offset, tail); +} + +// ─── Top-level generic decode function ─────────────────────────────────── +// Deserialises any 'a' that has a Generic(rep) instance. +// Only the Generic instance is required — ABIDecode is resolved via the bridge. + +forall a rep reader . + a : Generic(rep), + reader : WordReader, + ABIDecoder(rep, reader) : ABIDecode(rep) => +function decode(ptr : ABIDecoder(a, reader), headOffset : word) -> a { + match ptr { + | ABIDecoder(rdr) => + let rep_ptr : ABIDecoder(rep, reader) = ABIDecoder(rdr); + return Generic.to(ABIDecode.decode(rep_ptr, headOffset)); + } +} diff --git a/test/examples/cases/bug-import-default-inst-shadow.solc b/test/examples/cases/bug-import-default-inst-shadow.solc new file mode 100644 index 00000000..8425be2d --- /dev/null +++ b/test/examples/cases/bug-import-default-inst-shadow.solc @@ -0,0 +1,32 @@ +pragma no-patterson-condition ABIAttribs, ABIEncode; +pragma no-bounded-variable-condition ABIAttribs, ABIEncode; + +import std.{*}; +import std.Generic.{*}; + +// Minimal reproducer for the "imported-default-instance-stub mis-tagged" bug. +// +// std/Generic.solc exports: +// forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode => +// default instance a : ABIEncode { function encodeInto ... } +// +// This file redefines the exact same default instance locally. +// The instance head (True, "ABIEncode", [], TyVar "a") is shared. +// +// Bug path: +// 1. filterImportedInstanceConflicts uses topDeclClassNames, which returns [] +// because this file defines no class -- only instances. The imported stub +// is NOT filtered. +// 2. moduleInferenceDeclSegmentByKey maps the shared key to ModuleLocalDecl +// (the local definition arrives first in the ordered list). +// 3. retagModuleInferenceDecls retags the imported stub with the same key, +// giving it ModuleLocalDecl / CheckTopDeclBody mode. +// 4. tcTopDeclWithVisibility calls tcTopDecl' on the stub (funs = []). +// 5. tcInstance' -> checkCompleteInstDef -> "Incomplete definition for ABIEncode". + +forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode => +default instance a : ABIEncode { + function encodeInto(x : a, basePtr : word, offset : word, tail : word) -> word { + return ABIEncode.encodeInto(Generic.from(x), basePtr, offset, tail); + } +} From dc4271c61e96b29b5986ed0b49c6e7f274c94136 Mon Sep 17 00:00:00 2001 From: rodrigogribeiro Date: Tue, 16 Jun 2026 19:41:57 -0300 Subject: [PATCH 07/10] Adding minor changes --- src/Solcore/Backend/Specialise.hs | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs index ec903e51..96db81d6 100644 --- a/src/Solcore/Backend/Specialise.hs +++ b/src/Solcore/Backend/Specialise.hs @@ -1,13 +1,14 @@ module Solcore.Backend.Specialise ( -- core API - specialiseCompUnit - , typeOfTcExp + specialiseCompUnit, + typeOfTcExp, -- testing API - , TVSubst (..) - , emptyTVSubst - , (|->) - , runResolveMPTCTest - ) where + TVSubst (..), + emptyTVSubst, + (|->), + runResolveMPTCTest, + ) +where -- \* Specialisation -- Create specialised versions of polymorphic and overloaded functions. From d1d6e5719c70c6abaee3f32ae40b8e80e3b66d00 Mon Sep 17 00:00:00 2001 From: rodrigogribeiro Date: Wed, 17 Jun 2026 18:59:35 -0300 Subject: [PATCH 08/10] adding encoding lib as a test case --- run_contests.sh | 2 + src/Solcore/Backend/Specialise.hs | 30 +++++++- src/Solcore/Frontend/TypeInference/TcStmt.hs | 6 +- std/ABIGeneric.solc | 36 ++++++++++ test/Cases.hs | 7 +- test/examples/dispatch/generic_product.json | 51 +++++++++++++ test/examples/dispatch/generic_product.solc | 52 ++++++++++++++ test/examples/dispatch/generic_sum.json | 75 ++++++++++++++++++++ test/examples/dispatch/generic_sum.solc | 71 ++++++++++++++++++ 9 files changed, 323 insertions(+), 7 deletions(-) create mode 100644 std/ABIGeneric.solc create mode 100644 test/examples/dispatch/generic_product.json create mode 100644 test/examples/dispatch/generic_product.solc create mode 100644 test/examples/dispatch/generic_sum.json create mode 100644 test/examples/dispatch/generic_sum.solc diff --git a/run_contests.sh b/run_contests.sh index 3ccf8f96..0337035e 100755 --- a/run_contests.sh +++ b/run_contests.sh @@ -19,3 +19,5 @@ bash ./contest.sh test/examples/dispatch/slices.json bash ./contest.sh test/examples/dispatch/fallback.json bash ./contest.sh test/examples/dispatch/ecrecover.json bash ./contest.sh test/examples/dispatch/memory.json +bash ./contest.sh test/examples/dispatch/generic_sum.json +bash ./contest.sh test/examples/dispatch/generic_product.json diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs index 96db81d6..196cb731 100644 --- a/src/Solcore/Backend/Specialise.hs +++ b/src/Solcore/Backend/Specialise.hs @@ -562,7 +562,7 @@ tryResolveMPTC clsName mainTy' extras = do forM_ clsInsts $ \inst -> case inst of -- Only class constraint heads are relevant; skip equality constraints. - (_ :=> InCls _ instMainTy instExtras) -> + (q :=> InCls _ instMainTy instExtras) -> -- Match the instance's main type (pattern) against the call-site's -- concrete main type (target). specmatch binds the instance's -- quantified type variables (TVar) as needed and never touches @@ -571,8 +571,30 @@ tryResolveMPTC clsName mainTy' extras = do case specmatch instMainTy mainTy' of Left _ -> return () Right phi -> do + -- anfInstance normalises instances with extras by replacing each + -- concrete extra with a fresh variable bound by an equality pred: + -- C t [e1,e2] => [v1:~:e1, v2:~:e2] :=> C t [v1,v2] + -- After matching instMainTy against mainTy' we must also resolve + -- these equality constraints (with phi applied) to recover the + -- actual concrete extras; otherwise instExtras still contains + -- the fresh TyVars and looks abstract. + let appliedQ = map (applytv phi) q + eqSubst = + TVSubst + [ (v, t) + | (TyVar v :~: t) <- appliedQ, + null (freetv t) + ] + <> TVSubst + [ (v, t) + | (t :~: TyVar v) <- appliedQ, + null (freetv t) + ] + phi' = phi <> eqSubst + debug [" tryResolve match: phi=", pretty phi, " q=", show q, " appliedQ=", show appliedQ, " eqSubst=", pretty eqSubst, " phi'=", pretty phi', " instExtras=", show instExtras] -- Substitute to obtain the concrete extra types for this instance. - let concreteExtras = map (applytv phi) instExtras + let concreteExtras = map (applytv phi') instExtras + debug [" concreteExtras=", show concreteExtras, " allClosed=", show (all (null . freetv) concreteExtras)] -- If any extra is still abstract, the instance is parametric in a -- way that mainTy' alone does not determine; skip to stay sound. when (all (null . freetv) concreteExtras) $ @@ -584,7 +606,9 @@ tryResolveMPTC clsName mainTy' extras = do -- earlier authoritative binding is preserved. case specmatch extra concrete of Left _ -> return () - Right phi2 -> extSpSubst phi2 + Right phi2 -> do + debug [" extSpSubst phi2=", pretty phi2] + extSpSubst phi2 _ -> return () {- diff --git a/src/Solcore/Frontend/TypeInference/TcStmt.hs b/src/Solcore/Frontend/TypeInference/TcStmt.hs index 5030b57d..b968741d 100644 --- a/src/Solcore/Frontend/TypeInference/TcStmt.hs +++ b/src/Solcore/Frontend/TypeInference/TcStmt.hs @@ -792,8 +792,12 @@ elabFunDef isPub vs sig bdy (Forall _ (pinf :=> tinf)) ann@(Forall _ (pann :=> t findPhantomPredBindings :: [Pred] -> [Pred] -> TcM [(MetaTv, Ty)] findPhantomPredBindings pann pinf = do s0 <- getSubst + -- Apply s0 to BOTH sides so that fresh metas in pinf (e.g. "$94361") are + -- substituted to their source-named counterparts (e.g. Meta "a"), matching the + -- source-named metas in pann. Phantom extras (e.g. "$94362" for "rep") remain + -- free in s0 and stay as fresh metas in pinf', making them identifiable. let pann' = apply s0 (everywhere (mkT toMeta) pann) - pinf' = everywhere (mkT toMeta) pinf + pinf' = apply s0 (everywhere (mkT toMeta) pinf) dom_s0 = map fst (unSubst s0) forM_ (phantomMatchingPreds dom_s0 pann' pinf') $ \(pa, pi_) -> catchError (unifyPredExtras pa pi_) (\_ -> return ()) diff --git a/std/ABIGeneric.solc b/std/ABIGeneric.solc new file mode 100644 index 00000000..02b6c0ef --- /dev/null +++ b/std/ABIGeneric.solc @@ -0,0 +1,36 @@ +pragma no-patterson-condition ABIAttribs, ABIEncode, ABIDecode; +pragma no-bounded-variable-condition ABIAttribs, ABIEncode, ABIDecode; +pragma no-coverage-condition ABIDecode; + +export { + encode, + decode +}; + +import std.{*}; +import std.Generic.{*}; + +// Top-level generic ABI encode. +// Serialises any 'a' that has a Generic(rep) instance. +// ABIEncode for 'a' is resolved via the default instance bridge in std.Generic. +forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode => +function encode(x : a, basePtr : word, offset : word, tail : word) -> word { + let xrep : rep = Generic.from(x); + return ABIEncode.encodeInto(xrep, basePtr, offset, tail); +} + +// Top-level generic ABI decode. +// Deserialises any 'a' whose representation type 'rep' is decodable. +// The caller supplies ABIDecoder(a, reader); the function wraps it in +// ABIDecoder(rep, reader), decodes the rep, then converts via Generic.to. +forall a rep reader . + a : Generic(rep), + reader : WordReader, + ABIDecoder(rep, reader) : ABIDecode(rep) => +function decode(ptr : ABIDecoder(a, reader), headOffset : word) -> a { + match ptr { + | ABIDecoder(rdr) => + let rep_ptr : ABIDecoder(rep, reader) = ABIDecoder(rdr); + return Generic.to(ABIDecode.decode(rep_ptr, headOffset)); + } +} diff --git a/test/Cases.hs b/test/Cases.hs index 83f875fa..f0ff0a21 100644 --- a/test/Cases.hs +++ b/test/Cases.hs @@ -117,7 +117,9 @@ dispatches = runDispatchTest "Revert.solc", runDispatchTest "hashes.solc", runDispatchTest "empty.solc", - runDispatchTest "empty_no_constructor.solc" + runDispatchTest "empty_no_constructor.solc", + runDispatchTest "generic_product.solc", + runDispatchTest "generic_sum.solc" ] where runDispatchTest file = runTestForFileWith (emptyOption mempty) file "./test/examples/dispatch" @@ -517,8 +519,7 @@ cases = runTestExpectingFailure "catenable-err.solc" caseFolder, runTestForFile "pars.solc" caseFolder, runTestForFile "bug-rep-name-capture.solc" caseFolder, - runTestForFile "bug-import-default-inst-shadow.solc" caseFolder, - runTestForFile "abigeneric.solc" caseFolder + runTestForFile "bug-import-default-inst-shadow.solc" caseFolder ] where caseFolder = "./test/examples/cases" diff --git a/test/examples/dispatch/generic_product.json b/test/examples/dispatch/generic_product.json new file mode 100644 index 00000000..b1cb49c4 --- /dev/null +++ b/test/examples/dispatch/generic_product.json @@ -0,0 +1,51 @@ +{ + "generic_product": { + "bytecode": "", + "contract": "GenericProduct", + "tests": [ + { + "input": { + "calldata": "", + "value": "0" + }, + "kind": "constructor" + }, + { + "input": { + "text-calldata": "encodeX(3, 7) -> 3", + "calldata": "0x0dbc6e9b00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000000007", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000003", + "status": "success" + } + }, + { + "input": { + "text-calldata": "encodeY(3, 7) -> 7", + "calldata": "0xe9c28f9600000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000000007", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000007", + "status": "success" + } + }, + { + "input": { + "text-calldata": "decodeX(10, 20) -> 10", + "calldata": "0x0e3fc16f000000000000000000000000000000000000000000000000000000000000000a0000000000000000000000000000000000000000000000000000000000000014", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "000000000000000000000000000000000000000000000000000000000000000a", + "status": "success" + } + } + ] + } +} diff --git a/test/examples/dispatch/generic_product.solc b/test/examples/dispatch/generic_product.solc new file mode 100644 index 00000000..bae06dc2 --- /dev/null +++ b/test/examples/dispatch/generic_product.solc @@ -0,0 +1,52 @@ +import std.{*}; +import std.dispatch.{*}; +import std.Generic.{*}; +import std.ABIGeneric.{*}; + +pragma no-patterson-condition; +pragma no-coverage-condition; +pragma no-bounded-variable-condition; + +data Point = Point(uint256, uint256); + +// Only requirement: Generic instance using the primitive pair type. +// rep = (uint256, uint256) — primitive Solcore pair +instance Point : Generic((uint256, uint256)) { + function from(p : Point) -> (uint256, uint256) { + match p { | Point(x, y) => return (x, y); } + } + function to(t : (uint256, uint256)) -> Point { + match t { | (x, y) => return Point(x, y); } + } +} + +contract GenericProduct { + constructor() {} + + // Calls encode; returns word at offset 0 (the x field). + public function encodeX(a : uint256, b : uint256) -> uint256 { + let p : Point = Point(a, b); + let buf = allocate_zeroed_memory(64); + encode(p, buf, 0, 64); + return Typedef.abs(mload(buf)); + } + + // Calls encode; returns word at offset 32 (the y field). + public function encodeY(a : uint256, b : uint256) -> uint256 { + let p : Point = Point(a, b); + let buf = allocate_zeroed_memory(64); + encode(p, buf, 0, 64); + return Typedef.abs(mload(buf + 32)); + } + + // Writes [a][b] into memory, calls decode, returns the x field. + public function decodeX(a : uint256, b : uint256) -> uint256 { + let buf = allocate_zeroed_memory(64); + mstore(buf, Typedef.rep(a)); + mstore(buf + 32, Typedef.rep(b)); + let rdr : MemoryWordReader = MemoryWordReader(buf); + let dec : ABIDecoder(Point, MemoryWordReader) = ABIDecoder(rdr); + let p : Point = decode(dec, 0); + match p { | Point(x, _) => return x; } + } +} diff --git a/test/examples/dispatch/generic_sum.json b/test/examples/dispatch/generic_sum.json new file mode 100644 index 00000000..acd99eca --- /dev/null +++ b/test/examples/dispatch/generic_sum.json @@ -0,0 +1,75 @@ +{ + "generic_sum": { + "bytecode": "", + "contract": "GenericSum", + "tests": [ + { + "input": { + "calldata": "", + "value": "0" + }, + "kind": "constructor" + }, + { + "input": { + "text-calldata": "encodeNone() -> 0", + "calldata": "cc5ae1e8", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000000", + "status": "success" + } + }, + { + "input": { + "text-calldata": "encodeSomeTag(42) -> 1", + "calldata": "0xef5d5c21000000000000000000000000000000000000000000000000000000000000002a", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000001", + "status": "success" + } + }, + { + "input": { + "text-calldata": "encodePayload(99) -> 99", + "calldata": "0x342242e80000000000000000000000000000000000000000000000000000000000000063", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000063", + "status": "success" + } + }, + { + "input": { + "text-calldata": "decodeAndGet(tag=1, value=77) -> 77", + "calldata": "0xc222f3f50000000000000000000000000000000000000000000000000000000000000001000000000000000000000000000000000000000000000000000000000000004d", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "000000000000000000000000000000000000000000000000000000000000004d", + "status": "success" + } + }, + { + "input": { + "text-calldata": "decodeAndGet(tag=0, value=0) -> 0 (None)", + "calldata": "0xc222f3f500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000000", + "status": "success" + } + } + ] + } +} diff --git a/test/examples/dispatch/generic_sum.solc b/test/examples/dispatch/generic_sum.solc new file mode 100644 index 00000000..abbf11ce --- /dev/null +++ b/test/examples/dispatch/generic_sum.solc @@ -0,0 +1,71 @@ +import std.{*}; +import std.dispatch.{*}; +import std.Generic.{*}; +import std.ABIGeneric.{*}; + +pragma no-patterson-condition; +pragma no-coverage-condition; +pragma no-bounded-variable-condition; + +data Option(a) = None | Some(a); + +// Generic instance using the Sum ADT from std.Generic as the representation. +// Sum((), uint256): Sum.Inl(()) = None, Sum.Inr(v) = Some(v) +instance Option(uint256) : Generic(Sum((), uint256)) { + function from(x : Option(uint256)) -> Sum((), uint256) { + match x { + | Option.None => return Sum.Inl(()); + | Option.Some(v) => return Sum.Inr(v); + } + } + function to(r : Sum((), uint256)) -> Option(uint256) { + match r { + | Sum.Inl(_) => return Option.None; + | Sum.Inr(v) => return Option.Some(v); + } + } +} + +contract GenericSum { + constructor() {} + + // Calls encode; returns the tag word at offset 0. + // None -> 0 (Sum.Inl) + public function encodeNone() -> uint256 { + let x : Option(uint256) = Option.None; + let buf = allocate_zeroed_memory(64); + encode(x, buf, 0, 64); + return Typedef.abs(mload(buf)); + } + + // Calls encode; returns the tag word at offset 0. + // Some(n) -> 1 (Sum.Inr) + public function encodeSomeTag(n : uint256) -> uint256 { + let x : Option(uint256) = Option.Some(n); + let buf = allocate_zeroed_memory(64); + encode(x, buf, 0, 64); + return Typedef.abs(mload(buf)); + } + + // Calls encode; returns the payload word at offset 32. + public function encodePayload(n : uint256) -> uint256 { + let x : Option(uint256) = Option.Some(n); + let buf = allocate_zeroed_memory(64); + encode(x, buf, 0, 64); + return Typedef.abs(mload(buf + 32)); + } + + // Writes [tag][value] into memory, calls decode, returns the value or 0. + public function decodeAndGet(tag : uint256, value : uint256) -> uint256 { + let buf = allocate_zeroed_memory(64); + mstore(buf, Typedef.rep(tag)); + mstore(buf + 32, Typedef.rep(value)); + let rdr : MemoryWordReader = MemoryWordReader(buf); + let dec : ABIDecoder(Option(uint256), MemoryWordReader) = ABIDecoder(rdr); + let opt : Option(uint256) = decode(dec, 0); + match opt { + | Option.None => return uint256(0); + | Option.Some(v) => return v; + } + } +} From 873a2b549b315222343c2fc5b7d635318e9d34fe Mon Sep 17 00:00:00 2001 From: Marcin Benke Date: Thu, 18 Jun 2026 09:40:22 +0200 Subject: [PATCH 09/10] Ormolu formatting --- src/Solcore/Backend/Specialise.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Solcore/Backend/Specialise.hs b/src/Solcore/Backend/Specialise.hs index 196cb731..995850bc 100644 --- a/src/Solcore/Backend/Specialise.hs +++ b/src/Solcore/Backend/Specialise.hs @@ -582,13 +582,13 @@ tryResolveMPTC clsName mainTy' extras = do eqSubst = TVSubst [ (v, t) - | (TyVar v :~: t) <- appliedQ, - null (freetv t) + | (TyVar v :~: t) <- appliedQ, + null (freetv t) ] <> TVSubst [ (v, t) - | (t :~: TyVar v) <- appliedQ, - null (freetv t) + | (t :~: TyVar v) <- appliedQ, + null (freetv t) ] phi' = phi <> eqSubst debug [" tryResolve match: phi=", pretty phi, " q=", show q, " appliedQ=", show appliedQ, " eqSubst=", pretty eqSubst, " phi'=", pretty phi', " instExtras=", show instExtras] From 69a95cb6687075c7f6becf192ec4c55ac7764723 Mon Sep 17 00:00:00 2001 From: Rodrigo Geraldo Ribeiro Date: Thu, 18 Jun 2026 07:08:38 -0300 Subject: [PATCH 10/10] Update test/SpecialiseTests.hs Co-authored-by: Marcin Benke --- test/SpecialiseTests.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/SpecialiseTests.hs b/test/SpecialiseTests.hs index 62cac9d8..c0497560 100644 --- a/test/SpecialiseTests.hs +++ b/test/SpecialiseTests.hs @@ -49,7 +49,7 @@ hasAnyBind name s = any (\(v, _) -> v == TVar (Name name)) (unTVSubst s) specialiseTests :: TestTree specialiseTests = testGroup - "Specialise.resolveMPTCsFromPreds" + "Specialise.resolveMPTCFromPreds" [ testBind, testTwoBothPhantomExtras, testNopAFreeMain,