concept Stack {
    contract {
      push(value_type x);
      pop() : value_type;
      is_empty() : bool;
    }
    requires {
      value_type : Any;
    }
  }

  void MyFxn(Stack& x, Stack& y) {
    y.push(x.pop()); 
  }

  int main() {
    MyStack[int] s1;
    MyStack[string] s2;
    MyFxn(s1, s2); // compiler accepts this happily 
  }

One solution for the programmer is to use the C++ way of doing things:

  void MyFxn[T : Stack](T& x, T& y) {
    y.push(x.pop()); 
  }

void MyFxn( Stack[value_type=int]& x,
            Stack[value_type=int]& y )
{
   y.push(x.pop());
}

void MyFxn( Stack[int]& x,
            Stack[int]& y )
{
   y.push(x.pop());
}

void MyFxn( Stack[T1:Any]& x,
            Stack[T1]& y )

void MyFxn( Stack[T1:Any]& x,
            Stack[T1]& y,
            Stack& z );

void MyFxn( Stack[T1:Any]& x,
            Stack[T2:Any]& y );

  int main() {
    MyStack[int] s1;
    MyStack[long] s2;
    MyFxn(s1, s2); // ok, because int can be converted to long
  }

>   int main() {
>     MyStack[int] s1;
>     MyStack[long] s2;
> MyFxn(s1, s2); // ok, because int can be converted to
> d to long
>   }
> 

int example(int a,int b)
  where (a >= 0), (a < 32),
        (b > a), (b < 400)
{
  // code that returns some value on a and b
}

void MyFunction(Stack& x,Stack& y)
        where (typeof(x) == typeof(y))
{
  y.push(x.pop());
}

void MyFunction(Stack& x,Stack& y)
        where(derivedfrom(x,y) || derivedfrom(y,x))
{
  y.push(x.pop());
}

int example(int a,int b)
where (a >= 0), (a <  32),
      (b >  a), (b < 400)
whence (a >= example), (example < b)
{
  // code that returns some value on a and b
}