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