search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.18k stars 134 forks source link

No decreasing parameter even though constructor is unwrapped #2281

Open jvanbruegge opened 4 months ago

jvanbruegge commented 4 months ago

This simple size function throws an error even though I only use the fields of the datatype and not re-wrap them:

data Tree a = MkTree a [Tree a]

size :: Tree a -> Int
size (MkTree _ xs) = 1 + foldr ((+) . size) 0 xs
facundominguez commented 3 months ago

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 WARNING: Found false in Test.hs:...

nikivazou commented 3 months ago

The alternative also has a termination error. I do not know of a way to prove termination is such cases. The definition is not structurally terminating (thus the structural termination checker fails) and you cannot use any termination metric (since this is what you are defining)... I suggest you just deactivate the termination checker for size using {-@ lazy size@-}.

clayrat commented 3 months ago

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 foldr) defined mutually with the function where you're using it; of course, this is not ideal because of code duplication. See also various treatments of the mirror function on nested trees in Bove, Krauss, Sozeau, [2012] "Partiality and Recursion in Interactive Theorem Provers - An Overview"

facundominguez commented 3 months ago

The alternative also has a termination error.

And it is a bug that Liquid Haskell does not report it. Right?

nikivazou commented 3 months ago

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.