Use unambiguous [TVAssignment] instead of Unifier to figure out required...

Use unambiguous [TVAssignment] instead of Unifier to figure out required context to avoid variable clashes (e.g. 'select :: [a] Int -> a' would require Array [] [] instead of Array [] a)

Cloogle/Search.icl

@@ -104,25 +104,29 @@ unifyInformation :: !(Maybe Type) !(Map String [TypeDef]) ![TypeDef] !FunctionEn
 	-> *(!Maybe Unifier, ![TypeDef], !Maybe [(!String, ![LocationResult])], !*CloogleDB)
 unifyInformation orgsearchtype allsyns usedsyns fe db
 # (alwaysUnique,db) = alwaysUniquePredicate db
-# fe_type = prepare_unification False alwaysUnique allsyns <$> fe.fe_type
-# usedsyns = case fe_type of Nothing -> usedsyns; Just (syns,_) -> syns ++ usedsyns
-# unif = fe_type >>= \(_,type) -> finish_unification usedsyns <$> (orgsearchtype >>= unify type)
+# (usedsyns,fe_type) = appFst (flip (++) usedsyns) $ prep alwaysUnique $ fromJust fe.fe_type
+# tvas = orgsearchtype >>= unify fe_type
+| isNothing tvas = (Nothing, usedsyns, Nothing, db)
+# tvas = fromJust tvas
+# unif = finish_unification usedsyns tvas
 // Required Context
 # (ownContext,db) = ownContext fe db
-# (required_context,db) = fromMaybe (tuple Nothing) (liftA2 (findContext ownContext) fe.fe_type unif) db
-= (unif,usedsyns,required_context,db)
+# (required_context,db) = findContext ownContext fe_type tvas db
+= (Just unif,usedsyns,required_context,db)
 where
+	prep alwaysUnique = prepare_unification False alwaysUnique allsyns
+
 	ownContext :: FunctionEntry *CloogleDB -> *([TypeRestriction], *CloogleDB)
 	ownContext fe db
 	| isJust fe.fe_generic_vars =
-		([Derivation (getName fe.fe_loc) (Var v) \\ v <- fromJust fe.fe_generic_vars], db)
+		([Derivation (getName fe.fe_loc) (snd $ prep (const False) $ Var v) \\ v <- fromJust fe.fe_generic_vars], db)
 	= case fe.fe_class of
 		Nothing -> ([], db)
 		Just ci -> let ({value=ClassEntry ce},db`) = getIndex ci db in
-			([Instance (getName ce.ce_loc) (map Var ce.ce_vars)], db`)
+			([Instance (getName ce.ce_loc) (map (snd o prep (const False) o Var) ce.ce_vars)], db`)
 
-	findContext :: [TypeRestriction] Type Unifier *CloogleDB -> *(Maybe [(String, [LocationResult])], *CloogleDB)
-	findContext trs t unif db
+	findContext :: [TypeRestriction] Type [TVAssignment] *CloogleDB -> *(Maybe [(String, [LocationResult])], *CloogleDB)
+	findContext trs t tvas db
 	# trs = removeDup (concatMap applyUnifToTR (getTC t ++ trs))
 	= appFst Just $
 		mapSt (\tr -> appFst (tuple (concat $ print False tr) o map locResult) o findLocations tr) trs db
@@ -142,7 +146,17 @@ where
 			derivs = [Derivation g (Type st []) \\ Type st _ <- subts]
 
 		uni :: (Type -> Maybe Type)
-		uni = fmap norm o assignAll (map fromUnifyingAssignment unif.assignments)
+		uni = fmap (remove_var_prefixes o norm) o assignAll tvas
+		where
+			remove_var_prefixes :: !Type -> Type
+			remove_var_prefixes (Var v)         = Var (v % (1,size v-1))
+			remove_var_prefixes (Cons c ts)     = Cons (c % (1,size c-1)) (map remove_var_prefixes ts)
+			remove_var_prefixes (Type t ts)     = Type t (map remove_var_prefixes ts)
+			remove_var_prefixes (Func is r c)   = Func (map remove_var_prefixes is) (remove_var_prefixes r) c
+			remove_var_prefixes (Uniq t)        = Uniq $ remove_var_prefixes t
+			remove_var_prefixes (Forall vs t c) = Forall (map remove_var_prefixes vs) (remove_var_prefixes t) c
+			remove_var_prefixes (Arrow mt)      = Arrow $ remove_var_prefixes <$> mt
+			remove_var_prefixes (Strict t)      = Strict $ remove_var_prefixes t
 
 		norm :: (Type -> Type)
 		norm = snd o resolve_synonyms allsyns