From d7a33c974e403a418b5653ea12792d356606ad50 Mon Sep 17 00:00:00 2001
From: greg <greg.shuflin@protonmail.com>
Date: Wed, 11 Oct 2017 02:33:46 -0700
Subject: [PATCH] More work with unification

---
 src/schala_lang/type_check.rs | 31 +++++++++++++++++++++++--------
 1 file changed, 23 insertions(+), 8 deletions(-)

diff --git a/src/schala_lang/type_check.rs b/src/schala_lang/type_check.rs
index fc1903a..c680e7d 100644
--- a/src/schala_lang/type_check.rs
+++ b/src/schala_lang/type_check.rs
@@ -1,6 +1,9 @@
 use std::collections::HashMap;
 use std::rc::Rc;
 
+
+//SKOLEMIZATION - how you prevent an unassigned existential type variable from leaking!
+
 use schala_lang::parsing::{AST, Statement, Declaration, Signature, Expression, ExpressionType, Operation, Variant, TypeName};
 
 // from Niko's talk
@@ -134,7 +137,7 @@ impl TypeContext {
     self.symbol_table.get(&key).map(|entry| entry.clone())
   }
   pub fn debug_symbol_table(&self) -> String  {
-    format!("Symbol table:\n {:?}", self.symbol_table)
+    format!("Symbol table:\n {:?}\nEvar table:\n{:?}", self.symbol_table, self.evar_table)
   }
   fn alloc_existential_type(&mut self) -> Type {
     let ret = Type::TVar(TypeVar::Exist(self.existential_type_label_count));
@@ -360,13 +363,25 @@ impl TypeContext {
           Err(format!("Couldn't unify universal types {} and {}", a, b))
         }
       },
-      (&TVar(Exist(ref a)), &TVar(Exist(ref b))) => {
-        //the interesting case!!
-
-        if a == b {
-          Ok(TVar(Exist(a.clone())))
-        } else {
-          Err(format!("Couldn't unify existential types {} and {}", a, b))
+      //the interesting case!!
+      (&TVar(Exist(ref a)), ref t2) => {
+        let x = self.evar_table.get(a).map(|x| x.clone());
+        match x {
+          Some(ref t1) => self.unify(t1.clone().clone(), t2.clone().clone()),
+          None => {
+            self.evar_table.insert(*a, t2.clone().clone());
+            Ok(t2.clone().clone())
+          }
+        }
+      },
+      (ref t1, &TVar(Exist(ref a))) => {
+        let x = self.evar_table.get(a).map(|x| x.clone());
+        match x {
+          Some(ref t2) => self.unify(t2.clone().clone(), t1.clone().clone()),
+          None => {
+            self.evar_table.insert(*a, t1.clone().clone());
+            Ok(t1.clone().clone())
+          }
         }
       },
       _ => Err(format!("Types {:?} and {:?} don't unify", t1, t2))