New fixes in type inference / specialization for ABI encoding library

[rodrigogribeiro]

No description provided.

[mbenke]

$ cabal run sol-core -- -f test/examples/cases/bug-mptc-template-a.solc 
PANIC: ! specCall: no resolution found for Encoder.encode : Foo -> word -> word -> word

// Bug: tryResolveMPTC Template A wrongly binds `rep` when a class method takes
// more than one argument.
//
// Template A matches storedTy against (mainTy :-> freshV).
// For Encoder.encode specialised at Foo, storedTy = Foo -> word -> word.
// specmgu (Foo -> word -> word) (Foo -> freshV) succeeds with freshV = word -> word
// because `word -> word` is a fully-concrete type (no free vars), the guard
// `null (freetv concrete)` passes, and rep gets bound to word -> word instead
// of word.
//
// The phantom variable `rep` has no return-type context here (encodeAndDiscard
// returns ()) so it cannot be resolved from the call site -- tryResolveMPTC is
// the only mechanism that fires, and it produces the wrong answer.
//
// Expected (main, without tryResolveMPTC): clear "unresolved type variable" error.
// Actual (PR branch, with tryResolveMPTC): panic -- no resolution for
//   Encoder.encode : Foo -> word -> word -> word  (wrong 4-arg type from rep=word->word)

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;
    }
}

[mbenke]

Another regression:

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; }
    }
}

this seems to compile fine on main, but here fails with

PANIC: ! specCall: no resolution found for tagFirst : TypeA -> TypeB -> TagA

My understanding is that phantomMatchingPreds pairs EVERY annotation Tag with EVERY inferred Tag (a full 2x2 cross product), and unifyPredExtras then does unify mt1 mt2 on each pair -- including the (a-pred, b-pred) pairing, which unifies the two distinct type parameters a ~ b.

[mbenke]

Some tests would be nice too :)

[mbenke]

Suggested change

	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
	Right phi -> do
	let concrete = applytv phi freshV
	-- A representation type is never a function type. An arrow here means we
	-- matched a multi-argument method (e.g. self -> word -> rep) against the
	-- unary template (self -> freshV) and captured the trailing argument
	-- types by mistake; reject so the phantom var stays unresolved and the
	-- caller reports it cleanly instead of panicking on a bogus arity later.
	when (null (freetv concrete) && not (isArrow concrete)) $
	forM_ extras $ \extra ->
	case specmgu extra concrete of
	Left _ -> return ()
	Right phi2 -> extSpSubst phi2
	where
	isArrow (_ :-> _) = True
	isArrow _ = False

[mbenke]

compute the set of metavariables that occur in the function type (funMetas = mv tinf' ∪ mv tann') and exclude them from delta, keeping only genuinely phantom variables (present in predicates, absent from the function type) - also requires changing findPhantomPredBindings

Suggested change

	phantomDelta <- findPhantomPredBindings pann pinf
	let funMetas = mv tinf' `union` mv tann'
	phantomDelta <- findPhantomPredBindings funMetas pann pinf

[mbenke]

Suggested change

	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)
	findPhantomPredBindings :: [MetaTv] -> [Pred] -> [Pred] -> TcM [(MetaTv, Ty)]
	findPhantomPredBindings funMetas 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
	-- Keep only bindings for genuinely phantom vars: newly introduced (not in
	-- dom_s0) AND absent from the function type (funMetas). This drops stray
	-- bindings such as `a := b` produced by cross-product pairing of two
	-- same-class constraints, which would otherwise corrupt the signature.
	let delta = filter (\(v, _) -> v `notElem` dom_s0 && v `notElem` funMetas) (unSubst s_full)

[mbenke]

Added suggested fixes for the two issues mentioned in the review yesterday.

[mbenke]

We need some real tests - currently all test pass even when resolveMPTCFromPreds is replaced with return ()