Confusing behavior with replacePreds

[gridaphobe]

@nikivazou here's a fairly minimal example of the issue I'm having with predicate instantiation (https://gist.github.com/gridaphobe/b2750b53f26768e3f519).

ghci> t
RApp { rt_tycon = List
     , rt_args = [RApp { rt_tycon = Int
                       , rt_args = []
                       , rt_pargs = []
                       , rt_reft = U { ur_reft = VV : []
                                     , ur_pred = Pr [PV { pname = "p"
                                                        , ptype = PVProp ()
                                                        , parg = "_LIQUID_dummy"
                                                        , pargs = [((),"lq_tmp_db2",EVar "x")]}], ur_strata = []}}]
     , rt_pargs = [RProp { rf_args = [("lq_tmp_db2",RApp {rt_tycon = Int, rt_args = [], rt_pargs = [], rt_reft = ()})]
                         , rf_body = RApp { rt_tycon = Int, rt_args = [], rt_pargs = [], rt_reft = U {ur_reft = VV : [], ur_pred = Pr [PV {pname = "p", ptype = PVProp (), parg = "_LIQUID_dummy", pargs = [((),"lq_tmp_db2",EVar "lq_tmp_db2")]}], ur_strata = []}}}], rt_reft = U {ur_reft = VV : [], ur_pred = Pr [], ur_strata = []}}

ghci> su
[( PV {pname = "p", ptype = PVProp (RVar {rt_var = a, rt_reft = ()}), parg = "_LIQUID_dummy", pargs = [(RVar {rt_var = a, rt_reft = ()},"lq_tmp_db2",EVar "lq_tmp_db2")]}
 , RProp { rf_args = [("x5",RApp { rt_tycon = Int, rt_args = [], rt_pargs = [], rt_reft = ()})]
         , rf_body = RApp {rt_tycon = Int, rt_args = [], rt_pargs = [], rt_reft = U {ur_reft = VV : [(x5 < VV)], ur_pred = Pr [], ur_strata = []}}})]

ghci> replacePreds "bad" t su
RApp { rt_tycon = List
     , rt_args = [RApp { rt_tycon = Int
                       , rt_args = []
                       , rt_pargs = []
                       , rt_reft = U { ur_reft = VV : [(x < VV)]
                                     , ur_pred = Pr []
                                     , ur_strata = []}}]
     , rt_pargs = [RProp { rf_args = [("x5",RApp {rt_tycon = Int, rt_args = [], rt_pargs = [], rt_reft = ()})
                                     ,("lq_tmp_db2",RApp {rt_tycon = Int, rt_args = [], rt_pargs = [], rt_reft = ()})]
                         , rf_body = RApp {rt_tycon = Int, rt_args = [], rt_pargs = [], rt_reft = U {ur_reft = VV : [(x5 < VV)], ur_pred = Pr [], ur_strata = []}}}], rt_reft = U {ur_reft = VV : [], ur_pred = Pr [], ur_strata = []}}

Note that after replacePreds the predicate takes two arguments. If I understand correctly, "lq_tmp_db2" should not be an argument after the substitution.

[nikivazou]

@gridaphobe , is this still open?

[gridaphobe]

Yes, I reverted the commit that caused the issue, but that's not a proper fix, as we now have RPropPs floating around after Bare.