Open hyphenrf opened 2 weeks ago
The termination checker only looks for structurally smaller arguments. Working up to "matching constructors with structurally smaller arguments" would actually be a very simple change: sizeCompareCon
needs to recurse on arguments when s
and t
start with the same constructor.
Should I attempt this addition then? I'll happily prepare a PR
Should I attempt this addition then? I'll happily prepare a PR
You definitely should!
I had looked into this over the last two days and the logic is working, but I ran into a snag (you have to apply the change below for the test to pass, but then perf003 fails):
https://github.com/idris-lang/Idris2/compare/main...dunhamsteve:Idris2:total2?expand=1
The rule I'm using is:
Constructor matches, all arguments are either equal or smaller, and at least one is smaller. So no Unknown
allowed. I believe you can sneak in bigger values if you allow Unknown
arguments to the constructor.
The issue I hit is that there are some metas in a case like Just (xs) < Just (x :: xs)
(At Maybe (List a)
) The meta is solved but the normalization isn't substituting the result in. (So it is Unknown
when comparing against the one in the pattern.) If I change the tcOnly
normalization from withArgHoles
to withHoles
in Value.idr
it all works great:
tcOnly : EvalOpts
-tcOnly = { tcInline := True } withArgHoles
+tcOnly = { tcInline := True } withHoles
But the perf003
test never finishes. So I've got a performance regression.
The only difference between argHolesOnly
and holesOnly
that I can find is in Eval.idr
around line 500, and it looks like it's exactly the case of an erased argument that argHolesOnly
suppresses.
@dunhamsteve, just a guess: maybe you should try what you are doing upon #3272
It looks like the issue is in the normalization itself. I took out all of my changes and added one very targeted change:
findCalls defs (_ ** (env, lhs, rhs_in))
= do let pargs = getArgs (delazy defs lhs)
- rhs <- normaliseOpts tcOnly defs env rhs_in
+ rhs <- logTime 1 "tcOnly" $ normaliseOpts ({ holesOnly := True} tcOnly) defs env rhs_in
findSC defs env Toplevel pargs (delazy defs rhs)
The test looks like:
0 IdType : Type
IdType = {0 a : Type} -> a -> a
id : IdType
id = \ x : _ => x
idid : {0 a : Type} -> a -> a
idid = id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
id id id id id id id id id id
It's exponential in the number of id
, each additional id
doubles the time logged:
ids | ms | |
---|---|---|
20 | 1101 | |
21 | 2198 | 1.996 |
22 | 4371 | 1.988 |
23 | 8733 | 1.998 |
24 | 17574 | 2.012 |
25 | 35374 | 2.013 |
26 | 72390 | 2.046 |
Aside from the test though, the totality checking works well. :)
(And building idris2api.ipkg
does not slow down with that change.)
The length of the largest implicit argument a
doubles with each additional id
so once you start inlining the corresponding meta-variable(s) the size of the overall term blows up exponentially.
There are some real code bases where this behaviour occurs naturally so inlining all solved meta-variables for termination checking is unlikely to be feasible.
Before #2977 was merged, I was traversing meta-variable solutions during termination checking and that seemed to be fast enough. Sadly, I can't find that code right now but it would be easy enough to reproduce.
I think I've got the meta traversal working right and updated the branch.
It's passing my tests and perf003
. I had to wire defs
and the Core
monad into some of the code. I kept it out of sizeEq
because it was passed to a HOF, and did the expansion in compareSize
instead. I'm only expanding metas on the RHS and letting sizeEq
handle Meta/Meta comparison. (Do metas show up in patterns? Maybe inside dotted expressions?)
The time for a full idris2api
compilation doesn't seem affected by this change, and the perf003
test time seems the same too.
One thing I did do for expediency is consider type constructor applications to be the Same
quantity without digging into arguments. I could run them through the same process as data constructors if this is an issue.
Steps to Reproduce
I was trying this with a simple list and a NonEmpty predicate, but here's a minimal example without it:
It's possible to prove this terminates with
Control.WellFounded
, however, add some complexity going back to my original attempt:and it fails with a couple of strange error messages which I highlight below.
Expected Behavior
Idris can see that
xs
is in fact smaller than_::xs
, without much intervention from my side. Also whatever caused the strange error messages in wellfounded approach be addressed.Observed Behavior
First (simple) attempt:
A sprinkle of
WellFounded
makes Idris happy again.Second (more complex) attempt:
S (...)
, it fails highlightingx::xs
and complaining:Error: With clause does not match parent
S $ ...
or1 + ...
and a better(?) error message emerges, about both branches missing holes that need to be filled, I abbreviated the error messages, taking note to keep only the^^^
-highlighted section of the code:... I feel like that should be a bug report on its own?
Circumvention:
Extra Notes:
I asked this question on an Idris community channel before filing the bug report. Initial reactions were confused. There were suggestions that the totality checker simply makes no attempt to follow function/constructor applications. That made sense to me for functions but not for constructors (in my mind there's nothing preventing that, they're trivially reducible, and the compiler should at least easily know about
List
, in fact it has aSized
instance for it by default). However, more interestingly:in both cases we have a constructor, but in one case it's "shared" structure, while in the other it's "new". Comparing list lengths should remove that distinction... and I'm not sure if this is the core issue here or just another observed behavior.
Moreover, the fact that
NonEmpty
is an auto-implicit changes nothing about the above, at least as far as I can tell. I tried different variants of the declaration.