content: -- | This module has the code that uses the GHC definitions to:
  --   1. MAKE a name-resolution environment,
  --   2. USE the environment to translate plain symbols into Var, TyCon, etc.
  
  {-# LANGUAGE OverloadedStrings     #-}
  {-# LANGUAGE FlexibleContexts      #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE ScopedTypeVariables   #-}
  {-# LANGUAGE PartialTypeSignatures #-}
  {-# LANGUAGE ConstraintKinds       #-}
  {-# LANGUAGE TupleSections         #-}
  
  module Language.Haskell.Liquid.Bare.Resolve
    ( -- * Creating the Environment
      makeEnv
    , makeLocalVars
    , makeGHCTyLookupEnv
    , GHCTyLookupEnv(..)
  
      -- * Resolving symbols
    , Lookup
  
    -- * Looking up names
    , lookupGhcDataConLHName
    , lookupGhcDnTyCon
    , lookupGhcIdLHName
    , lookupLocalVar
    , lookupGhcTyConLHName
    , lookupGhcTyThingFromName
    , lookupGhcId
  
    -- * Checking if names exist
    , knownGhcType
  
    -- * Misc
    , coSubRReft
    , unQualifySymbol
  
    -- * Conversions from Bare
    , ofBareTypeE
    , ofBareType
    , ofBPVar
  
    -- * Post-processing types
    , txRefSort
    , errResolve
  
    -- * Fixing local variables
    , resolveLocalBinds
    , partitionLocalBinds
    ) where
  
  import qualified Control.Exception                 as Ex
  import           Data.Bifunctor (first)
  import           Data.Function (on)
  import           Data.IORef (newIORef)
  import qualified Data.List                         as L
  import qualified Data.HashSet                      as S
  import qualified Data.Maybe                        as Mb
  import qualified Data.HashMap.Strict               as M
  import           GHC.Stack
  import           Text.Megaparsec.Pos (sourceColumn, sourceLine)
  import qualified Text.PrettyPrint.HughesPJ         as PJ
  
  import qualified Language.Fixpoint.Types               as F
  import qualified Language.Fixpoint.Types.Visitor       as F
  import qualified Language.Fixpoint.Misc                as Misc
  import qualified Liquid.GHC.API       as Ghc
  import qualified Language.Haskell.Liquid.GHC.Interface as Interface
  import qualified Language.Haskell.Liquid.GHC.Misc      as GM
  import qualified Language.Haskell.Liquid.Misc          as Misc
  import           Language.Haskell.Liquid.Types.DataDecl
  import           Language.Haskell.Liquid.Types.Errors
  import           Language.Haskell.Liquid.Types.Names
  import           Language.Haskell.Liquid.Types.RType
  import           Language.Haskell.Liquid.Types.RTypeOp
  import qualified Language.Haskell.Liquid.Types.RefType as RT
  import           Language.Haskell.Liquid.Types.Types
  import           Language.Haskell.Liquid.Types.Specs
  import           Language.Haskell.Liquid.Types.Visitors
  import           Language.Haskell.Liquid.Bare.Types
  import           Language.Haskell.Liquid.UX.Config
  import           System.IO.Unsafe (unsafePerformIO)
  
  myTracepp :: (F.PPrint a) => String -> a -> a
  myTracepp = F.notracepp
  
  -- type Lookup a = Misc.Validate [Error] a
  type Lookup a = Either [Error] a
  
  -------------------------------------------------------------------------------
  -- | Creating an environment
  -------------------------------------------------------------------------------
  makeEnv :: Config -> GHCTyLookupEnv -> [Ghc.Id] -> Ghc.TcGblEnv -> Ghc.InstEnvs -> LocalVars -> GhcSrc -> LogicMap -> [(ModName, BareSpec)] -> Env
  makeEnv cfg ghcTyLookupEnv dataConIds tcg instEnv localVars src lmap specs = RE
    { reTyLookupEnv = ghcTyLookupEnv
    , reTcGblEnv  = tcg
    , reInstEnvs = instEnv
    , reUsedExternals = usedExternals
    , reLMap      = lmap
    , reDataConIds = dataConIds
    , reLocalVars = localVars
    , reSrc       = src
    , reGlobSyms  = S.fromList     globalSyms
    , reCfg       = cfg
    }
    where
      globalSyms  = concatMap getGlobalSyms specs
      usedExternals = Ghc.orphNamesOfExprs $ map snd $ Ghc.flattenBinds $ _giCbs src
  
  getGlobalSyms :: (ModName, BareSpec) -> [F.Symbol]
  getGlobalSyms (_, spec)
    = filter (not . GM.isQualifiedSym)
         $ (mbName <$> measures  spec)
        ++ (mbName <$> cmeasures spec)
        ++ (mbName <$> imeasures spec)
        ++ (mbName <$> omeasures spec)
    where
      mbName = lhNameToResolvedSymbol . F.val . msName
  
  makeLocalVars :: [Ghc.CoreBind] -> LocalVars
  makeLocalVars = localVarMap . localBinds
  
  -- TODO: rewrite using CoreVisitor
  localBinds :: [Ghc.CoreBind] -> [LocalVarDetails]
  localBinds                    = concatMap (bgoT [])
    where
      bgoT g (Ghc.NonRec _ e) = go g e
      bgoT g (Ghc.Rec xes)    = concatMap (go g . snd) xes
      pgo g isRec (x, e)      = mkLocalVarDetails g isRec x : go g e
      bgo g (Ghc.NonRec x e)  = pgo g False (x, e)
      bgo g (Ghc.Rec xes)     = concatMap (pgo g True) xes
      go g (Ghc.App e a)       = concatMap (go g) [e, a]
      go g (Ghc.Lam x e)       = go (x:g) e
      go g (Ghc.Let b e)       = bgo g b ++ go (Ghc.bindersOf b ++ g) e
      go g (Ghc.Tick _ e)      = go g e
      go g (Ghc.Cast e _)      = go g e
      go g (Ghc.Case e _ _ cs) = go g e ++ concatMap (\(Ghc.Alt _ bs e') -> go (bs ++ g) e') cs
      go _ (Ghc.Var _)         = []
      go _ _                   = []
  
      mkLocalVarDetails g isRec v = LocalVarDetails
        { lvdSourcePos = F.sp_start $ F.srcSpan v
        , lvdVar = v
        , lvdLclEnv = g
        , lvdIsRec = isRec
        }
  
  localVarMap :: [LocalVarDetails] -> LocalVars
  localVarMap lvds =
      LocalVars
        { lvSymbols = Misc.group
            [ (x, lvd)
            | lvd <- lvds
            , let v = lvdVar lvd
                  x = F.symbol $ Ghc.occNameString $ Ghc.nameOccName $ Ghc.varName v
            ]
        , lvNames = Ghc.mkNameEnvWith (Ghc.getName . lvdVar) lvds
        }
  
  makeGHCTyLookupEnv :: Ghc.CoreProgram -> Ghc.TcRn GHCTyLookupEnv
  makeGHCTyLookupEnv cbs = do
      hscEnv <- Ghc.getTopEnv
      session <- Ghc.Session <$> Ghc.liftIO (newIORef hscEnv)
      tcg <- Ghc.getGblEnv
        -- Types differ in tcg_type_env vs the core bindings though they seem to
        -- be alpha-equivalent. We prefer the type in the core bindings and we
        -- also include the types of local variables.
      let varsEnv = Ghc.mkTypeEnv $ map Ghc.AnId $ letVars cbs
          typeEnv = Ghc.tcg_type_env tcg `Ghc.plusTypeEnv` varsEnv
      return GHCTyLookupEnv
        { gtleSession = session
        , gtleTypeEnv = typeEnv
        }
  
  localKey   :: Ghc.Var -> Maybe F.Symbol
  localKey v
    | isLocal m = Just x
    | otherwise = Nothing
    where
      (m, x)    = splitModuleNameExact . GM.dropModuleUnique . F.symbol $ v
  
  isLocal :: F.Symbol -> Bool
  isLocal = isEmptySymbol
  
  isEmptySymbol :: F.Symbol -> Bool
  isEmptySymbol x = F.lengthSym x == 0
  
  -- | @lookupLocalVar@ takes as input the list of "global" (top-level) vars
  --   that also match the name @lx@; we then pick the "closest" definition.
  --   See tests/names/pos/LocalSpec.hs for a motivating example.
  
  lookupLocalVar :: F.Loc a => LocalVars -> LocSymbol -> [a] -> Maybe (Either a Ghc.Var)
  lookupLocalVar localVars lx gvs = findNearest lxn kvs
    where
      kvs                   = prioritizeRecBinds (M.lookupDefault [] x (lvSymbols localVars)) ++ gs
      gs                    = [(F.sp_start $ F.srcSpan v, Left v) | v <- gvs]
      lxn                   = F.sp_start $ F.srcSpan lx
      (_, x)                = unQualifySymbol (F.val lx)
  
      -- Sometimes GHC produces multiple bindings that have the same source
      -- location. To select among these, we give preference to the recursive
      -- bindings which might need termination metrics.
      prioritizeRecBinds lvds =
        let (recs, nrecs) = L.partition lvdIsRec lvds
         in map lvdToPair (recs ++ nrecs)
      lvdToPair lvd = (lvdSourcePos lvd, Right (lvdVar lvd))
  
      findNearest :: F.SourcePos -> [(F.SourcePos, b)] -> Maybe b
      findNearest key kvs1 = argMin [ (posDistance key k, v) | (k, v) <- kvs1 ]
  
      -- We prefer the var with the smaller distance, or equal distance
      -- but left of the spec, or not left of the spec but below it.
      posDistance a b =
        ( abs (F.unPos (sourceLine a) - F.unPos (sourceLine b))
        , sourceColumn a < sourceColumn b -- Note: False is prefered/smaller to True
        , sourceLine a > sourceLine b
        )
  
      argMin :: (Ord k) => [(k, v)] -> Maybe v
      argMin = Mb.listToMaybe . map snd . L.sortBy (compare `on` fst)
  
  
  lookupGhcDnTyCon :: Env -> ModName -> DataName -> Lookup (Maybe Ghc.TyCon)
  lookupGhcDnTyCon env name = failMaybe env name . lookupGhcDnTyConE env
  
  lookupGhcDnTyConE :: Env -> DataName -> Lookup Ghc.TyCon
  lookupGhcDnTyConE env (DnCon  lname)
    = Ghc.dataConTyCon <$> lookupGhcDataConLHName env lname
  lookupGhcDnTyConE env (DnName lname)
    = do
     case lookupTyThing (reTyLookupEnv env) lname of
       Ghc.ATyCon tc -> Right tc
       Ghc.AConLike (Ghc.RealDataCon d) -> Right $ Ghc.dataConTyCon d
       _ -> panic
             (Just $ GM.fSrcSpan lname) $ "not a type or data constructor: " ++ show (val lname)
  
  lookupGhcDataConLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.DataCon
  lookupGhcDataConLHName env lname = do
     case lookupTyThing (reTyLookupEnv env) lname of
       Ghc.AConLike (Ghc.RealDataCon d) -> Right d
       _ -> panic
             (Just $ GM.fSrcSpan lname) $ "not a data constructor: " ++ show (val lname)
  
  lookupGhcIdLHName :: HasCallStack => Env -> Located LHName -> Lookup Ghc.Id
  lookupGhcIdLHName env lname =
     case lookupTyThing (reTyLookupEnv env) lname of
       Ghc.AConLike (Ghc.RealDataCon d) -> Right (Ghc.dataConWorkId d)
       Ghc.AnId x -> Right x
       _ -> panic
             (Just $ GM.fSrcSpan lname) $ "not a variable or data constructor: " ++ show (val lname)
  
  lookupGhcTyThingFromName :: GHCTyLookupEnv -> Ghc.Name -> Maybe Ghc.TyThing
  -- see note about unsafePerformIO in lookupTyThingMaybe
  lookupGhcTyThingFromName env n =
     unsafePerformIO $ Ghc.reflectGhc (Interface.lookupTyThing (gtleTypeEnv env) n) (gtleSession env)
  
  lookupGhcId :: Env -> Ghc.Name -> Maybe Ghc.Id
  lookupGhcId env n =
      case lookupGhcTyThingFromName env' n of
        Just (Ghc.AConLike (Ghc.RealDataCon d)) -> Just (Ghc.dataConWorkId d)
        Just (Ghc.AnId x) -> Just x
        _ -> Nothing
    where
      env' = reTyLookupEnv env
  
  -------------------------------------------------------------------------------
  -- | Checking existence of names
  -------------------------------------------------------------------------------
  knownGhcType :: Env -> LocBareType -> Bool
  knownGhcType env (F.Loc l _ t) =
    case ofBareTypeE env l Nothing t of
      Left e  -> myTracepp ("knownType: " ++ F.showpp (t, e)) False
      Right _ -> True
  
  
  
  _rTypeTyCons :: (Ord c) => RType c tv r -> [c]
  _rTypeTyCons        = Misc.sortNub . foldRType f []
    where
      f acc t@RApp {} = rt_tycon t : acc
      f acc _         = acc
  
  -- | `unQualifySymbol name sym` splits `sym` into a pair `(mod, rest)` where
  --   `mod` is the name of the module, derived from `sym` if qualified.
  unQualifySymbol :: F.Symbol -> (Maybe F.Symbol, F.Symbol)
  unQualifySymbol sym
    | GM.isQualifiedSym sym = first Just (splitModuleNameExact sym)
    | otherwise             = (Nothing, sym)
  
  splitModuleNameExact :: F.Symbol -> (F.Symbol, F.Symbol)
  splitModuleNameExact x' = myTracepp ("splitModuleNameExact for " ++ F.showpp x)
                            (GM.takeModuleNames x, GM.dropModuleNames x)
    where
      x = GM.stripParensSym x'
  
  errResolve :: PJ.Doc -> String -> LocSymbol -> Error
  errResolve k msg lx = ErrResolve (GM.fSrcSpan lx) k (F.pprint (F.val lx)) (PJ.text msg)
  
  -------------------------------------------------------------------------------
  -- | @ofBareType@ and @ofBareTypeE@ should be the _only_ @SpecType@ constructors
  -------------------------------------------------------------------------------
  ofBareType :: HasCallStack => Env -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> SpecType
  ofBareType env l ps t = either fail' id (ofBareTypeE env l ps t)
    where
      fail'                  = Ex.throw
      -- fail                   = Misc.errorP "error-ofBareType" . F.showpp
  
  ofBareTypeE :: HasCallStack => Env -> F.SourcePos -> Maybe [PVar BSort] -> BareType -> Lookup SpecType
  ofBareTypeE env l ps t = ofBRType env (const (resolveReft l ps t)) l t
  
  resolveReft :: F.SourcePos -> Maybe [PVar BSort] -> BareType -> RReft -> RReft
  resolveReft l ps t
          = txParam l RT.subvUReft (RT.uPVar <$> πs) t
          . fixReftTyVars t       -- same as fixCoercions
    where
      πs  = Mb.fromMaybe tπs ps
      tπs = ty_preds (toRTypeRep t)
  
  fixReftTyVars :: BareType -> RReft -> RReft
  fixReftTyVars bt  = coSubRReft coSub
    where
      coSub         = M.fromList [ (F.symbol a, F.FObj (specTvSymbol a)) | a <- tvs ]
      tvs           = RT.allTyVars bt
      specTvSymbol  = F.symbol . RT.bareRTyVar
  
  coSubRReft :: F.CoSub -> RReft -> RReft
  coSubRReft su r = r { ur_reft = coSubReft su (ur_reft r) }
  
  coSubReft :: F.CoSub -> F.Reft -> F.Reft
  coSubReft su (F.Reft (x, e)) = F.Reft (x, F.applyCoSub su e)
  
  
  ofBSort :: HasCallStack => Env -> F.SourcePos -> BSort -> RSort
  ofBSort env l t = either (Misc.errorP "error-ofBSort" . F.showpp) id (ofBSortE env l t)
  
  ofBSortE :: HasCallStack => Env -> F.SourcePos -> BSort -> Lookup RSort
  ofBSortE env l t = ofBRType env (const id) l t
  
  ofBPVar :: Env -> F.SourcePos -> BPVar -> RPVar
  ofBPVar env l = fmap (ofBSort env l)
  
  --------------------------------------------------------------------------------
  txParam :: F.SourcePos -> ((UsedPVar -> UsedPVar) -> t) -> [UsedPVar] -> RType c tv r -> t
  txParam l f πs t = f (txPvar l (predMap πs t))
  
  txPvar :: F.SourcePos -> M.HashMap F.Symbol UsedPVar -> UsedPVar -> UsedPVar
  txPvar l m π = π { pargs = args' }
    where
      args' | not (null (pargs π)) = zipWith (\(_,x ,_) (t,_,y) -> (t, x, y)) (pargs π') (pargs π)
            | otherwise            = pargs π'
      π'    = Mb.fromMaybe err $ M.lookup (pname π) m
      err   = uError $ ErrUnbPred sp (pprint π)
      sp    = GM.sourcePosSrcSpan l
  
  predMap :: [UsedPVar] -> RType c tv r -> M.HashMap F.Symbol UsedPVar
  predMap πs t = M.fromList [(pname π, π) | π <- πs ++ rtypePredBinds t]
  
  rtypePredBinds :: RType c tv r -> [UsedPVar]
  rtypePredBinds = map RT.uPVar . ty_preds . toRTypeRep
  
  
  
  --------------------------------------------------------------------------------
  type Expandable r = ( PPrint r
                      , Reftable r
                      , SubsTy RTyVar (RType RTyCon RTyVar ()) r
                      , Reftable (RTProp RTyCon RTyVar r)
                      , HasCallStack)
  
  ofBRType :: (Expandable r) => Env -> ([F.Symbol] -> r -> r) -> F.SourcePos -> BRType r
           -> Lookup (RRType r)
  ofBRType env f l = go []
    where
      goReft bs r             = return (f bs r)
      goRFun bs x i t1 t2 r  = RFun x i{permitTC = Just (typeclass (getConfig env))} <$> (rebind x <$> go bs t1) <*> go (x:bs) t2 <*> goReft bs r
      rebind x t              = F.subst1 t (x, F.EVar $ rTypeValueVar t)
      go bs (RAppTy t1 t2 r)  = RAppTy <$> go bs t1 <*> go bs t2 <*> goReft bs r
      go bs (RApp tc ts rs r) = goRApp bs tc ts rs r
      go bs (RFun x i t1 t2 r) = goRFun bs x i t1 t2 r
      go bs (RVar a r)        = RVar (RT.bareRTyVar a) <$> goReft bs r
      go bs (RAllT a t r)     = RAllT a' <$> go bs t <*> goReft bs r
        where a'              = dropTyVarInfo (mapTyVarValue RT.bareRTyVar a)
      go bs (RAllP a t)       = RAllP a' <$> go bs t
        where a'              = ofBPVar env l a
      go bs (RAllE x t1 t2)   = RAllE x  <$> go bs t1    <*> go bs t2
      go bs (REx x t1 t2)     = REx   x  <$> go bs t1    <*> go (x:bs) t2
      go bs (RRTy xts r o t)  = RRTy  <$> xts' <*> goReft bs r <*> pure o <*> go bs t
        where xts'            = mapM (traverse (go bs)) xts
      go bs (RHole r)         = RHole    <$> goReft bs r
      go _ (RExprArg le)      = return    $ RExprArg le
      goRef bs (RProp ss (RHole r)) = rPropP <$> mapM goSyms ss <*> goReft bs r
      goRef bs (RProp ss t)         = RProp  <$> mapM goSyms ss <*> go bs t
      goSyms (x, t)                 = (x,) <$> ofBSortE env l t
      goRApp bs tc ts rs r          = bareTCApp <$> goReft bs r <*> lc' <*> mapM (goRef bs) rs <*> mapM (go bs) ts
        where
          lc'                    = F.atLoc lc <$> lookupGhcTyConLHName (reTyLookupEnv env) lc
          lc                     = btc_tc tc
  
  lookupGhcTyConLHName :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Lookup Ghc.TyCon
  lookupGhcTyConLHName env lc = do
      case lookupTyThing env lc of
        Ghc.ATyCon tc -> Right tc
        Ghc.AConLike (Ghc.RealDataCon dc) -> Right $ Ghc.promoteDataCon dc
        _ -> panic
              (Just $ GM.fSrcSpan lc) $ "not a type constructor: " ++ show (val lc)
  
  -- | Get the TyThing from an LHName.
  --
  -- This function uses 'unsafePerformIO' to lookup the 'Ghc.TyThing' of a 'Ghc.Name'.
  -- This should be benign because the result doesn't depend of when exactly this is
  -- called. Since this code is intended to be used inside a GHC plugin, there is no
  -- danger that GHC is finalized before the result is evaluated.
  lookupTyThingMaybe :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Maybe Ghc.TyThing
  lookupTyThingMaybe env lc@(Loc _ _ c0) = unsafePerformIO $ do
      case c0 of
        LHNUnresolved _ _ -> panic (Just $ GM.fSrcSpan lc) $ "unresolved name: " ++ show c0
        LHNResolved rn _ -> case rn of
          LHRLocal _ -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a local name: " ++ show c0
          LHRIndex i -> panic (Just $ GM.fSrcSpan lc) $ "cannot resolve a LHRIndex " ++ show i
          LHRLogic _ -> panic (Just $ GM.fSrcSpan lc) $ "lookupTyThing: cannot resolve a LHRLogic name " ++ show (lhNameToResolvedSymbol c0)
          LHRGHC n ->
            Ghc.reflectGhc (Interface.lookupTyThing (gtleTypeEnv env) n) (gtleSession env)
  
  lookupTyThing :: HasCallStack => GHCTyLookupEnv -> Located LHName -> Ghc.TyThing
  lookupTyThing env lc =
      Mb.fromMaybe (panic (Just $ GM.fSrcSpan lc) $ "not found: " ++ show (val lc)) $
        lookupTyThingMaybe env lc
  
  bareTCApp :: (Expandable r)
            => r
            -> Located Ghc.TyCon
            -> [RTProp RTyCon RTyVar r]
            -> [RType RTyCon RTyVar r]
            -> RType RTyCon RTyVar r
  bareTCApp r (Loc l _ c) rs ts | Just rhs <- Ghc.synTyConRhs_maybe c
    = if GM.kindTCArity c < length ts
        then Ex.throw err -- error (F.showpp err)
        else tyApp (RT.subsTyVarsMeet su $ RT.ofType rhs) (drop nts ts) rs r
      where
         tvs = [ v | (v, b) <- zip (GM.tyConTyVarsDef c) (Ghc.tyConBinders c), GM.isAnonBinder b]
         su  = zipWith (\a t -> (RT.rTyVar a, toRSort t, t)) tvs ts
         nts = length tvs
  
         err :: Error
         err = ErrAliasApp (GM.sourcePosSrcSpan l) (pprint c) (Ghc.getSrcSpan c)
                           (PJ.hcat [ PJ.text "Expects"
                                    , pprint (GM.realTcArity c)
                                    , PJ.text "arguments, but is given"
                                    , pprint (length ts) ] )
  -- TODO expandTypeSynonyms here to
  bareTCApp r (Loc _ _ c) rs ts | Ghc.isFamilyTyCon c && isTrivial t
    = expandRTypeSynonyms (t `RT.strengthen` r)
    where t = RT.rApp c ts rs mempty
  
  bareTCApp r (Loc _ _ c) rs ts
    = RT.rApp c ts rs r
  
  
  tyApp :: Reftable r => RType c tv r -> [RType c tv r] -> [RTProp c tv r] -> r
        -> RType c tv r
  tyApp (RApp c ts rs r) ts' rs' r' = RApp c (ts ++ ts') (rs ++ rs') (r `meet` r')
  tyApp t                []  []  r  = t `RT.strengthen` r
  tyApp _                 _  _   _  = panic Nothing "Bare.Type.tyApp on invalid inputs"
  
  expandRTypeSynonyms :: (Expandable r) => RRType r -> RRType r
  expandRTypeSynonyms = RT.ofType . Ghc.expandTypeSynonyms . RT.toType False
  
  {-
  expandRTypeSynonyms :: (Expandable r) => RRType r -> RRType r
  expandRTypeSynonyms t
    | rTypeHasHole t = t
    | otherwise      = expandRTypeSynonyms' t
  
  rTypeHasHole :: RType c tv r -> Bool
  rTypeHasHole = foldRType f False
    where
      f _ (RHole _) = True
      f b _         = b
  -}
  
  ------------------------------------------------------------------------------------------
  -- | Is this the SAME as addTyConInfo? No. `txRefSort`
  -- (1) adds the _real_ sorts to RProp,
  -- (2) gathers _extra_ RProp at turns them into refinements,
  --     e.g. tests/pos/multi-pred-app-00.hs
  ------------------------------------------------------------------------------------------
  
  txRefSort :: TyConMap -> F.TCEmb Ghc.TyCon -> LocSpecType -> LocSpecType
  txRefSort tyi tce t = F.atLoc t $ mapBot (addSymSort (GM.fSrcSpan t) tce tyi) (val t)
  
  addSymSort :: Ghc.SrcSpan -> F.TCEmb Ghc.TyCon -> TyConMap -> SpecType -> SpecType
  addSymSort sp tce tyi (RApp rc@RTyCon{} ts rs rr)
    = RApp rc ts (zipWith3 (addSymSortRef sp rc) pvs rargs [1..]) r2
    where
      (_, pvs)           = RT.appRTyCon tce tyi rc ts
      -- pvs             = rTyConPVs rc'
      (rargs, rrest)     = splitAt (length pvs) rs
      r2                 = L.foldl' go rr rrest
      go r (RProp _ (RHole r')) = r' `meet` r
      go r (RProp  _ t' )       = let r' = Mb.fromMaybe mempty (stripRTypeBase t') in r `meet` r'
  
  addSymSort _ _ _ t
    = t
  
  addSymSortRef :: (PPrint s) => Ghc.SrcSpan -> s -> RPVar -> SpecProp -> Int -> SpecProp
  addSymSortRef sp rc p r i = addSymSortRef' sp rc i p r
  
  addSymSortRef' :: (PPrint s) => Ghc.SrcSpan -> s -> Int -> RPVar -> SpecProp -> SpecProp
  addSymSortRef' _ _ _ p (RProp s (RVar v r)) | isDummy v
    = RProp xs t
      where
        t  = ofRSort (pvType p) `RT.strengthen` r
        xs = spliceArgs "addSymSortRef 1" s p
  
  addSymSortRef' sp rc i p (RProp _ (RHole r@(MkUReft _ (Pr [up]))))
    | length xs == length ts
    = RProp xts (RHole r)
    | otherwise
    = -- Misc.errorP "ZONK" $ F.showpp (rc, pname up, i, length xs, length ts)
      uError $ ErrPartPred sp (pprint rc) (pprint $ pname up) i (length xs) (length ts)
      where
        xts = Misc.safeZipWithError "addSymSortRef'" xs ts
        xs  = Misc.snd3 <$> pargs up
        ts  = Misc.fst3 <$> pargs p
  
  addSymSortRef' _ _ _ _ (RProp s (RHole r))
    = RProp s (RHole r)
  
  addSymSortRef' _ _ _ p (RProp s t)
    = RProp xs t
      where
        xs = spliceArgs "addSymSortRef 2" s p
  
  spliceArgs :: String  -> [(F.Symbol, b)] -> PVar t -> [(F.Symbol, t)]
  spliceArgs msg syms p = go (fst <$> syms) (pargs p)
    where
      go []     []           = []
      go []     ((s,x,_):as) = (x, s):go [] as
      go (x:xs) ((s,_,_):as) = (x,s):go xs as
      go xs     []           = panic Nothing $ "spliceArgs: " ++ msg ++ "on XS=" ++ show xs
  
  ---------------------------------------------------------------------------------
  -- RJ: formerly, `replaceLocalBinds` AFAICT
  -- | @resolveLocalBinds@ resolves that the "free" variables that appear in the
  --   type-sigs for non-toplevel binders (that correspond to other locally bound)
  --   source variables that are visible at that at non-top-level scope.
  --   e.g. tests-names-pos-local02.hs
  ---------------------------------------------------------------------------------
  resolveLocalBinds :: Env -> [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
                    -> [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
  ---------------------------------------------------------------------------------
  resolveLocalBinds env xtes = [ (x,t,es) | (x, (t, es)) <- topTs ++ replace locTs ]
    where
      (locTs, topTs)         = partitionLocalBinds [ (x, (t, es)) | (x, t, es) <- xtes]
      replace                = M.toList . replaceSigs . M.fromList
      replaceSigs sigm       = coreVisitor replaceVisitor M.empty sigm cbs
      cbs                    = _giCbs (reSrc env)
  
  replaceVisitor :: CoreVisitor SymMap SigMap
  replaceVisitor = CoreVisitor
    { envF  = addBind
    , bindF = updSigMap
    , exprF = \_ m _ -> m
    }
  
  addBind :: SymMap -> Ghc.Var -> SymMap
  addBind env v = case localKey v of
    Just vx -> M.insert vx (F.symbol v) env
    Nothing -> env
  
  updSigMap :: SymMap -> SigMap -> Ghc.Var -> SigMap
  updSigMap env m v = case M.lookup v m of
    Nothing  -> m
    Just tes -> M.insert v (myTracepp ("UPD-LOCAL-SIG " ++ GM.showPpr v) $ renameLocalSig env tes) m
  
  renameLocalSig :: SymMap -> (LocBareType, Maybe [Located F.Expr])
                 -> (LocBareType, Maybe [Located F.Expr])
  renameLocalSig env (t, es) = (F.substf tSub t, F.substf esSub es)
    where
      tSub                   = F.EVar . qualifySymMap env
      esSub                  = tSub `F.substfExcept` xs
      xs                     = ty_binds (toRTypeRep (F.val t))
  
  qualifySymMap :: SymMap -> F.Symbol -> F.Symbol
  qualifySymMap env x = M.lookupDefault x x env
  
  type SigMap = M.HashMap Ghc.Var  (LocBareType, Maybe [Located F.Expr])
  type SymMap = M.HashMap F.Symbol F.Symbol
  
  ---------------------------------------------------------------------------------
  partitionLocalBinds :: [(Ghc.Var, a)] -> ([(Ghc.Var, a)], [(Ghc.Var, a)])
  ---------------------------------------------------------------------------------
  partitionLocalBinds = L.partition (Mb.isJust . localKey . fst)
  