-
Notifications
You must be signed in to change notification settings - Fork 135
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
No decreasing parameter even though constructor is unwrapped #2281
Comments
Hello @jvanbruegge. I'm guessing that this is a limitation of the termination checker indeed. Perhaps @nikivazou can comment on how difficult it would be to make it work. This alternative definition seems to work. size :: Tree a -> Int
size (MkTree _ xs) = 1 + listSize xs
listSize :: [Tree a] -> Int
listSize xss = foldr (\(MkTree _ xs) s -> s + listSize xs) 0 xss although it gives some warnings in the console |
The alternative also has a termination error. |
Proving termination for functions defined on nested types is indeed often tricky in type theory, the typical advice in such a case is to have a specialized version of the higher-order function that you pass the result of the recursive call to (here |
And it is a bug that Liquid Haskell does not report it. Right? |
There is no bug. It reports an error. Not termination error, but the reported error is generated because LH cannot prove termination. |
This simple
size
function throws an error even though I only use the fields of the datatype and not re-wrap them:The text was updated successfully, but these errors were encountered: