HasCallStack interferes with termination checking

[facundominguez]

The following file fails to verify

module Test where

import Language.Haskell.Liquid.Prelude (liquidError)
import GHC.Stack

{-@ myhead :: {xs:[a] | len xs > 0} -> a @-}
myhead :: HasCallStack => [a] -> a
myhead (x:_) = x

{-@ type PosInt = {v: Int | v > 0 } @-}
{-@ type List a N = {v : [a] | (len v) = N} @-}
{-@ type Matrix a Rows Cols  = (List (List a Cols) Rows) @-}
{-@ transpose                :: c:Int -> r:PosInt -> Matrix a r c -> Matrix a c r @-}

transpose                    :: Int -> Int -> [[a]] -> [[a]]
transpose 0 _ _              = []
transpose c r ((x:xs) : xss) = (x : map myhead xss) : transpose (c-1) r (xs : map tail xss)
transpose c r ([] : _)       = liquidError "dead code"
transpose c r []             = liquidError "dead code"

gives the error

test.hs:18:1: error:
    Termination Error
HasCallStackTest.transpose
No decreasing parameter
   |
18 | transpose 0 _ _              = []
   | ^^^^^^^^^

A similar error is obtained if the liquidError calls are replaced with calls to error.

I found this when upgrading to ghc-9.4 in #2234, as head starts using HasCallStack in the corresponding version of base.

[facundominguez]

This seems to happen because HasCallStack causes some let declarations to be introduced with location information.

transpose
  = \ (@a_aUS) ->
      let {
        $dIP_aV7 :: HasCallStack
        [LclId,
         Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=False,
                 WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 300 0}]
        $dIP_aV7
          = (pushCallStack
               (GHC.CString.unpackCString# "myhead"#,
                GHC.Stack.Types.SrcLoc
                  (GHC.CString.unpackCString# "main"#)
                  (GHC.CString.unpackCString# "HasCallStackTest"#)
                  (GHC.CString.unpackCString# "test.hs"#)
                  (GHC.Types.I# 19#)
                  (GHC.Types.I# 41#)
                  (GHC.Types.I# 19#)
                  (GHC.Types.I# 47#))
               emptyCallStack)
            `cast` (Sym (GHC.Classes.N:IP[0] <"callStack">_N <CallStack>_N)
                    :: CallStack ~R# (?callStack::CallStack)) } in
      \ (ds_d1RB :: Int) (ds_d1RC :: Int) (ds_d1RD :: [[a_aUS]]) ->
        src<test.hs:(18,1)-(21,54)>
        case ds_d1RB of { GHC.Types.I# ds_d1RN ->
        case ds_d1RN of {
        ...

When A normalization transforms this term, it inserts new let declarations before the type binder

transpose
   = \ (@a) ->
       (let {
          lq_anf$##7205759403792800809 :: GHC.Prim.Addr#
          [LclId]
          lq_anf$##7205759403792800809 = "myhead"# }
         in let ...
         in
         \ (@a)
          (ds_d1RB :: GHC.Types.Int)
          (ds_d1RC :: GHC.Types.Int)
          (ds_d1RD :: [[a]]) ->
          src<test.hs:(18,1)-(21,54)>
          case ds_d1RB of lq_anf$##7205759403792800828
            ...
       ) @a

and now the termination checker is confused because a type binder occurs at the beginning of the term, and then again after the multiple let declarations.

I'm contributing a fix in #2236 to have A normalization produce instead

transpose
   = \ (@a) ->
       let {
          lq_anf$##7205759403792800809 :: GHC.Prim.Addr#
          [LclId]
          lq_anf$##7205759403792800809 = "myhead"# }
         in let ...
         in
          \
          (ds_d1RB :: GHC.Types.Int)
          (ds_d1RC :: GHC.Types.Int)
          (ds_d1RD :: [[a]]) ->
          src<test.hs:(18,1)-(21,54)>
          case ds_d1RB of lq_anf$##7205759403792800828
            ...

which seems to fix the issue.