Termination checker tripped up by ($)

The following module is accepted by LH:

{-# LANGUAGE GADTs, DataKinds, TypeOperators, KindSignatures #-}
module Main where

import GHC.TypeLits
import Unsafe.Coerce

-- See https://github.com/ucsd-progsys/liquidhaskell/issues/2095
workaround :: (n1 + 1) ~ (n2 + 1) => Vec n1 a -> Vec n2 a
workaround = unsafeCoerce

data Vec (n :: Nat) a where
    Nil :: Vec 0 a
    Cons :: a -> Vec n a -> Vec (n + 1) a

foo :: Vec n a -> Vec n a -> Vec n a
foo Nil Nil = Nil
foo (Cons x xs) (Cons y ys) = Cons x zs
  where
    zs = foo xs (workaround ys)
foo _ _ = undefined

However, changing the definition of foo slightly, to:

foo :: Vec n a -> Vec n a -> Vec n a
foo Nil Nil = Nil
foo (Cons x xs) (Cons y ys) = Cons x zs
  where
    zs = foo xs $ workaround ys
foo _ _ = undefined

(note the difference in the binding of zs), suddenly LH doesn't see that foo terminates:

/home/cactus/prog/haskell/liquid-haskell/bugs/gadt-rec/src/main.hs:16:1: error:
    Termination Error
Main.foo
No decreasing parameter
   |
16 | foo Nil Nil = Nil
   | ^^^

ucsd-progsys / liquidhaskell

Termination checker tripped up by ($) #2096