Improve syntactic analysis for impossible cases in lifted functions

[sdleffler]

I'm trying to lift head, using {-@ measure head @-}. head is defined as follows:

{-@ head :: NEList a -> a @-}
head                    :: [a] -> a
head (x:_)              =  x
head []                 =  errorEmptyList "head"
{-# NOINLINE [1] head #-}

This does not work, because currently, eliminating impossible cases from the lifted function is done by a simple syntactic analysis pass looking for Control.Exception.Base.patError. As a stopgap it would be possible to add GHC.Err.errorWithoutStackTrace so that errorEmptyList could be lifted:

{-@ errorEmptyList :: Impossible String -> a @-}
errorEmptyList :: String -> a
errorEmptyList fun =
  errorWithoutStackTrace (prel_list_str ++ fun ++ ": empty list")

Another symptom of this problem is that

head (x:_) = x

is correctly lifted into the logic, but

head (x:_) = x
head [] = myerror ""

myerror = Control.Exception.Base.patError

is not, because only a shallow syntactic check is done.

link to demo

[ranjitjhala]

Hmm. So is the issue here that the code

head (x:_) = x 

generates core that is easily liftable (i.e. supported by the current implementation), but

head (x:_) = x 
head []   = _throw_some_custom_error

does not?

[sdleffler]

Yes, that's the gist of it. Especially, this will work:

head (x:_) = x
head [] = Control.Exception.Base.patError

It's a simple syntactic check to see if the immediate expression is one of a specific set of error functions, so it won't catch it if you create another function which, if substituted in, is one of this specific error functions.

[sdleffler]

Link to a demo showing this: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1506546435_3997.hs