@@ -99,10 +99,13 @@ constrain env (A.A region expression) tipe =
9999 return $ con /\ tipe === (argType ==> resType)
100100
101101 E.App func arg ->
102− exists $ \t ->
103− do funcCon <- constrain env func (t ==> tipe)
104− argCon <- constrain env arg t
105− return (funcCon /\ argCon)
102+ do argVar <- variable Flexible
103+ resultVar <- variable Flexible
104+ argCon <- constrain env arg (varN argVar)
105+ funcCon <- constrain env func (varN argVar ==> varN resultVar)
106+ let appCon = tipe === varN resultVar
107+ return $
108+ ex [argVar,resultVar] (CAnd [ argCon, funcCon, appCon ])
106109
107110 E.MultiIf branches ->
108111 constrainIf env region branches tipe