fixes bug 438, incorporate subtypes into type unification when typechecking parameter...

diff --git a/src/util/matcher.h b/src/util/matcher.h
index 1eb7229789a6b8ecb6125d263365a761aaebc8e8..78738e27f6d1eb33a227eef3e84f2cc6e9ffcee2 100644 (file)
--- a/src/util/matcher.h
+++ b/src/util/matcher.h
@@ -66,8 +66,16 @@ public:
     std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), pattern );
     if( i!=d_types.end() ){
       int index = i - d_types.begin();
-      if( !d_match[index].isNull() && d_match[index]!=tn ){
-        return false;
+      if( !d_match[index].isNull() ){
+        Debug("typecheck-idt") << "check subtype " << tn << " " << d_match[index] << std::endl;
+        TypeNode tnn = TypeNode::leastCommonTypeNode( tn, d_match[index] );
+        //recognize subtype relation
+        if( !tnn.isNull() ){
+          d_match[index] = tnn;
+          return true;
+        }else{
+          return false;
+        }
       }else{
         d_match[ i - d_types.begin() ] = tn;
         return true;