Why not auto-reflect functions as needed?

[yanhasu]

Issue #1285 suggests merging inline and measure into reflect to increase user-friendliness.

Why not go one step further and get rid of reflect too, by automatically reflecting functions that are used in the refinement logic (and their transitive dependencies)?

e.g. in the following example,

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}

{-@ trivialPalindrome :: {v:String | myRev v = v} @-}
trivialPalindrome = ""

myRev :: [a] -> [a]
myRev []     = []
myRev (x:xs) = myApp (myRev xs) [x]

myApp :: [a] -> [a] -> [a]
myApp []     ys = ys
myApp (x:xs) ys = x:(myApp xs ys)

myLen :: [a] -> Int
myLen [] = 0
myLen (_:xs) = 1 + myLen xs

Both myRev and myApp would both auto-reflected (or made into measures, as per #1748), but myLen would not be.

Currently, the user needs to reflect (or measure or inline) these functions anyway, so totality checking shouldn't cause any new issues.

Benefits of automating reflection include:

• A simpler explanation of what can go in the refinement logic: "any terminating expression" vs."arithmetic & measures & reflected functions".
• Clearer error messages: "couldn't prove X terminating"+dependency trace vs. "symbol X not found"

[plredmond]

I think it would be great if everything was auto-reflected :heavy_plus_sign:

But.. Currently reflection has some bad interactions with module exports and hierarchies... Namely, your modules have to expose all the symbols which are part of any reflected definitions.. So if module A imports module B, and then module A reflects a definition aFun which uses a definition from module B, bFun, you end up in a situation where users of the reflected aFun need to import module B.. this is odd and I might be explaining it wrong