New fixes in type inference / specialization for ABI encoding library

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

sol-core.cabal

@@ -174,6 +174,7 @@ test-suite sol-core-tests
     HullCases
     MatchCompilerTests
     ModuleTypeCheckTests
+    SpecialiseTests
     YulEvalTests
     ParserTests
 

src/Solcore/Backend/Specialise.hs

@@ -1,4 +1,14 @@
-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.
@@ -20,7 +30,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
@@ -347,10 +357,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 (_ :-> rest) = resultTy rest
+    resultTy t = t
 
 -- | Specialise a function call
 -- given actual arguments and the expected result type
@@ -447,6 +472,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 +486,131 @@ specFunDef fd0 = withLocalState do
 specBody :: [Stmt Id] -> SM [Stmt Id]
 specBody = mapM specStmt
 
+-- 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
+  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 ()
+
+-- | 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.
+--
+-- 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
+  -- 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.
+      (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
+        -- 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
+            -- 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
+            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) $
+              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 -> do
+                    debug ["  extSpSubst phi2=", pretty phi2]
+                    extSpSubst phi2
+      _ -> return ()
+
 {-
 ensureSimple ty' stmt subst = case ty' of
     TyVar _ -> panics [ "specStmt(",pretty stmt,"): polymorphic return type: "
@@ -525,7 +680,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 +696,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''
@@ -710,6 +879,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

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
 

src/Solcore/Frontend/TypeInference/TcStmt.hs

@@ -753,15 +753,83 @@ 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.
+--
+-- 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
+  -- 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' = 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 ())
+  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 mt_a _) <- pann,
+      hasPhantomMeta pa, -- skip annotation preds already fully resolved in s0
+      pi_@(InCls cls' mt_i _) <- pinf,
+      cls == cls',
+      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)
+    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)