#define testUnify
///testUnify(a, b)
/**
 * testUnify :: TypeConLink -> TypeConLink -> Boolean
 * 
 * Returns whether types `a` and `b` can be unified.
 *
 * @param a the first type con
 * @param b the second type con
 * @returns true if a and b can be unified, false otherwise
 */
var a = argument0;
var b = argument1;

assertInstanceof(a, TypeConLink);
assertInstanceof(b, TypeConLink);


//same instance can always be unified
if (a == b)
  return true;


//test whether inhabited type can be unified
if (instanceof(a, TypeCon1Link) && instanceof(b, TypeCon1Link))
  return testUnifyType(a.type, b.type);


//inhabited type can only be unified with type con if it is a free type
if (!instanceof(a, TypeCon1Link) && instanceof(b, TypeCon1Link))
  return testUnify(b, a);
if (instanceof(a, TypeCon1Link) && !instanceof(b, TypeCon1Link)) {
  if (instanceof(a.type, FreeType) && !containsType(a.type, b) && instanceof(b.to[|0], TypeCon1Link))
    return testUnify(a, b.to[|0]);
  else
    return false;
}

//type cons can only be unified if they have the same arity and their inhabited types match
if (!instanceof(a, TypeCon1Link) && !instanceof(b, TypeCon1Link)) {
  if (ds_list_size(a.to) != ds_list_size(b.to))
    return false;

  for (var i = 0; i < ds_list_size(a.to); i++)
    if (!testUnify(a.to[|i], b.to[|i]))
      return false;

  return true;
}


#define testUnifyType
///testUnify(a, b)
/**
 * testUnify :: Type -> Type -> Boolean
 * 
 * Returns whether types `a` and `b` can be unified.
 *
 * @param a the first type
 * @param b the second type
 * @returns true if a and b can be unified, false otherwise
 */

var a = argument0;
var b = argument1;

assertInstanceof(a, Type);
assertInstanceof(b, Type);

//the same type can always be unified
if (a == b)
  return true;


//two free variables can always be unified
if (instanceof(a, FreeType) && instanceof(b, FreeType))
  return true;


//a type variable can be unified with a concrete type iff its traits are a subset of the concrete traits
if (instanceof(a, FreeType) && !instanceof(b, FreeType))
  return ds_set_is_subset(a.traits, b.traits);
if (!instanceof(a, FreeType) && instanceof(b, FreeType))
  return ds_set_is_subset(b.traits, a.traits);


//two different concrete types cannot be unified
return false;
#define containsType
///containsType(type, con)
/**
 * containsType :: FreeType -> TypeConLink -> Boolean
 *
 * Returns whether a free type appears within a typecon.
 */

var type = argument0;
var con = argument1;

assertInstanceof(type, FreeType);
assertInstanceof(con, TypeConLink);

if (instanceof(con, TypeCon1Link))
  return con.type == type;
else
  for (var i = 0; i < ds_list_size(con.to); i++)
    if (containsType(type, con.to[|i]))
      return true;

return false;