Unresolved type variables in pattern matching code

I have found another problem with type annotations, which breaks specialisation.

Consider a simple contract (https://github.com/rodrigogribeiro/solcore/blob/main/test/examples/spec/04pair.solc):

contract Pair {
data Pair[a,b] = Pair[a,b]

  function fst(p) {
    match p {
      | Pair[a,b] => return a;
    };
  }

  function main() {
    return fst(Pair[1,0]);
  }
}

The output from the pattern matching compiler is (relevant fragment):

   function fst (p : Pair[e, f]) {
      match (p) {
      | Pair[var_2, var_4] =>
         let var_6 = var_2 ;
         let var_8 = var_4 ;
         return var_6
      | var_1 =>
         revert('Incomplete matching');
      }
   }

which a first sight looks quite reasonable (except for the redundant revert, but that's anotjer story), however:

variables in patterns are not annotated at all
variables in branches are annotated with unbound type variables

Here's a detailed dump of the Pair branch:

pattern: [PCon Pair [PVar var_2,PVar var_4]]
body:
[ Let (Id {idName = var_6, idType = TyVar (TVar var_7)}) 
      (Just (TyVar (TVar var_7))) 
      (Just (Var (Id {idName = var_2, idType = TyVar (TVar var_3)})))

, Let (Id {idName = var_8, idType = TyVar (TVar var_9)}) 
      (Just (TyVar (TVar var_9))) 
      (Just (Var (Id {idName = var_4, idType = TyVar (TVar var_5)})))

,Return (Var (Id {idName = var_6, idType = TyVar (TVar e)}))
]

Note that in the return statement, var_6 is annotated correctly with the quantified variable e, but in the let statement, it is annotated with unbound var_7.

rodrigogribeiro / solcore

Unresolved type variables in pattern matching code #11