LetRecStack.hs

{-@ LIQUID "--eliminate=all" @-}

-- | This test case is to check that LH properly accounts for the case where GHC Core
--   contains stuff like:
--   foo :: T
--   foo =
--     let t1 = e1
--         t2 = e2
--         ...
--         tn = en
--     in
--     let rec bar = e
--     in
--       bar
--
--  where `T` is a liquid type specification. This sort of stuff is introduced by GHC8
--  in order to manage the implicit `CallStack` parameters, but it ends up generating
--  extra KVars where none are needed (as we already have the signature.)

{-@ LIQUID "--no-termination" @-}

module Foo (foo) where

die :: String -> a
die = error

--data Peano a = Z a | S (Peano a) | P (Peano a)
data Peano = Z | S (Peano ) | P (Peano)

{-@ foo :: Peano -> Nat @-}
foo :: Peano -> Int
foo =
  let t0 = 0
      t1 = 1
  in
  let baz p = case p of
                Z   -> t0
                S p -> t1 + baz p
                P p -> die ms
              where
                ms = "yikes"
  in
    baz