zipWith throws NonTermination exception

[mirpa29]

Describe the bug
If I define Fibonacci sequence and use zipWith from linear-base, it throws exception starting at 3rd number

euler-hs-linear: Uncaught exception ghc-internal:GHC.Internal.Control.Exception.Base.NonTermination:
<<loop>>

I reduced my code to

import Data.Word
import qualified Data.List.Linear as Linear
import qualified Data.Num.Linear as Linear
import Data.Unrestricted.Linear (Consumable, lseq)

test :: Word32
test = fib !! 2
  where
    fib = 1 : 2 : Linear.zipWith (Linear.+) fib (tail fib)

-- my implementation of linear zipWith
linZipWith ∷ (Consumable a, Consumable b) ⇒ (a ⊸ b ⊸ c) → [a] ⊸ [b] ⊸ [c]
linZipWith _ [] ys = ys `lseq` []
linZipWith _ xs [] = xs `lseq` []
linZipWith f (x:xs) (y:ys) = f x y : linZipWith f xs ys

To Reproduce
Using index greater than 1 into fib will throw exception.

Expected behavior
I expected type error, if any. My implementation linZipWith works fine, no type errors, no exception.

Environment
ghc 9.12.2
linear-base 0.5

Additional context
I have no experience with Linear Types. I wanted to try it in some simple code.

[aspiwack]

Good find.

Your implementation of linear zipWith would not loop this way. We've been lazy and implemented zipWith in terms of zipWith' which is stricter. I'll fix this in the coming days.

[aspiwack]

Sorry, I let this be buried.

I'm trying to figure out how I want to tackle this, right now.

As it happens, the reason why zipWith' is stricter than zip is because its type is somewhat wrong. We'd really want something like

data LOList r a
  = Nil r
  | Cons a (LOList r a)

zipWith' :: (a %1 -> b %1 -> c) -> [a] %1 -> [b] %1 -> LOList (Maybe (Either (NonEmpty a) (NonEmpty b))) c

With such a type, the computation of the leftovers are delayed to after the list has been exhausted.

Without linear type, we can give a function from LOList r a -> ([a], r) which preserves laziness (but ultimately traverses the LOList twice). But linear types prevent this. So it's an unnecessary behaviour of zipWith' but a necessary consequence of the type we've chosen for it which gives this behaviour.

It's, of course, trivial to fix for zipWith proper. But it got me thinking.

[aspiwack]

I think I'm going to go for the approach in #492. A single implementation based on continuations, the strictness of zipWith' is clarified and hopefully more obvious to identify.

[aspiwack]

(continuations is a bit of a misnomer there probably, it's in catamorphism form? Sort of and impredicative encoding. It's, at least, certainly not in CPS)