rc :: List a -> a -> List a
rc l x = x : l
fold rc [] [3,2,1]
The type of fold looks like
fold :: (a -> b -> a) -> a -> List b -> a
and we're applying it to 'rc (List Void) (List Int)'. When we hit the
second argument, we add the constraint
a >= List Void
We then go back and call apply on the first argument. When we do
that, it turns the >= constraint into
a == List Void
But "a" occurs as the return type, so matching return types gives
List Int <= a (= List Void)
The correct solution is to apply fixpoint iteration instead of
freezing. If we plug the value of a constrained type variable into
apply and then adjust the constraint, we need to call apply again to
produce an updated value. I'll take a look at this.
On a related note, it took me a while to realize the problem since the
error messages aren't detailed enough. It'd be better if the error
messages said that it failed when unifying return types, and that the
"Int <= Void" constraint arose as a result of "List Int <= List Void".
I guess this means we need to add stack support to TypeMonad, though
I'm not sure what the cleanest way to go about that is.
Geoffrey
If you mean what I think, then it's already there -- we just need to add more
messages:
typeReError noLoc "message" $ stuff
Executes stuff and, if there's an error, puts "message" at the top of the
stack, otherwise does nothing. It'd be easy enough to make a typeReMismatch
version... or some better name. We can also make one that is essentially
"sequence" but that collects all the errors if there are any and calls
typeErrors with them (like what happens in resolve).
:-Dyla
range x y = if x <= y then x : range (x + 1) y else []
range :: Int -> Int -> Void -- starting point
range Int Int = Void -- lookup for recursion
(:) Int Void = Void -- apply
if Bool Void = Void -- apply
Void (List Void) = Void -- apply
range :: Int -> Int -> Void -- convergance
If there is a problem I'm guessing it's the "(:) Int Void" step. A function
being applied to Void should probably actually try to find a matching
overload, right? So "(:) Int Void" unifies "Void" with "List a" and we get
"List a". In fact, just removing this second "apply" rule makes this case
work fine. Is that the right thing to do?
:-Dylan
"(:) Int Void" should definitely be Void; the second argument can't
exist, so the call can't be executed, so it will never return
anything.
Could this actually be a bug in our handling of "if"? What should happen is
range :: Int -> Int -> Void -- starting point
if :: Bool -> Void -> List Void -> List Void -- first pass through
body of range
range :: Int -> Int -> List Void -- second range iteration
if :: Bool -> List Int -> List Void -> List Int -- second body iteration
range :: Int -> Int -> List Int -- convergence
Which step is breaking? This might be another symptom of the freezing issue.
Geoffrey
We never make it this far, because "apply (if Bool) Void" is immediately
determined to be Void, and then "apply Void (List Void)" is still Void, so we
never make it to the second argument. According to what you're saying, "apply
_ Void" should still create the closure, and perhaps other things too.
Yeah, that means this is a bug in the Delay code. It isn't true that
"f (Delayed Void) = Void", so at some point we're checking argType
when we should be checking the other one (or vis versa). The Void
return type was correct before we introduced the delay feature, since
range would unconditionally never return.
Geoffrey
Yep, this is what I meant. Cool.
I fixed the inference bug, so now only one line in base-test.duck is
commented out. I also added a dedicated failure test to exercise the
new fixpoint behavior.
Geoffrey
Now no more lines commented out, and much saner Delayed handling (on my
github).
:-Dylan
Very cool. Nice that the PTrie annotations moved to edges. I also
like the appearance of "undefined" in Interp, since it will vanish
happily once TValues disappear.
Geoffrey