Related to issue #2319, in this PR we fully qualify symbols when transforming CoreExpr into Expr of the logic so we don't mistake builtin symbols with functions defined by the user (see example in the issue).

Worth mentioning, it means that this does not pass verification:

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

module Inc00 where

import Prelude hiding (not)

{-@ reflect not @-}
not :: Bool -> Bool
not a = a

{-@ lemma :: {not True} @-}
lemma = ()

If you want to refer to your reflected functions that clash with builtin symbols of the logic, you have to fully qualify them:

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

module Inc00 where

import Prelude hiding (not)

{-@ reflect not @-}
not :: Bool -> Bool
not a = a

{-@ lemma :: {Inc00.not True} @-}
lemma = ()

So that there's no ambiguity. Without qualification, we assume not (or the like) to refer to the builtin symbols from the logic.

Any comments welcome!