From 7bb97d7258303c5ac228222baccb6bffe3c55f50 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 29 Nov 2012 22:02:20 +0000
Subject: [PATCH] fixes bug 438, incorporate subtypes into type unification
 when typechecking parameterized datatypes

---
 src/util/matcher.h | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/util/matcher.h b/src/util/matcher.h
index 1eb722978..78738e27f 100644
--- 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;
-- 
2.30.2