fold inference bug
Geoffrey Irving
through apply. Consider
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
Dylan Alex Simon
> 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.
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
Dylan Alex Simon
unable to infer recursive function types at all. If this is the case, we
should at least catch it somehow, though it does seem an annoying restriction.
I vaguely remember you talking about this at some point.
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
Geoffrey Irving
> of "ambiguous f Void" calls. Hrm.
"(:) 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
Dylan Alex Simon
>
> On Sun, Aug 30, 2009 at 3:07 PM, Dylan Alex Simon<dy...@dylex.net> wrote:
> >> The second bug may not actually be a bug per se, but just that we are
> >> should at least catch it somehow, though it does seem an annoying restriction.
> >> I vaguely remember you talking about this at some point.
> >>
> >>
> >> ? ? ? ? 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
> >> "List a". ?In fact, just removing this second "apply" rule makes this case
> >> work fine. ?Is that the right thing to do?
> >
> > Oh, well clearly it's not because it breaks other things and introduces a lot
>
> "(:) 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
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.
Geoffrey Irving
>> 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
>
> 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
Geoffrey Irving
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
Dylan Alex Simon
> commented out. I also added a dedicated failure test to exercise the
> new fixpoint behavior.
Now no more lines commented out, and much saner Delayed handling (on my
github).
:-Dylan
Geoffrey Irving
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