content: {-# LANGUAGE ConstraintKinds       #-}
  {-# LANGUAGE DeriveDataTypeable    #-}
  {-# LANGUAGE DoAndIfThenElse       #-}
  {-# LANGUAGE FlexibleContexts      #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE LambdaCase            #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE RankNTypes            #-}
  {-# LANGUAGE ScopedTypeVariables   #-}
  {-# LANGUAGE TupleSections         #-}
  {-# LANGUAGE UndecidableInstances  #-}
  {-# LANGUAGE ViewPatterns          #-}
  
  module Language.Rsc.Typecheck.Checker (verifyFile, typeCheck) where
  
  import           Control.Arrow                      (first, second, (***))
  import           Control.Monad
  import           Data.Default
  -- import qualified Data.Foldable                      as FO
  import           Data.Function                      (on)
  import           Data.Generics
  import qualified Data.IntMap.Strict                 as I
  import           Data.List                          (partition, sortBy)
  import           Data.Maybe                         (fromMaybe)
  import qualified Data.Traversable                   as T
  import           Language.Fixpoint.Misc             as FM
  import qualified Language.Fixpoint.Types            as F
  import           Language.Fixpoint.Types.Errors
  import           Language.Rsc.Annotations
  import           Language.Rsc.AST
  import           Language.Rsc.ClassHierarchy
  import           Language.Rsc.CmdLine               (Config, noFailCasts)
  import           Language.Rsc.Core.EitherIO
  import           Language.Rsc.Environment
  import           Language.Rsc.Errors
  import           Language.Rsc.Locations
  import           Language.Rsc.Lookup
  import           Language.Rsc.Misc                  (nths, single, zipWith3M)
  import           Language.Rsc.Names
  import           Language.Rsc.Parser
  import           Language.Rsc.Pretty
  import           Language.Rsc.Program
  import           Language.Rsc.SSA.SSA
  import           Language.Rsc.Symbols
  import           Language.Rsc.SystemUtils
  import           Language.Rsc.Typecheck.Environment
  import           Language.Rsc.Typecheck.Sub
  import           Language.Rsc.Typecheck.Subst
  import           Language.Rsc.Typecheck.TCMonad
  import           Language.Rsc.Typecheck.Types
  import           Language.Rsc.Typecheck.Unify
  import           Language.Rsc.Types
  import           Language.Rsc.TypeUtilities
  import           Language.Rsc.Visitor
  import           Text.PrettyPrint.HughesPJ          (($+$))
  
  -- import           Debug.Trace                        hiding (traceShow)
  
  import qualified System.Console.CmdArgs.Verbosity   as V
  
  --------------------------------------------------------------------------------
  -- | Top-level Verifier
  --------------------------------------------------------------------------------
  verifyFile :: Config -> [FilePath] -> IO (UAnnSol a, FError)
  --------------------------------------------------------------------------------
  verifyFile cfg fs
    = runEitherIO (do p   <- parseRscFromFiles fs
                      cha <- liftEither (mkCHA p)
                      ssa <- ssaTransform p cha
                      tc  <- typeCheck cfg ssa cha
                      return tc)
    >>= either unsafe (pure . safe cfg)
  
  
  unsafe errs = do putStrLn "\n\n\nErrors Found!\n\n"
                   return $ (NoAnn, errs)
  
  safe cfg (Rsc {code = Src fs}) = (NoAnn, failCasts (noFailCasts cfg) fs)
      where
          failCasts True  _ = F.Safe
          failCasts False f = applyNonNull F.Safe F.Unsafe
                            $ concatMap castErrors
                            $ casts f
  
          casts :: Data r => [Statement (AnnTc r)] -> [AnnTc r]
          casts = foldStmts castVis () []
            where
              castVis = defaultVisitor { accExpr = aE }
              aE _ (Cast_ a _) = [a]
              aE _ _ = [ ]
  
  --------------------------------------------------------------------------------
  castErrors :: Unif r => AnnTc r -> [Error]
  --------------------------------------------------------------------------------
  castErrors (FA _ l facts) = downErrors
    where
      downErrors = [ errorDownCast l t | TypeCast _ t <- facts]
  
  --------------------------------------------------------------------------------
  typeCheck
    :: Unif r => Config -> TcRsc r -> ClassHierarchy r -> EitherIO FError (TcRsc r)
  --------------------------------------------------------------------------------
  typeCheck cfg pgm cha = EitherIO $ do
      startPhase Loud "TC"
      v <- V.getVerbosity
      return $ execute cfg v pgm (tcRsc pgm cha)
  
  --------------------------------------------------------------------------------
  -- | TypeCheck program
  --------------------------------------------------------------------------------
  tcRsc :: Unif r => TcRsc r -> ClassHierarchy r -> TCM r (TcRsc r)
  --------------------------------------------------------------------------------
  tcRsc p@(Rsc {code = Src fs}) cha = do
      γ       <- initGlobalEnv p cha
      _       <- checkTypes cha
      (fs',_) <- tcStmts γ fs
      fs''    <- patch fs'
      ast_cnt <- getAstCount
      return   $ p { code = Src fs'', maxId = ast_cnt }
  
    -- where
  
      -- as ss' = vcat $ map (\s0 -> vcat (map (\a -> pp (fSrc a) $+$
      -- nest 6 (vcat (map pp (fFact a)))) (FO.toList s0))) ss'
  
  
  
  -- | Patch annotation on the AST
  --------------------------------------------------------------------------------
  patch :: Unif r => [Statement (AnnTc r)] -> TCM r [Statement (AnnTc r)]
  --------------------------------------------------------------------------------
  patch fs
    = do  (m, θ) <- (,) <$> getAnns <*> getSubst
          return $ map (\f -> apply θ $ fmap (pa m) f) fs
    where
      pa m (FA i l f) = FA i l $ f ++ filter vld (I.findWithDefault [] i m)
      vld TypInst{}     = True
      vld Overload{}    = True
      vld EltOverload{} = True
      vld PhiVar{}      = True
      vld PhiLoopTC{}   = True
      vld TypeCast{}    = True
      vld DeadCast{}    = True
      vld _             = False
  
  -- accumNodeIds :: Unif r => Statement (AnnTc r) -> [(Int, [Fact r])]
  -- accumNodeIds = FD.foldl (\b (FA i _ f) -> (i, f): b) []
  
  
  --------------------------------------------------------------------------------
  -- | TypeCheck Function
  --------------------------------------------------------------------------------
  
  --------------------------------------------------------------------------------
  tcFun :: Unif r => TCEnv r -> Statement (AnnTc r)
                   -> TCM r (Statement (AnnTc r), Maybe (TCEnv r))
  --------------------------------------------------------------------------------
  tcFun γ (FunctionStmt l f xs Nothing)
    = return $ (FunctionStmt l f xs Nothing, Just γ)
  tcFun γ (FunctionStmt l f xs (Just body))
    | Just ft   <- tcEnvFindTy f γ
    = do  ts    <- tcFunTys l f xs ft
          body' <- foldM (tcCallable γ l f xs) body ts
          return $ (FunctionStmt l f xs (Just body'), Just γ)
    | otherwise
    = die $ errorMissingSpec (srcPos l) f
  
  tcFun _  s = die $ bug (srcPos s) $ "Calling tcFun not on FunctionStatement"
  
  -- | `tcCallable g l f xs fty body` checks @body@ under the environment @g@
  -- (which needs to be set beforehand), with input arguments @xs@ and overload
  -- signature @fty@ (which includes the context number).
  --------------------------------------------------------------------------------
  tcCallable :: (Unif r, PP f, IsLocated f)
             => TCEnv r -> AnnTc r -> f
             -> [Id (AnnTc r)]
             -> [Statement (AnnTc r)]
             -> IOverloadSig r
             -> TCM r [Statement (AnnTc r)]
  --------------------------------------------------------------------------------
  tcCallable γ l f xs body fty = do
      γ'    <- initCallableEnv l γ f fty xs body
      body' <- addReturnStmt l γ' body
      tcFunBody γ' l body'
  
  addReturnStmt l γ body
    | isTVoid (tcEnvFindReturn γ)
    = (body ++) . single <$> (`ReturnStmt` Nothing) <$> freshenAnn l
    | otherwise
    = return body
  
  tcFunBody γ l body = do
      z <- tcStmts γ body
      case z of
        (_, Just _) | rt /= tVoid -> fatal er
        (b, _     ) | otherwise   -> return b
    where
      er = errorMissingReturn (srcPos l)
      rt = tcEnvFindReturn γ
  
  --------------------------------------------------------------------------------
  tcSeq :: (TCEnv r -> a -> TCM r (a, TCEnvO r)) -> TCEnv r -> [a] -> TCM r ([a], TCEnvO r)
  --------------------------------------------------------------------------------
  tcSeq f             = go []
    where
      go acc γ []     = return (reverse acc, Just γ)
      go acc γ (x:xs) = do (y, γo) <- f γ x
                           case γo of
                             Nothing -> return (reverse acc ++ y:xs, Nothing)
                             Just γ' -> go (y:acc) γ' xs
  
  --------------------------------------------------------------------------------
  tcStmts :: Unif r =>
    TCEnv r -> [Statement (AnnTc r)] -> TCM r ([Statement (AnnTc r)], TCEnvO r)
  --------------------------------------------------------------------------------
  tcStmts = tcSeq tcStmt
  
  --------------------------------------------------------------------------------
  tcStmt  :: Unif r =>
    TCEnv r -> Statement (AnnTc r) -> TCM r (Statement (AnnTc r), TCEnvO r)
  --------------------------------------------------------------------------------
  -- | skip
  tcStmt γ s@(EmptyStmt _)
    = return (s, Just γ)
  
  -- | interface Foo (this definition will be hoisted)
  tcStmt γ s@(InterfaceStmt _ _)
    = return (s, Just γ)
  
  -- | x = e
  tcStmt γ s@(ExprStmt l (AssignExpr l1 OpAssign (LVar lx x) e)) =
      tcWrap check >>= tcSW γ s
    where
      check = case tcEnvFindSymInfo x γ of
        -- Just (SI _ _ WriteGlobal t) -> do
        --     (e', _) <- tcExprT γ e t
        --     γ'      <- pure (tcEnvAdd (SI xSym Local WriteGlobal t) γ)
        --     return     (mkStmt e', Just γ')
  
        Just (SI _ _ WriteGlobal t) -> do
            (e', _) <- tcExprT γ e t
            return     (mkStmt e', Just γ)
  
        Just (SI _ _ a _) ->
            error $ "Could this happen- x = e ?? " ++ ppshow a
  
        Nothing -> do
            (e', t) <- tcExpr γ e Nothing
            γ'      <- pure (tcEnvAdd (SI xSym Local WriteLocal t) γ)
            return     (mkStmt e', Just γ')
  
      mkStmt  = ExprStmt l . AssignExpr l1 OpAssign (LVar lx x)
      xSym    = F.symbol x
  
  
  -- | e1.f = e2
  tcStmt γ s@(ExprStmt l (AssignExpr l2 OpAssign (LDot l1 e1 f) e2))
    = tcWrap check >>= tcSW γ s
    where
      check = do
        ue1       <- pure (enableUnique e1)
        (e1', t1) <- tcExpr γ ue1 Nothing
        m1o       <- pure (getMutability (envCHA γ) t1)
        m1fo      <- pure (getFieldMutability (envCHA γ) t1 f)
        case (m1o, m1fo) of
          (Just m1, Just m1f)
            | isSubtype γ m1f tMU || isSubtypeWithUq γ m1 tUQ ->
              case getProp l γ F.dummySymbol f t1 of
                Left e -> tcError e
                Right (unzip -> (ts, fs)) ->
                    do  e1''      <- castM γ e1' True t1 (tOr ts)
                        -- This is a consumable position --> UQ is allowed
                        (e2' , _) <- tcScan (tcExprT γ) e2 (map f_ty fs)
                        return (ExprStmt l (AssignExpr l2 OpAssign (LDot l1 e1'' f) e2'), Just γ)
  
            | otherwise -> tcError (errorImmutableRefAsgn l f e1 t1)
  
          (Nothing, _) -> tcError (errorExtractMut l t1 e1)
          (_, Nothing) -> tcError (errorExtractFldMut l f t1)
  
  -- | e
  tcStmt γ (ExprStmt l e)
    = do (e', to) <- tcExprW γ e
         return (ExprStmt l e', const γ <$> to)
  
  -- | s1;s2;...;sn
  tcStmt γ (BlockStmt l stmts)
    = do (stmts', g) <- tcStmts γ stmts
         return (BlockStmt l stmts', g)
  
  -- | if b { s1 }
  tcStmt γ (IfSingleStmt l b s)
    = tcStmt γ (IfStmt l b s (EmptyStmt l))
  
  -- | if b { s1 } else { s2 }
  tcStmt γ s@(IfStmt l e s1 s2)
    = do opTy         <- safeEnvFindTy l γ (builtinOpId BITruthy :: Identifier)
         ([e'], z)    <- tcNormalCallW γ l (builtinOpId BITruthy :: Identifier) [e] opTy
         case z of
           Just _  ->
              do  z1 <- tcStmt γ s1
                  z2 <- tcStmt γ s2
                  tcWrap (check e' z1 z2) >>= tcSW γ s
  
           Nothing -> return (IfStmt l e' s1 s2, Nothing)
    where
      check e' (s1', γ1) (s2', γ2) = do
          z <- envJoin l γ γ1 γ2
          return (IfStmt l e' s1' s2', z)
  
  -- | while c { b }
  tcStmt γ (WhileStmt l c b)
    = tcExprW γ c >>= \case
        (c', Nothing) -> return (WhileStmt l c' b, Nothing)
        (c', Just t)  -> do
            _         <- unifyTypeM (srcPos l) γ t tBool  -- meh ..
            (b', γ')  <- tcStmt γ b
            γ'        <- envLoopJoin l γ γ'
            return       (WhileStmt l c' b', Just γ')
  
  -- | var x1 [ = e1 ]; ... ; var xn [= en];
  tcStmt γ (VarDeclStmt l ds)
    = do (ds', z) <- tcSeq tcVarDecl γ ds
         return      (VarDeclStmt l ds', z)
  
  -- | return e
  tcStmt γ (ReturnStmt l (Just e)) =
      do  (e', _)   <- tcWrap check >>= tcEW γ e
          return       (ReturnStmt l (Just e'), Nothing)
    where
      rt    = tcEnvFindReturn γ
      check = do
          (e', t)   <- tcExpr γ (enableUnique e) (Just rt)
          θ         <- unifyTypeM (srcPos l) γ t rt
          (t', rt') <- pure (apply θ t, apply θ rt)
          e''       <- castM γ e' True t' rt'
          return       (e'', rt')
  
  tcStmt _ (ReturnStmt l Nothing)
    = return (ReturnStmt l Nothing, Nothing)
  
  -- | throw e
  tcStmt γ (ThrowStmt l e)
    = do  (e', _) <- tcExprW γ e
          return     (ThrowStmt l e', Nothing)
  
  -- | function (xs) { s }
  tcStmt γ s@FunctionStmt{}
    = tcFun γ s
  
  -- | class A<S...> [extends B<T...>] [implements I,J,...] { ... }
  tcStmt γ (ClassStmt l x ce)
    = do  d  <- resolveTypeM l γ rn
          msS <- mapM (tcStaticClassElt γS d) ceS
          msI <- mapM (tcInstanceClassElt γI d) ceI
          return $ (ClassStmt l x (msS ++ msI), Just γ)
    where
      γS         = γ
  
      γI         = γ
      rn         = QN (envPath γ) (F.symbol x)
      (ceS, ceI) = partition isStaticClassElt ce
  
  -- | module M { ... }
  tcStmt γ (ModuleStmt l n body) = do
      γ1 <- initModuleEnv γ n body
      (ModuleStmt l n *** return (Just γ)) <$>  tcStmts γ1 body
  
  -- | enum M { ... }
  tcStmt γ (EnumStmt l n body) =
      return (EnumStmt l n body, Just $ tcEnvAdd si γ)
    where
      si    = SI nSym exprt RdOnly tEnum
      tEnum = TRef (Gen name []) fTop
      path  = envPath γ
      name  = QN path nSym
      nSym  = F.symbol n
      exprt = Exported      -- TODO: do this check
  
  -- OTHER (Not handled)
  tcStmt _ s
    = convertError "tcStmt" s
  
  
  --------------------------------------------------------------------------------
  tcVarDecl :: Unif r => TCEnv r -> VarDecl (AnnTc r) -> TCM r (VarDecl (AnnTc r), TCEnvO r)
  --------------------------------------------------------------------------------
  tcVarDecl γ v@(VarDecl l x (Just e)) =
    case varDeclSymbol v of
      Left err -> fatal err
  
      Right Nothing -> do
        -- Local (no type annotation)
          (e', to) <- tcExprW γ e
          sio      <- pure (SI xSym Local WriteLocal <$> to)
          return      (VarDecl l x (Just e'), tcEnvAddo γ x sio)
  
        -- Local (with type annotation)
      Right (Just (SI _ lc WriteLocal t)) -> do
          (e', t') <- tcExprT γ e t
          return ( VarDecl l x $ Just e'
                 , Just $ tcEnvAdd (SI xSym lc WriteLocal t') γ)
  
        -- Global
      Right (Just s@(SI _ _ WriteGlobal t)) -> do
          -- PV: the global variable should be in scope already,
          --     since it is being hoisted to the beginning of the
          --     scope.
          (e', _)  <- tcExprT γ e t
          return      (VarDecl l x (Just e'), Just $ tcEnvAdd s γ)
  
        -- ReadOnly
      Right (Just (SI _ lc RdOnly t)) -> do
          ([e'], Just t') <- tcNormalCallWCtx γ l exprTId [(e, Just t)] (idTy t)
          return ( VarDecl l x $ Just e'
                 , Just $ tcEnvAdd (SI xSym lc RdOnly t') γ)
  
      c -> fatal (unimplemented l "tcVarDecl" ("case: " ++ ppshow c))
    where
      xSym    = F.symbol x
      exprTId = builtinOpId BIExprT :: Identifier
  
  tcVarDecl γ v@(VarDecl l x Nothing) =
    case varDeclSymbol v of
      Left err -> fatal err
  
      Right (Just (SI _ lc Ambient t)) ->
          return $ (v, Just $ tcEnvAdds [(x, SI xSym lc Ambient t)] γ)
  
      Right _ -> fatal (bug l "TC-tcVarDecl: this shouldn't happen")
    where
      xSym = F.symbol x
  
  --------------------------------------------------------------------------------
  tcStaticClassElt
    :: Unif r
    => TCEnv r -> TypeDecl r -> ClassElt (AnnTc r) -> TCM r (ClassElt (AnnTc r))
  --------------------------------------------------------------------------------
  
  -- | Static method: The classes type parameters should not be included in env
  --
  tcStaticClassElt γ (TD sig _ ms) (MemberMethDecl l True x xs body) =
    case F.lookupSEnv (F.symbol x) (s_mems ms) of
      Just FI{} ->
          tcError $ bugStaticField l x sig
      Just (MI _ _ mts) -> do
          let t = tAnd $ map snd mts
          its <- tcFunTys l x xs t
          body' <- foldM (tcCallable γ l x xs) body its
          return $ MemberMethDecl l True x xs body'
      Nothing ->
          fatal (errorClassEltAnnot (srcPos l) (sig) x)
  
  -- | Static field
  --
  tcStaticClassElt γ (TD sig _ ms) (MemberVarDecl l True x (Just e)) =
    case F.lookupSEnv (F.symbol x) (s_mems ms) of
      Just MI{} ->
          tcError $ bugStaticField l x sig
      Just (FI _ _ _ t) -> do
          ([e'],_) <- tcNormalCall γ l (builtinOpId BIFieldInit :: Identifier) [(e, Just t)] (mkInitFldTy t)
          return $ MemberVarDecl l True x $ Just e'
      Nothing ->
          fatal (errorClassEltAnnot (srcPos l) sig x)
  
  tcStaticClassElt _ _ (MemberVarDecl l True x Nothing)
    = fatal (unsupportedStaticNoInit (srcPos l) x)
  
  tcStaticClassElt _ _ c = error (show $ pp "tcStaticClassElt - not a static element: " $+$ pp c)
  
  
  
  --------------------------------------------------------------------------------
  tcInstanceClassElt
    :: Unif r
    => TCEnv r -> TypeDecl r -> ClassElt (AnnTc r) -> TCM r (ClassElt (AnnTc r))
  --------------------------------------------------------------------------------
  -- | Constructor
  
  tcInstanceClassElt γ typeDecl (Constructor l xs body) = do
      its    <- tcFunTys l ctor xs ctorTy
      body'  <- foldM (tcCallable γ' l ctor xs) body its
      return  $ Constructor l xs body'
    where
      TD sig@(TS _ (BGen nm bs) _) _ ms = typeDecl
      γ'     = tcEnvAdd viExit (initClassCtorEnv sig γ)
      ctor   = builtinOpId BICtor :: Identifier
  
      thisT   = TRef (Gen nm (map btVar bs)) fTop
      cExit   = builtinOpId BICtorExit :: Identifier
      viExit  = SI (F.symbol cExit) Local Ambient $ mkFun (bs, xts, ret)
      ret     = thisT
  
      xts      = case expandType def (envCHA γ) thisT of
                  Just (TObj _ ms _ ) ->
                      sortBy c_sym [ B x Req t | (x, FI _ _ _ t) <- F.toListSEnv (i_mems ms) ]
                  _ -> []
  
      c_sym = on compare (show . b_sym)     -- XXX: Symbolic compare is on Symbol ID
      ctorTy = fromMaybe (die $ unsupportedNonSingleConsTy (srcPos l)) (tm_ctor ms)
  
  
  -- | Instance variable
  --
  tcInstanceClassElt _ _ m@(MemberVarDecl _ False _ Nothing)
    = return m
  tcInstanceClassElt _ _ (MemberVarDecl l False x _)
    = die $ bugClassInstVarInit (srcPos l) x
  
  -- | Instance method
  --
  --   TODO: check method mutability
  --   TODO: The method's mutability should influence the type of tThis that is used
  --         as a binder to this.
  --   TODO: Also might not need 'tce_this'
  --
  tcInstanceClassElt γ (TD sig _ ms) (MemberMethDecl l False x xs bd)
    | Just (MI _ _ mts) <- F.lookupSEnv (F.symbol x) (i_mems ms)
    = do  let (ms', ts) = unzip mts
          its          <- tcFunTys l x xs $ tAnd ts
          let mts'      = zip ms' its
          bd'          <- foldM (\b (m,t) -> tcCallable (mkEnv m) l x xs b t) bd mts'
          return        $ MemberMethDecl l False x xs bd'
    | otherwise
    = fatal (errorClassEltAnnot (srcPos l) (sig) x)
    where
      mkEnv m     = initClassMethEnv m sig γ
  
  tcInstanceClassElt _ _ c = error (show $ pp "tcInstanceClassElt - not an instance element: " $+$ pp c)
  
  
  -- | `tcExprT l fn γ e t` checks expression `e`
  --
  --     * under environment `γ`,
  --
  --     * against a type `t`.
  --
  --   Expressions that are ONLY contextually typed, do not need to be checked
  --   against type `t`.
  --------------------------------------------------------------------------------
  tcExprT :: Unif r => TCEnv r -> ExprSSAR r -> RType r -> TCM r (ExprSSAR r, RType r)
  --------------------------------------------------------------------------------
  tcExprT γ e t
    | onlyCtxTyped e
    = tcExprWD γ e (Just t)
    | otherwise
    = do  ([e'], _) <- tcNormalCall γ l exprTId [(e, Just t)] (idTy t)
          return (e', t)
    where
      l       = getAnnotation e
      exprTId = builtinOpId BIExprT :: Identifier
  
  tcEnvAddo _ _ Nothing  = Nothing
  tcEnvAddo γ x (Just t) = Just (tcEnvAdds [(x, t)] γ)
  
  --------------------------------------------------------------------------------
  tcExprW  :: Unif r => TCEnv r -> ExprSSAR r -> TCM r (ExprSSAR r, Maybe (RType r))
  --------------------------------------------------------------------------------
  tcExprW γ e = tcWrap (tcExpr γ e Nothing) >>= tcEW γ e
  
  
  -- | `tcExprWD γ e t` checks expression @e@ under environment @γ@.
  --    (with an optional contextual type @t@ potentially wrapping it in a cast)
  --
  --------------------------------------------------------------------------------
  tcExprWD :: Unif r
    => TCEnv r -> ExprSSAR r -> Maybe (RType r) -> TCM r (ExprSSAR r, RType r)
  --------------------------------------------------------------------------------
  tcExprWD γ e t
    = do  eet <- tcWrap (tcExpr γ e t)
          et  <- tcEW γ e eet
          case et of
            (e', Just t) -> return (e', t)
            (e', _     ) -> return (e', tBot)
  
  
  -- | Wraps `tcNormalCall` with a cast-wrapping check of an error.
  --
  --------------------------------------------------------------------------------
  tcNormalCallW
    :: Unif r => TCEnv r -> AnnTc r -> Identifier
              -> [ExprSSAR r] -> RType r
              -> TCM r ([ExprSSAR r], Maybe (RType r))
  --------------------------------------------------------------------------------
  tcNormalCallW γ l o es t
    = tcWrap (tcNormalCall γ l o (es `zip` nths) t) >>= \case
        Right (es', t') -> return (es', Just t')
        Left e -> (,Nothing) <$> mapM (deadcastM "tcNormalCallW" γ [e]) es
  
  --------------------------------------------------------------------------------
  tcNormalCallWCtx
    :: Unif r => TCEnv r -> AnnTc r -> Identifier
              -> [(ExprSSAR r, Maybe (RType r))] -> RType r
              -> TCM r ([ExprSSAR r], Maybe (RType r))
  --------------------------------------------------------------------------------
  tcNormalCallWCtx γ l o es t
    = tcWrap (tcNormalCall γ l o es t) >>= \case
        Right (es', t') -> return (es', Just t')
        Left err -> (,Nothing) <$> mapM (deadcastM "tcNormalCallWCtx" γ [err]) (fst <$> es)
  
  -- | Like `tcNormalCallW`, but return _|_ in case of failure
  --
  --------------------------------------------------------------------------------
  tcNormalCallWD
    :: Unif r => TCEnv r -> AnnTc r -> Identifier -> [ExprSSAR r]
              -> RType r -> TCM r ([ExprSSAR r], RType r)
  --------------------------------------------------------------------------------
  tcNormalCallWD γ l o es t =
      tcNormalCallW γ l o es t >>= \case
        (es', Just t) -> return (es', t)
        (es', _     ) -> return (es', tBot)
  
  
  -- | Wrap expressions and statement in deadcasts
  --
  --   Both return empty environments in case of a failure. This causes the
  --   remainder of the basic block to not b checked at all. If this is not the
  --   prefered behavior, change by returning `Just γ`, where `γ` the input
  --   environment.
  --
  --------------------------------------------------------------------------------
  tcEW :: Unif r => TCEnv r -> ExprSSAR r -> Either Error (ExprSSAR r, b)
                 -> TCM r ((ExprSSAR r), Maybe b)
  --------------------------------------------------------------------------------
  tcEW _ _ (Right (e', t')) = return (e', Just t')
  tcEW γ e (Left er)        = (,Nothing) <$> deadcastM "tcEW" γ [er] e
  
  --------------------------------------------------------------------------------
  tcSW :: Unif r => TCEnv r -> Statement (AnnSSA r)
                 -> Either Error (Statement (AnnSSA r), Maybe b)
                 -> TCM r (Statement (AnnSSA r), Maybe b)
  --------------------------------------------------------------------------------
  tcSW _ _ (Right (s, b)) = return (s, b)
  tcSW γ s (Left  e)      = do
      l1    <- freshenAnn l
      l2    <- freshenAnn l
      dc    <- deadcastM "tcSW" γ [e] (NullLit l1)
      return   (ExprStmt l2 dc, Nothing)
    where l = getAnnotation s
  
  
  --------------------------------------------------------------------------------
  tcExpr :: Unif r
         => TCEnv r -> ExprSSAR r -> Maybe (RType r) -> TCM r (ExprSSAR r, RType r)
  --------------------------------------------------------------------------------
  tcExpr _ e@(IntLit _ _) _
    = return (e, tNum)
  
  tcExpr _ e@(NumLit _ _) _
    = return (e, tReal)
  
  tcExpr _ e@(HexLit _ _) _
    = return (e, tBV32)
  
  tcExpr _ e@(BoolLit _ _) _
    = return (e, tBool)
  
  tcExpr _ e@(StringLit _ _) _
    = return (e, tString)
  
  tcExpr _ e@(NullLit _) _
    = return (e, tNull)
  
  tcExpr γ e@(ThisRef l) _
    = case tcEnvFindTy thisSym γ of
        Just t  -> return (e, t)
        Nothing -> fatal (errorUnboundId (fSrc l) "this")
  
  tcExpr γ e@(VarRef l x) _
    -- | `undefined`
    | F.symbol x == F.symbol "undefined"
    = return (e, tUndef)
  
    -- | Ignore the `cast` variable
    | Just t <- to, isCastId x
    = return (e,t)
  
    -- | If `x` is a unique reference and it this does not appear to be
    --   place where unique references can appear, then flag an error.
    | Just t <- to
    , Just m <- getMutability (envCHA γ) t
    , isSubtypeWithUq γ m tUQ
    , not (isUniqueEnabled e)
    = tcError (errorUniqueRef l (Just e))
  
    -- | Regural bound variable
    | Just t <- to
    = return (e,t)
  
    | otherwise
    = tcError (errorUnboundId (fSrc l) x)
    where
      to = tcEnvFindTy x γ
  
  tcExpr γ (CondExpr l e e1 e2) (Just t)
    = do  opTy         <- safeEnvFindTy l γ (builtinOpId BITruthy :: Identifier)
          ([e'], z)    <- tcNormalCallW γ l (builtinOpId BITruthy :: Identifier) [e] opTy
          case z of
            Just _  -> do
                (e1', _) <- tcWrap (tcExprT γ e1 t) >>= tcEW γ e1
                (e2', _) <- tcWrap (tcExprT γ e2 t) >>= tcEW γ e2
                return      (CondExpr l e' e1' e2', t)
  
            Nothing -> error "TODO: error tcExpr condExpr"
  
  tcExpr _ e@(CondExpr l _ _ _) Nothing
    = tcError $ unimpCondExpCtxType l e
  
  tcExpr γ e@(PrefixExpr _ _ _) s
    = tcCall γ e s
  
  tcExpr γ e@(InfixExpr _ _ _ _) s
    = tcCall γ e s
  
  -- | f(e)
  tcExpr γ e@(CallExpr _ _ _) s
    = tcCall γ e s
  
  -- | [e1,..,en]
  tcExpr γ e@(ArrayLit l es) to
    = arrayLitTy l γ e to (length es) >>= \case
        Left ee    -> fatal ee
        Right opTy -> first (ArrayLit l) <$> tcNormalCallWD γ l (builtinOpId BIArrayLit) es opTy
  
  -- | { f1: e1, ..., fn: tn }
  tcExpr γ (ObjectLit l pes) to
    = do  (es', ts) <- unzip <$> T.mapM (uncurry (tcExprWD γ)) ets
          t         <- pure (TObj tUQ (tmsFromList (zipWith toFI ps ts)) fTop)
          return       $ (ObjectLit l (zip ps es'), t)
    where
      (ps , _)       = unzip pes
      toFI p t       = FI (F.symbol p) Req tUQ t
      ets            = map (\(p,e) -> (e, pTy p)) pes
      pTy p          | Just f@FI{} <- lkup p = Just (f_ty f)
                     | otherwise             = Nothing
      lkup p         = F.lookupSEnv (F.symbol p) ctxTys
      ctxTys         = maybe mempty (i_mems . typeMembersOfType (envCHA γ)) to
  
  -- | <T>e
  tcExpr γ ex@(Cast l e) _
    | [t] <- [ct | UserCast ct <- fFact l]
    = first (Cast l) <$> tcCast l γ e t
    | otherwise
    = die $  bugNoCasts (srcPos l) ex
  
  -- | Subtyping induced cast
  --
  --   If the existing cast has been added by another context (i.e. e' == Cast_  ...)
  --   then typecheck the contents of the cast and return the type of the internal
  --   expression.
  --
  --   If it's from the same context then the internal expression has been
  --   typechecked, so just return the inferred type.
  --
  tcExpr γ (Cast_ l e) to
    = case tCasts ++ dCasts of
        -- No casts in this context
        [ ] -> do (e', t) <- tcExpr γ e to
                  l'      <- freshenAnn l
                  return     (Cast_ l' e', t)
  
        -- [Right t] -> pure (Cast_ l e, ofType t)
  
        -- [Left _ ] -> pure (Cast_ l e, tBot)
  
        _         -> die $ bugNestedCasts (srcPos l) e
  
    where
      tCasts = [ Right t_ | TypeCast ξ t_ <- fFact l, tce_ctx γ == ξ ]
      dCasts = [ Left  es | DeadCast ξ es <- fFact l, tce_ctx γ == ξ ]
  
  -- | e.f
  tcExpr γ e@(DotRef _ _ _) s
    = tcCall γ e s
  
  -- | e1[e2]
  tcExpr γ e@(BracketRef _ _ _) s
    = tcCall γ e s
  
  -- | e1[e2] = e3
  tcExpr γ e@(AssignExpr _ OpAssign (LBracket _ _ _) _) s
    = tcCall γ e s
  
  -- | new C(e, ...)
  tcExpr γ e@(NewExpr _ _ _) s
    = tcCall γ e s
  
  -- | super
  tcExpr γ e@(SuperRef l) _
    = case tcEnvFindTy (builtinOpId BISuper :: Identifier) γ of
        Just t  -> return (e,t)
        Nothing -> fatal (errorSuper (fSrc l))
  
  -- | function (x,..) {  }
  tcExpr γ (FuncExpr l fo xs body) tCtxO
    | Just ft   <- funTy
    =  do ts    <- tcFunTys l f xs ft
          body' <- foldM (tcCallable γ l f xs) body ts
          return $ (FuncExpr l fo xs body', ft)
    | otherwise
    = fatal (errorNoFuncAnn $ srcPos l)
    where
      funTy | [ft] <- [ t | SigAnn _ _ t <- fFact l ] = Just ft
            | Just ft <- tCtxO = Just ft
            | otherwise        = Nothing
      f     = maybe (F.symbol "<anonymous>") F.symbol fo
  
  tcExpr _ e _
    = convertError "tcExpr" e
  
  -- | @tcCast@ emulating a simplified version of a function call
  --------------------------------------------------------------------------------
  tcCast :: Unif r => AnnTc r -> TCEnv r -> ExprSSAR r -> RType r -> TCM r (ExprSSAR r, RType r)
  --------------------------------------------------------------------------------
  tcCast l γ e tc
    = do  ([e'],t') <- tcNormalCall γ l (builtinOpId BICastExpr :: Identifier) [(e, Just tc)] (castTy tc)
          return       (e', t')
  
  --------------------------------------------------------------------------------
  tcCall :: Unif r => TCEnv r -> ExprSSAR r -> Maybe (RType r) -> TCM r (ExprSSAR r, RType r)
  --------------------------------------------------------------------------------
  
  -- | `o e`
  tcCall γ (PrefixExpr l o e) _
    = do opTy <- safeEnvFindTy l γ (prefixOpId o :: Identifier)
         z    <- tcNormalCallWD γ l (prefixOpId o) [e] opTy
         case z of
           ([e'], t) -> return (PrefixExpr l o e', t)
           _         -> fatal (impossible l "tcCall PrefixExpr")
  
  -- | `e1 o e2`
  tcCall γ (InfixExpr l o@OpInstanceof e1 e2) _
    = do (e2',t) <- tcExpr γ e2 Nothing
         case t of
           TClass (BGen (QN _ x) _)  ->
              do  opTy <- safeEnvFindTy l γ (infixOpId o :: Identifier)
                  ([e1',_], t') <- let args = [e1, StringLit l2 (F.symbolSafeString x)] in
                                   tcNormalCallWD γ l (infixOpId o) args opTy
                        -- TODO: add qualified name
                  return (InfixExpr l o e1' e2', t')
           _  -> fatal (unimplemented l "tcCall-instanceof" $ ppshow e2)
    where
      l2 = getAnnotation e2
  
  tcCall γ (InfixExpr l o e1 e2) _
    = do opTy <- safeEnvFindTy l γ  (infixOpId o :: Identifier)
         z    <- tcNormalCallWD γ l (infixOpId o :: Identifier) [e1, e2'] opTy
         case z of
           ([e1', e2'], t) -> return (InfixExpr l o e1' e2', t)
           _ -> fatal (impossible (srcPos l) "tcCall InfixExpr")
    where
      e2' | o `elem` [OpIn] = enableUnique e2
          | otherwise       = e2
  
  -- | `e1[e2]` Special case for Enumeration, and object literals with numeric
  -- or string arguments.
  --
  tcCall γ e@(BracketRef l e1 e2) _
    = runFailM (tcExpr γ e1 Nothing) >>= \case
        -- Enumeration
        Right (_, t) | isEnumType (envCHA γ) t -> fatal (unimplemented (srcPos l) msg e)
        -- Default
        _ -> safeEnvFindTy l γ (builtinOpId BIBracketRef :: Identifier) >>= call
    where
      msg     = "Support for dynamic access of enumerations"
      call ty = tcNormalCallWD γ l (builtinOpId BIBracketRef :: Identifier) [e1, e2] ty >>= \case
            ([e1', e2'], t) -> return (BracketRef l e1' e2', t)
            _ -> fatal (impossible (srcPos l) "tcCall BracketRef")
  
  -- | `e1[e2] = e3`
  tcCall γ (AssignExpr l OpAssign (LBracket l1 e1 e2) e3) _
    = do opTy <- safeEnvFindTy l γ (builtinOpId BIBracketAssign :: Identifier)
         z <- tcNormalCallWD γ l (builtinOpId BIBracketAssign :: Identifier) [enableUnique e1,e2,e3] opTy
         case z of
           ([e1', e2', e3'], t) -> return (AssignExpr l OpAssign (LBracket l1 e1' e2') e3', t)
           _ -> fatal (impossible (srcPos l) "tcCall AssignExpr")
  
  -- | `new e(e1,...,en)`
  tcCall γ (NewExpr l e es) s
    = do (e',t) <- tcExpr γ e Nothing
         case extractCtor γ t of
           Just ct -> do
              (es', tNew) <- tcNormalCallWD γ l (builtinOpId BICtor :: Identifier) es ct
              tNew'       <- pure (adjustCtxMut tNew s)
              return (NewExpr l e' es', tNew')
           Nothing ->
              fatal (errorConstrMissing (srcPos l) t)
  
  -- | e.f
  --
  tcCall γ (DotRef l e0 f) _ = do
      tOpt <- runFailM (tcExpr γ ue Nothing)
      case tOpt of
        Right et -> checkAccess et
        Left (TCErr Fatal e) -> fatal e
        Left (TCErr NonFatal e) -> tcError e
    where
      ue = enableUnique e0
  
      checkAccess (_, tRcvr) = do
          b <- unifyAndSubtypeM l γ tRcvr genArrTy
          -- Is this an array '.length' access?
          if b && F.symbol f == F.symbol "length" then
              checkArrayLength
          -- Otherwise, treat as normal access.
          else
              checkProp (getProp l γ F.dummySymbol f tRcvr)
  
      -- `a.length`
      checkArrayLength = do
          l1  <- freshenAnn l
          l2  <- freshenAnn l
          i   <- freshenId (builtinOpId BIGetLength)
          tcExpr γ (CallExpr l1 (VarRef l2 i) [ue]) Nothing
  
      -- Normal property access
      checkProp (Left er)   = tcError er
      checkProp (Right tfs) = do
          let (rTs, fs) = unzip tfs
          (e0', _)     <- tcExprT γ ue (tOr rTs)
          let t         = tyWithOpt fs
          return          (DotRef l e0' f, t)
  
      -- Add `or undef` in case of an optional field access
      tyWithOpt fs = case unzip [(t, o) | FI _ o _ t <- fs] of
          (ts, os) | Opt `elem` os -> orUndef (tOr ts)
                   | otherwise     -> tOr ts
  
      -- forall M T . Array<M,T>
      genArrTy =  mkAll bvs (TRef (Gen arrayName vs) fTop)
        where
          bvs  = [BTV m def (Just tRO), BTV t def Nothing]
          vs   = map tVar [TV  m def, TV t def]
          m    = F.symbol "M"
          t    = F.symbol "T"
  
  
  
  -- | `super(e1,...,en)`
  --
  --   XXX: there shouldn't be any `super(..)` calls after SSA ...
  --
  tcCall _ (CallExpr _ (SuperRef _)  _) _
    = error "BUG: super(..) calls should have been eliminated"
  
  -- | `e.m(es)`
  --
  tcCall γ (CallExpr l em@(DotRef l1 e0 f) es) _
    -- | isVariadicCall f = tcError (unimplemented l "Variadic" ex)
    | otherwise        = checkNonVariadic
    where
      ue  = enableUnique e0
      -- -- Variadic check
      -- isVariadicCall f_ = F.symbol f_ == F.symbol "call"
  
      -- Non-variadic
      checkNonVariadic =
        runFailM (tcExpr γ ue Nothing) >>= \case
          Right (_, te)           -> checkMemberAccess te
          Left (TCErr Fatal    e) -> fatal e
          Left (TCErr NonFatal e) -> tcError e
  
      -- Check all corresponding type members `tms`
      checkMemberAccess te =
        case getProp l γ F.dummySymbol f te of
          Right tms@(map fst -> ts) -> do
              (e', _   ) <- tcExprT γ ue (tOr ts)
              (es', ts') <- foldM stepTypeMemM (es, []) tms
              return        (CallExpr l (DotRef l1 e' f) es', tOr ts')
  
          Left e -> tcError e
  
      stepTypeMemM (es_, ts) (tR, m) = second (:ts) <$> checkTypeMember es_ tR m
  
      -- Check a single type member
      checkTypeMember es_ _  (FI _ Req _ ft) = tcNormalCallWD γ l biID es_ ft
      checkTypeMember _   _  (FI f _   _ _ ) = tcError $ errorOptFunUnsup l f ue
      checkTypeMember es_ tR (MI _ Req mts)  =
        case getMutability (envCHA γ) tR of
          Just mR ->
              case [ t | (m, t) <- mts, isSubtypeWithUq γ mR m ] of
                [] -> tcError $ errorMethMutIncomp l em mts mR
                ts -> tcNormalCallWD γ l biID es_ (tAnd ts)
  
          Nothing -> tcError $ errorNoMutAvailable l ue tR
  
      checkTypeMember _ _ (MI _ Opt _)  =
        error "TODO: Add error message at checkTypeMember MI Opt"
  
      biID = builtinOpId BIDotRefCallExpr
  
  -- | `e(es)`
  tcCall γ ex@(CallExpr l e es) _ = do
      (e', ft0) <- tcExpr γ e Nothing
      tcWrap (tcNormalCall γ l (builtinOpId BICallExpr) (es `zip` nths) ft0) >>= \case
        Right (es', t) -> return (CallExpr l e' es', t)
        Left e         -> (,tBot) <$> deadcastM "tcCall-CallExpr" γ [e] ex
  
         -- (es', t)  <- tcNormalCallWD γ l (builtinOpId BICallExpr) es ft0
         -- return       (CallExpr l e' es', t)
  
  tcCall _ e _
    = fatal (unimplemented (srcPos e) "tcCall" e)
  
  --------------------------------------------------------------------------------
  -- | @tcNormalCall@ resolves overloads and returns cast-wrapped versions of
  --   the arguments if subtyping fails.
  --
  --   May throw exceptions.
  --
  --------------------------------------------------------------------------------
  tcNormalCall :: Unif r
               => TCEnv r -> AnnTc r -> Identifier
               -> [(ExprSSAR r, Maybe (RType r))]
               -> RType r -> TCM r ([ExprSSAR r], RType r)
  --------------------------------------------------------------------------------
  tcNormalCall γ l fn etos ft0
    = do ets <- T.mapM (uncurry (tcExpr γ)) etos
         z   <- resolveOverload γ l fn ets ft0
         case z of
           Just (i, θ, ft) ->
               do addAnn l (Overload (tce_ctx γ) (F.symbol fn) i)
                  addSubst l θ
                  (es, ts) <- pure (unzip ets)
                  -- tcCallCase γ l fn es ts ft
  
  -- XXX: Why all this ??
                  tcWrap (tcCallCase γ l fn es ts ft) >>= \case
                    Right ets' -> return ets'
                    Left  er   -> do
                        es' <- T.mapM (deadcastM "tcNormalCall" γ [er] . fst) ets
                        return (es', tNull)
  
           Nothing -> tcError $ uncurry (errorCallNotSup (srcPos l) fn ft0) (unzip ets)
  
  
  --------------------------------------------------------------------------------
  -- | `resolveOverload γ l fn es ts ft`
  --
  --   When resolving an overload there are two prossible cases:
  --
  --   1. There is only a single signature available: then return just this
  --      signature regardless of subtyping constraints
  --
  --   2. There are more than one signature available: return all that pass the
  --      subtype check (this is what tcCallCaseTry does).
  --
  --------------------------------------------------------------------------------
  resolveOverload :: (Unif r, PP a)
                  => TCEnv r
                  -> AnnTc r
                  -> a
                  -> [(ExprSSAR r, RType r)]
                  -> RType r
                  -> TCM r (Maybe (IntCallSite, RSubst r, RType r))
  --------------------------------------------------------------------------------
  -- | A function signature is compatible if:
  --
  --   * The supplied parameters have the same number of 'normal' arguments, i.e.
  --     not including the 'self' argument.
  --
  --   * If the function requires a 'self' argument, the parameters provide one.
  --
  resolveOverload γ l fn es ft =
    case validOverloads of
      [(i,t)] -> Just . (i,,t) <$> getSubst
      _       -> tcCallCaseTry γ l fn (snd <$> es) validOverloads
    where
      validOverloads = [ (i, mkFun s) | (i, s@(_, bs, _)) <- overloads γ ft
                                      , length bs == length es ]
  
  --------------------------------------------------------------------------------
  -- | A successful pairing of formal to actual parameters will return `Just θ`,
  --   where @θ@ is the corresponding substitution. If the types are not acceptable
  --   this will return `Nothing`. In this case successful means:
  --
  --   1. Unifying without errors.
  --
  --   2. Passing the subtyping test.
  --
  --   The monad state is completely reversed after this function returns, thanks
  --   to `runMaybeM`. We don't need to reverse the action of `instantiateFTy`.
  --------------------------------------------------------------------------------
  tcCallCaseTry :: (Unif r, PP a)
    => TCEnv r -> AnnTc r -> a -> [RType r] -> [(IntCallSite, RType r)]
    -> TCM r (Maybe (IntCallSite, RSubst r, RType r))
  --------------------------------------------------------------------------------
  tcCallCaseTry _ _ _ _ []
    = return Nothing
  
  tcCallCaseTry γ l fn ts ((i,ft):fts)
    = runFailM go >>= \case Right (Just θ') -> return $ Just (i, θ', ft)
                            _               -> tcCallCaseTry γ l fn ts fts
    where
      go = do
        (βs, its1, _)  <- instantiateFTy l (tce_ctx γ) fn ft
        ts1            <- zipWithM (instantiateTy l $ tce_ctx γ) [1..] ts
        θ              <- unifyTypesM (srcPos l) γ ts1 its1
  
        let (ts2, its2) = apply θ (ts1, its1)
  
        --  1. Pick the type variables (V) that have a bound (B).
        --  2. Find the binding that the unification braught to them (T := V θ).
        let (appVs, cs) = unzip [(apply θ (btVar bv), c) | bv@(BTV _ _ (Just c)) <- βs]
  
        --  3. Use that to check against the bound B.
        --  4. Also check the argument types.
        if appVs <:: cs && ts2 <:: its2 then
            return $ Just θ
        else
            return Nothing
  
      (<::) ts1 ts2 = and (zipWith (isSubtypeWithUq γ) ts1 ts2)
  
  --------------------------------------------------------------------------------
  tcCallCase
    :: (PP a, Unif r)
    => TCEnv r -> AnnTc r -> a -> [ExprSSAR r]
    -> [RType r] -> RType r -> TCM r ([ExprSSAR r], RType r)
  --------------------------------------------------------------------------------
  tcCallCase γ@(tce_ctx -> ξ) l fn es ts ft
    = do  (βs, rhs, ot)   <- instantiateFTy l ξ fn ft
          lhs             <- zipWithM (instantiateTy l ξ) [1..] ts
          θ               <- unifyTypesM (srcPos l) γ lhs rhs
  
          let (vs, appVs, cs)  = unzip3 [ (s, apply θ (btVar bv), c) | bv@(BTV s l (Just c)) <- βs
                                                              , not (unassigned (TV s l) θ) ]
  
          unless (appVs <:: cs) (tcError (errorBoundsInvalid l vs appVs cs))
  
          let (lhs', rhs') = apply θ (lhs, rhs)
  
          es'             <- zipWith3M (castMC γ) es lhs' rhs'
          return           $ (es', apply θ ot)
  
    where
      (<::) ts1 ts2 = and (zipWith (isSubtypeWithUq γ) ts1 ts2)
  
  --------------------------------------------------------------------------------
  instantiateTy :: Unif r => AnnTc r -> IContext -> Int -> RType r -> TCM r (RType r)
  --------------------------------------------------------------------------------
  instantiateTy l ξ i (bkAll -> (bs, t))
    = do  (_, t)  <- freshTyArgs l i ξ bs t
          -- TODO: need to take the first arg into account, i.e. add the
          --       constraint to the environment
          return     $ t
  
  --------------------------------------------------------------------------------
  instantiateFTy :: (Unif r, PP a) => AnnTc r -> IContext -> a -> RType r
                                   -> TCM r ([BTVar r], [RType r], RType r)
  --------------------------------------------------------------------------------
  instantiateFTy l ξ fn ft@(bkAll -> (bs, t))
    = do  (fbs, ft')      <- freshTyArgs l 0 ξ bs t
          (_, ts, t')     <- maybe er return (bkFunNoBinds ft')
          return           $ (fbs, ts, t')
      where
        er      = tcError $ errorNonFunction (srcPos l) fn ft
  
  
  --------------------------------------------------------------------------------
  unifyAndSubtypeM
    :: Unif r => AnnTc r -> TCEnv r -> RType r -> RType r -> TCM r Bool
  --------------------------------------------------------------------------------
  unifyAndSubtypeM l γ t1 t2 = do
      eSubst <- unif
      case eSubst of
        Left _  -> return False
        Right (t1', t2') -> return $ isSubtype γ t1' t2'
    where
      (bs1, t1') = bkAll t1
      (bs2, t2') = bkAll t2
      unif       = runFailM $ do
          (_, t1'') <- freshTyArgs l 1 (envCtx γ) bs1 t1'
          (_, t2'') <- freshTyArgs l 2 (envCtx γ) bs2 t2'
          θ         <- unifyTypeM (srcPos l) γ t1'' t2''
          return       (apply θ t1'', apply θ t2'')
  
  
  
  
  -- | envJoin
  --
  --   XXX: May throw `tcError`: wrap appropriately
  --
  --------------------------------------------------------------------------------
  envJoin :: Unif r
    => AnnTc r -> TCEnv r -> TCEnvO r -> TCEnvO r -> TCM r (Maybe (TCEnv r))
  --------------------------------------------------------------------------------
  envJoin _ _ Nothing x           = return x
  envJoin _ _ x Nothing           = return x
  envJoin l γ (Just γ1) (Just γ2) = do
      s1s   <- mapM (safeEnvFindSI l γ1) xs    -- SI entry at the end of the 1st branch
      s2s   <- mapM (safeEnvFindSI l γ2) xs    -- SI entry at the end of the 2nd branch
      return $ Just $ foldl (\γ' (s1, s2) -> tcEnvAdd (siJoin γ1 s1 s2) γ') γ (zip s1s s2s)
    where
      xs        = [ x | PhiVar x <- fFact l ]
  
  siJoin γ s1 s2
      | isSubtype γ (v_type s1) (v_type s2) = s2
      | isSubtype γ (v_type s2) (v_type s1) = s1
      | otherwise = s1 { v_type = tOr [v_type s1, v_type s2] }
  
  --------------------------------------------------------------------------------
  envLoopJoin :: Unif r => AnnTc r -> TCEnv r -> TCEnvO r -> TCM r (TCEnv r)
  --------------------------------------------------------------------------------
  envLoopJoin _ γ Nothing   = return γ
  
  --  XXX: use the "next" name for the Φ-var in the propagated env γ_
  --
  envLoopJoin l γ (Just γ') = foldM (\γ_ (x, x') -> do
        s    <- safeEnvFindSI l γ  x
        s'   <- safeEnvFindSI l γ' x'
  
        -- [ T2 <: T1 ==> T1 ]
        --
        -- Lift uniqueness restriction since we are not allowing the loop SSA var
        -- to escape (any more than the original variable).
        --
        if isSubtypeWithUq γ_ (v_type s') (v_type s) then do
            addAnn l (PhiLoopTC (x, x', toType (v_type s)))
            return   (tcEnvAdd (s { v_name = v_name s' }) γ_)
  
        -- This would require a fixpoint computation, so it's not allowed
        else
            tcError (errorLoopWiden l x x' (v_type s) (v_type s'))
      ) γ (zip xs xs')
  
    where
      (xs, xs') = unzip [ x | PhiLoop x <- fFact l ]
  
  
  --------------------------------------------------------------------------------
  tcScan :: (a -> b -> TCM r (a, b)) -> a -> [b] -> TCM r (a, [b])
  --------------------------------------------------------------------------------
  tcScan f e ts = second reverse <$> foldM step (e, []) ts
    where
      step (a, bs) b = second (:bs) <$> f a b
  
  
  -- Local Variables:
  -- flycheck-disabled-checkers: (haskell-liquid)
  -- End:
  