Skip to content

Leftover constraint when function return type is unknown #208

Description

@MxmUrw

Take the following example:

function count(f:: Function, d::Matrix) :: Priv()
  (dim, _) = size(d)
  counter = 0
  for i in 1:dim
    dd = d[i,:]
    if f(dd) == 1
      counter = counter + 1
    else
      counter = clone(counter)
    end
  end
  counter
end

We get as result:

---------------------------------------------------------------------------
Type:
Fun([([Fun([([NoFun(Vector<n: τ_31, c: τ_10>[s_8](τ_82)) @ s_23] -> NoFun(τa_26)) @ Nothing]) @ (∞,∞),NoFun(Matrix<n: τ_31, c: τ_10>[s_9 × s_8](τ_82)) @ (∞,∞)] ->* NoFun(Num(Int[--]))) @ Just [Function,Matrix{Any}]])
---------------------------------------------------------------------------

in other words:

---------------------------------------------------------------------------
Type:
{
  -  {
    -  Vector<n: τ_31, c: τ_10>[s_8](τ_82)
        @ s_23
    --------------------------
     -> τa_26
  
  }
      @ (∞, ∞)
  
  -  Matrix<n: τ_31, c: τ_10>[s_9 × s_8](τ_82)
      @ (∞, ∞)
  --------------------------
   ->* Int[--]

}
---------------------------------------------------------------------------
Constraints:
   - top:
constr_7 : [final,worst,global,exact,special] IsTypeOpResult (Binary == (τa_26 @ η_17,Num(Int[1]) @ η_18) Bool)
   - others:

The actual question now is the constr_7 which we currently simply cannot resolve because τa_26 is the return type of the input function, and we thus have no idea what type it is.

What we might want to do is allow some kind of annotations for this case? Or resolve the == ops differently in the worst-case-solving?

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions