Backwards constness propagation #204
Description
Since #202 we have special terms needed for calling black boxes unbox(bb(args...), type, sizes) where sizes is for example a single term describing the size of a vector.
Now in the function
julia> typecheck_hs_from_string("
module L
f(x) :: BlackBox() = zeros(x,x)
function g(x::Integer)
m = unbox(f(x), Matrix{<:Real}, (x,x))
(xx,_)=size(m)
xx
end
end")
======================== Errors =====================
======================== End Errors =====================
---------------------------------------------------------------------------
Type:
{
- Int[s_7 ©]
@ ∑∅
--------------------------
-> Int[s_7 ©]
}
---------------------------------------------------------------------------
Constraints:
- top:
- others:
[]
()we would infer that g : Int[n] -> Int[n], thus refining the input type. This is necessary because this function can only be called if the input x is const, only in this case can we know what the output of the black box is going to be.
On the other hand, we have a problem with const in ops. They had a "proper" solving order (which did not work because of something), so we relaxed the ordered solving in #108, and ?. This means that it now probably could happen that we can have the case where a constraint a + b = Int[n] is ignored by op-solving, while the RHS comes from a BB call, and requires that the LHS actually does resolve to something const.