From 2c288dbff326f6af7a3e1624b3edc3d8f764f5d6 Mon Sep 17 00:00:00 2001 From: Michael Sippel <micha@fragmental.art> Date: Wed, 12 Mar 2025 16:38:39 +0100 Subject: [PATCH 1/4] fix tests - in subtype unification: correctly propagate error - in case of subtype between two ladders, check that the matching sub-ladders end at the same bottom rung (to exclude trait-types from sub-types) --- src/test/morphism.rs | 14 ++++++++++---- src/test/unification.rs | 2 +- src/unification.rs | 15 ++++++++++++--- 3 files changed, 23 insertions(+), 8 deletions(-) diff --git a/src/test/morphism.rs b/src/test/morphism.rs index 294ac00..fc0419a 100644 --- a/src/test/morphism.rs +++ b/src/test/morphism.rs @@ -419,6 +419,12 @@ fn test_morphism_path_listedit() dst_type: dict.parse("Char ~ EditTree").unwrap() }) ); + base.add_morphism( + DummyMorphism(MorphismType{ + src_type: dict.parse("<List~Vec Char>").unwrap(), + dst_type: dict.parse("<List Char>").unwrap() + }) + ); base.add_morphism( DummyMorphism(MorphismType{ src_type: dict.parse("<List Char>").unwrap(), @@ -483,12 +489,12 @@ fn test_morphism_path_listedit() }, MorphismInstance { m: DummyMorphism(MorphismType{ - src_type: dict.parse("<List~Vec ReprTree>").unwrap(), - dst_type: dict.parse("<List ReprTree> ~ EditTree").unwrap() + src_type: dict.parse("<List~Vec Char~ReprTree>").unwrap(), + dst_type: dict.parse("<List Char> ~ EditTree").unwrap() }), - halo: dict.parse("<Seq~List <Digit 10>~Char>").unwrap(), + halo: dict.parse("<Seq~List <Digit 10>>").unwrap(), σ: HashMap::new() - } + }, ]) ); } diff --git a/src/test/unification.rs b/src/test/unification.rs index de31d5b..dfff9d2 100644 --- a/src/test/unification.rs +++ b/src/test/unification.rs @@ -142,7 +142,7 @@ fn test_subtype_unification() { assert_eq!( UnificationProblem::new_sub(vec![ - (dict.parse("<Seq~T <Digit 10> ~ Char>").unwrap(), + (dict.parse("<Seq~T <Digit 10> ~ Char ~ Ascii>").unwrap(), dict.parse("<Seq~<LengthPrefix x86.UInt64> Char ~ Ascii>").unwrap()), ]).solve(), Ok(( diff --git a/src/unification.rs b/src/unification.rs index eb55646..5fb0818 100644 --- a/src/unification.rs +++ b/src/unification.rs @@ -255,6 +255,7 @@ impl UnificationProblem { halo: TypeTerm::unit(), addr: new_addr }) { + if a1.len() == i+a2.len() { for j in 0..a2.len() { if i+j < a1.len() { let mut new_addr = unification_pair.addr.clone(); @@ -283,6 +284,13 @@ impl UnificationProblem { } else { TypeTerm::Ladder(halo).strip() }); + } else { + /* after the first match, the remaining ladders dont have the same length + * thus it cannot be a subtype, + * at most it could be a trait type + */ + } + } else { halo.push(a1[i].clone()); //eprintln!("could not unify ladders"); @@ -339,7 +347,7 @@ impl UnificationProblem { // eprintln!("after strip: {:?}", y); // eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y); - if let Ok(halo) = self.eval_subtype( + match self.eval_subtype( UnificationPair { lhs: x.clone(), rhs: y.clone(), @@ -347,6 +355,7 @@ impl UnificationProblem { addr: new_addr, } ) { + Ok(halo) => { if halo == TypeTerm::unit() { let mut y = y.clone(); y.apply_substitution(&|k| self.σ.get(k).cloned()); @@ -376,8 +385,8 @@ impl UnificationProblem { halo_args.push(halo); n_halos_required += 1; } - } else { - return Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }); + }, + Err(err) => { return Err(err); } } } From fe73c47504c63bd7db9dc3a50f3595600a00e6bb Mon Sep 17 00:00:00 2001 From: Michael Sippel <micha@fragmental.art> Date: Fri, 14 Mar 2025 17:44:27 +0100 Subject: [PATCH 2/4] find_morphism_path(): param-normalize halo --- src/morphism.rs | 10 ++++---- src/test/morphism.rs | 59 ++++++++------------------------------------ 2 files changed, 15 insertions(+), 54 deletions(-) diff --git a/src/morphism.rs b/src/morphism.rs index 7b2ac5e..9f29ba8 100644 --- a/src/morphism.rs +++ b/src/morphism.rs @@ -21,8 +21,8 @@ pub struct MorphismType { impl MorphismType { pub fn normalize(self) -> Self { MorphismType { - src_type: self.src_type.normalize().param_normalize(), - dst_type: self.dst_type.normalize().param_normalize(), + src_type: self.src_type.strip().param_normalize(), + dst_type: self.dst_type.strip().param_normalize(), /* subtype_bounds: Vec::new(), trait_bounds: Vec::new() @@ -149,7 +149,7 @@ impl<M: Morphism + Clone> MorphismBase<M> { if let Some( map_morph ) = item_morph_inst.m.map_morphism( seq_type.clone() ) { dst_types.push( MorphismInstance { - halo: TypeTerm::Ladder(dst_halo_ladder).normalize(), + halo: TypeTerm::Ladder(dst_halo_ladder).strip().param_normalize(), m: map_morph, σ: item_morph_inst.σ } @@ -221,7 +221,7 @@ impl<M: Morphism + Clone> MorphismBase<M> { n.halo = n.halo.clone().apply_substitution( &|k| σ.get(k).cloned() - ).clone().strip(); + ).clone().strip().param_normalize(); n.σ = new_σ; } @@ -256,7 +256,7 @@ impl<M: Morphism + Clone> MorphismBase<M> { n.halo = n.halo.clone().apply_substitution( &|k| next_morph_inst.σ.get(k).cloned() - ).clone().strip(); + ).clone().strip().param_normalize(); n.σ = new_σ; } diff --git a/src/test/morphism.rs b/src/test/morphism.rs index fc0419a..e6db4a3 100644 --- a/src/test/morphism.rs +++ b/src/test/morphism.rs @@ -330,51 +330,6 @@ fn test_morphism_path_posint() { ] ) ); - - - -/* - assert_eq!( - base.find_morphism_path(MorphismType { - src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(), - dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap() - }), - Some( - vec![ - dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap().normalize(), - dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), - dict.parse("Symbol ~ ℕ ~ <PosInt 10 LittleEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), - dict.parse("Symbol ~ ℕ ~ <PosInt 16 LittleEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), - dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ ℤ_2^64 ~ machine.UInt64>").unwrap().normalize(), - dict.parse("Symbol ~ ℕ ~ <PosInt 16 BigEndian> ~ <Seq <Digit 16> ~ Char>").unwrap().normalize(), - ] - ) - ); - */ -/* - assert_eq!( - base.find_morphism_with_subtyping( - &MorphismType { - src_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ Char>").unwrap(), - dst_type: dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10> ~ ℤ_2^64 ~ machine.UInt64>").unwrap() - } - ), - - Some(( - DummyMorphism(MorphismType{ - src_type: dict.parse("<Seq <Digit Radix> ~ Char>").unwrap(), - dst_type: dict.parse("<Seq <Digit Radix> ~ ℤ_2^64 ~ machine.UInt64>").unwrap() - }), - - dict.parse("Symbol ~ ℕ ~ <PosInt 10 BigEndian> ~ <Seq <Digit 10>>").unwrap(), - - vec![ - (dict.get_typeid(&"Radix".into()).unwrap(), - dict.parse("10").unwrap()) - ].into_iter().collect::<std::collections::HashMap<TypeID, TypeTerm>>() - )) - ); -*/ } #[test] @@ -421,14 +376,20 @@ fn test_morphism_path_listedit() ); base.add_morphism( DummyMorphism(MorphismType{ - src_type: dict.parse("<List~Vec Char>").unwrap(), - dst_type: dict.parse("<List Char>").unwrap() + src_type: dict.parse("Char").unwrap(), + dst_type: dict.parse("Char ~ ReprTree").unwrap() }) ); base.add_morphism( DummyMorphism(MorphismType{ - src_type: dict.parse("<List Char>").unwrap(), - dst_type: dict.parse("<List Char~ReprTree>").unwrap() + src_type: dict.parse("Char ~ ReprTree").unwrap(), + dst_type: dict.parse("Char").unwrap() + }) + ); + base.add_morphism( + DummyMorphism(MorphismType{ + src_type: dict.parse("<List~Vec Char>").unwrap(), + dst_type: dict.parse("<List Char>").unwrap() }) ); base.add_morphism( From dc6626833d771b8bc377ac34f4fe8d79291fc224 Mon Sep 17 00:00:00 2001 From: Michael Sippel <micha@fragmental.art> Date: Fri, 14 Mar 2025 17:46:59 +0100 Subject: [PATCH 3/4] add failing unification testcase --- src/test/unification.rs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/test/unification.rs b/src/test/unification.rs index dfff9d2..6480b13 100644 --- a/src/test/unification.rs +++ b/src/test/unification.rs @@ -251,6 +251,26 @@ fn test_trait_not_subtype() { ); } +#[test] +fn test_reprtree_list_subtype() { + let mut dict = BimapTypeDict::new(); + + dict.add_varname("Item".into()); + + assert_eq!( + subtype_unify( + &dict.parse("<List~Vec <Digit 10>~Char~ReprTree>").expect(""), + &dict.parse("<List~Vec Item~ReprTree>").expect("") + ), + Ok(( + TypeTerm::unit(), + vec![ + (dict.get_typeid(&"Item".into()).unwrap(), dict.parse("<Digit 10>~Char").unwrap()) + ].into_iter().collect() + )) + ); +} + #[test] pub fn test_subtype_delim() { let mut dict = BimapTypeDict::new(); From 3eaca0dc376b7be2c0e803419a7d07203de50416 Mon Sep 17 00:00:00 2001 From: Michael Sippel <micha@fragmental.art> Date: Sat, 15 Mar 2025 11:33:48 +0100 Subject: [PATCH 4/4] work on unification - add more unification tests - rewrite subtype unification of ladders to work from bottom up --- src/test/unification.rs | 68 ++++++++-- src/unification.rs | 269 ++++++++++++++++++++++++---------------- 2 files changed, 224 insertions(+), 113 deletions(-) diff --git a/src/test/unification.rs b/src/test/unification.rs index 6480b13..6021dda 100644 --- a/src/test/unification.rs +++ b/src/test/unification.rs @@ -132,7 +132,61 @@ fn test_unification() { } #[test] -fn test_subtype_unification() { +fn test_subtype_unification1() { + let mut dict = BimapTypeDict::new(); + dict.add_varname(String::from("T")); + + assert_eq!( + UnificationProblem::new_sub(vec![ + (dict.parse("A ~ B").unwrap(), + dict.parse("B").unwrap()), + ]).solve(), + Ok(( + vec![ dict.parse("A").unwrap() ], + vec![].into_iter().collect() + )) + ); + + assert_eq!( + UnificationProblem::new_sub(vec![ + (dict.parse("A ~ B ~ C ~ D").unwrap(), + dict.parse("C ~ D").unwrap()), + ]).solve(), + Ok(( + vec![ dict.parse("A ~ B").unwrap() ], + vec![].into_iter().collect() + )) + ); + + assert_eq!( + UnificationProblem::new_sub(vec![ + (dict.parse("A ~ B ~ C ~ D").unwrap(), + dict.parse("T ~ D").unwrap()), + ]).solve(), + Ok(( + vec![ TypeTerm::unit() ], + vec![ + (dict.get_typeid(&"T".into()).unwrap(), dict.parse("A ~ B ~ C").unwrap()) + ].into_iter().collect() + )) + ); + + assert_eq!( + UnificationProblem::new_sub(vec![ + (dict.parse("A ~ B ~ C ~ D").unwrap(), + dict.parse("B ~ T ~ D").unwrap()), + ]).solve(), + Ok(( + vec![ dict.parse("A").unwrap() ], + vec![ + (dict.get_typeid(&"T".into()).unwrap(), dict.parse("C").unwrap()) + ].into_iter().collect() + )) + ); +} + +#[test] +fn test_subtype_unification2() { let mut dict = BimapTypeDict::new(); dict.add_varname(String::from("T")); @@ -232,9 +286,9 @@ fn test_trait_not_subtype() { &dict.parse("A ~ B ~ C").expect("") ), Err(UnificationError { - addr: vec![], - t1: dict.parse("A ~ B").expect(""), - t2: dict.parse("A ~ B ~ C").expect("") + addr: vec![1], + t1: dict.parse("B").expect(""), + t2: dict.parse("C").expect("") }) ); @@ -244,9 +298,9 @@ fn test_trait_not_subtype() { &dict.parse("<Seq~List~Vec Char~ReprTree>").expect("") ), Err(UnificationError { - addr: vec![1], - t1: dict.parse("<Digit 10> ~ Char").expect(""), - t2: dict.parse("Char ~ ReprTree").expect("") + addr: vec![1,1], + t1: dict.parse("Char").expect(""), + t2: dict.parse("ReprTree").expect("") }) ); } diff --git a/src/unification.rs b/src/unification.rs index 5fb0818..767bbde 100644 --- a/src/unification.rs +++ b/src/unification.rs @@ -137,85 +137,119 @@ impl UnificationProblem { } } + + + pub fn add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: TypeTerm) -> Result<(),()> { + + if new_lower_bound == TypeTerm::TypeID(TypeID::Var(v)) { + return Ok(()); + } + + if new_lower_bound.contains_var(v) { + // loop + return Err(()); + } + + if let Some(lower_bound) = self.lower_bounds.get(&v).cloned() { +// eprintln!("var already exists. check max. type"); + if let Ok(halo) = self.eval_subtype( + UnificationPair { + lhs: lower_bound.clone(), + rhs: new_lower_bound.clone(), + halo: TypeTerm::unit(), + addr: vec![] + } + ) { +// eprintln!("found more general lower bound"); +// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone()); + // generalize variable type to supertype + self.lower_bounds.insert(v, new_lower_bound); + Ok(()) + } else if let Ok(halo) = self.eval_subtype( + UnificationPair{ + lhs: new_lower_bound, + rhs: lower_bound, + halo: TypeTerm::unit(), + addr: vec![] + } + ) { +// eprintln!("OK, is already larger type"); + Ok(()) + } else { +// eprintln!("violated subtype restriction"); + Err(()) + } + } else { +// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone()); + self.lower_bounds.insert(v, new_lower_bound); + Ok(()) + } + } + + + pub fn add_upper_subtype_bound(&mut self, v: u64, new_upper_bound: TypeTerm) -> Result<(),()> { + if new_upper_bound == TypeTerm::TypeID(TypeID::Var(v)) { + return Ok(()); + } + + if new_upper_bound.contains_var(v) { + // loop + return Err(()); + } + + if let Some(upper_bound) = self.upper_bounds.get(&v).cloned() { + if let Ok(_halo) = self.eval_subtype( + UnificationPair { + lhs: new_upper_bound.clone(), + rhs: upper_bound, + halo: TypeTerm::unit(), + addr: vec![] + } + ) { + // found a lower upper bound + self.upper_bounds.insert(v, new_upper_bound); + Ok(()) + } else { + Err(()) + } + } else { + self.upper_bounds.insert(v, new_upper_bound); + Ok(()) + } + } + pub fn eval_subtype(&mut self, unification_pair: UnificationPair) -> Result< // ok: halo type TypeTerm, // error UnificationError > { + eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs); match (unification_pair.lhs.clone(), unification_pair.rhs.clone()) { /* Variables */ - (t, TypeTerm::TypeID(TypeID::Var(varid))) => { -// eprintln!("t <= variable"); - if ! t.contains_var( varid ) { - // let x = self.σ.get(&TypeID::Var(varid)).cloned(); - if let Some(lower_bound) = self.lower_bounds.get(&varid).cloned() { -// eprintln!("var already exists. check max. type"); - if let Ok(halo) = self.eval_subtype( - UnificationPair { - lhs: lower_bound.clone(), - rhs: t.clone(), - halo: TypeTerm::unit(), - addr: vec![] - } - ) { -// eprintln!("found more general lower bound"); -// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone()); - // generalize variable type to supertype - self.lower_bounds.insert(varid, t.clone()); - } else if let Ok(halo) = self.eval_subtype( - UnificationPair{ - lhs: t.clone(), - rhs: lower_bound.clone(), - halo: TypeTerm::unit(), - addr: vec![] - } - ) { -// eprintln!("OK, is already larger type"); - } else { -// eprintln!("violated subtype restriction"); - return Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t }); - } - } else { -// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone()); - self.lower_bounds.insert(varid, t.clone()); - } - self.reapply_subst(); - Ok(TypeTerm::unit()) - } else if t == TypeTerm::TypeID(TypeID::Var(varid)) { + (t, TypeTerm::TypeID(TypeID::Var(v))) => { + //eprintln!("t <= variable"); + if self.add_lower_subtype_bound(v, t.clone()).is_ok() { Ok(TypeTerm::unit()) } else { - Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(varid)), t2: t }) + Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t }) } } - (TypeTerm::TypeID(TypeID::Var(varid)), t) => { -// eprintln!("variable <= t"); - - if let Some(upper_bound) = self.upper_bounds.get(&varid).cloned() { - if let Ok(_halo) = self.eval_subtype( - UnificationPair { - lhs: t.clone(), - rhs: upper_bound, - halo: TypeTerm::unit(), - addr: vec![] - } - ) { - // found a lower upper bound - self.upper_bounds.insert(varid, t); - } + (TypeTerm::TypeID(TypeID::Var(v)), t) => { + //eprintln!("variable <= t"); + if self.add_upper_subtype_bound(v, t.clone()).is_ok() { + Ok(TypeTerm::unit()) } else { - self.upper_bounds.insert(varid, t); + Err(UnificationError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(v)), t2: t }) } - Ok(TypeTerm::unit()) } - /* Atoms */ @@ -236,68 +270,91 @@ impl UnificationProblem { */ (TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) => { - let mut halo = Vec::new(); - if a1.len() < a2.len() { - return Err(UnificationError { - addr: vec![], - t1: unification_pair.lhs, - t2: unification_pair.rhs - }); - } - for i in 0..a1.len() { - let mut new_addr = unification_pair.addr.clone(); - new_addr.push(i); - if let Ok(r_halo) = self.eval_subtype( UnificationPair { - lhs: a1[i].clone(), - rhs: a2[0].clone(), + let mut l1_iter = a1.into_iter().enumerate().rev(); + let mut l2_iter = a2.into_iter().rev(); - halo: TypeTerm::unit(), - addr: new_addr - }) { - if a1.len() == i+a2.len() { - for j in 0..a2.len() { - if i+j < a1.len() { - let mut new_addr = unification_pair.addr.clone(); - new_addr.push(i+j); + let mut halo_ladder = Vec::new(); - let lhs = a1[i+j].clone();//.apply_substitution(&|k| self.σ.get(k).cloned()).clone(); - let rhs = a2[j].clone();//.apply_substitution(&|k| self.σ.get(k).cloned()).clone(); + while let Some(rhs) = l2_iter.next() { + //eprintln!("take rhs = {:?}", rhs); + if let Some((i, lhs)) = l1_iter.next() { + //eprintln!("take lhs ({}) = {:?}", i, lhs); + let mut addr = unification_pair.addr.clone(); + addr.push(i); + //eprintln!("addr = {:?}", addr); - if let Ok(rung_halo) = self.eval_subtype( + match (lhs.clone(), rhs.clone()) { + (t, TypeTerm::TypeID(TypeID::Var(v))) => { + + if self.add_upper_subtype_bound(v,t.clone()).is_ok() { + let mut new_upper_bound_ladder = vec![ t ]; + + if let Some(next_rhs) = l2_iter.next() { + + // TODO + + } else { + // take everything + + while let Some((i,t)) = l1_iter.next() { + new_upper_bound_ladder.push(t); + } + } + + new_upper_bound_ladder.reverse(); + if self.add_upper_subtype_bound(v, TypeTerm::Ladder(new_upper_bound_ladder)).is_ok() { + // ok + } else { + return Err(UnificationError { + addr, + t1: lhs, + t2: rhs + }); + } + } else { + return Err(UnificationError { + addr, + t1: lhs, + t2: rhs + }); + } + } + (lhs, rhs) => { + if let Ok(ψ) = self.eval_subtype( UnificationPair { lhs: lhs.clone(), rhs: rhs.clone(), - addr: new_addr.clone(), - halo: TypeTerm::unit() + addr:addr.clone(), halo: TypeTerm::unit() } ) { - halo.push(rung_halo); + // ok. + //eprintln!("rungs are subtypes. continue"); + halo_ladder.push(ψ); } else { - return Err(UnificationError{ addr: new_addr, t1: lhs, t2: rhs }) + return Err(UnificationError { + addr, + t1: lhs, + t2: rhs + }); } } } - - return Ok( - if halo.len() == 1 { - halo.pop().unwrap() - } else { - TypeTerm::Ladder(halo).strip() - }); - } else { - /* after the first match, the remaining ladders dont have the same length - * thus it cannot be a subtype, - * at most it could be a trait type - */ - } - } else { - halo.push(a1[i].clone()); - //eprintln!("could not unify ladders"); + // not a subtype, + return Err(UnificationError { + addr: vec![], + t1: unification_pair.lhs, + t2: unification_pair.rhs + }); } } + //eprintln!("left ladder fully consumed"); - Err(UnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) + for (i,t) in l1_iter { + halo_ladder.push(t); + } + halo_ladder.reverse(); + Ok(TypeTerm::Ladder(halo_ladder).strip().param_normalize()) }, (t, TypeTerm::Ladder(a1)) => { @@ -362,9 +419,9 @@ impl UnificationProblem { y = y.strip(); let mut top = y.get_lnf_vec().first().unwrap().clone(); halo_args.push(top.clone()); -// eprintln!("add top {:?}", top); + //eprintln!("add top {:?}", top); } else { -// eprintln!("add halo {:?}", halo); + //eprintln!("add halo {:?}", halo); if n_halos_required > 0 { let x = &mut halo_args[n_halos_required-1]; if let TypeTerm::Ladder(argrs) = x { @@ -391,7 +448,7 @@ impl UnificationProblem { } if n_halos_required > 0 { -// eprintln!("halo args : {:?}", halo_args); + //eprintln!("halo args : {:?}", halo_args); Ok(TypeTerm::App(halo_args)) } else { Ok(TypeTerm::unit())