{-# LANGUAGE PatternGuards #-}
module TCheck(tiExpr, tiExpl) where

import Data.List
import Control.Monad(when, unless)
import qualified Data.Map as M
import qualified Data.Set as S
import qualified GraphWrapper as GW
import Data.Ix(range)

import ListMap(lookupWithDefaultBy)
import SCC(scc)
import Util(findDup, concatMapM,
            headOrErr, initOrErr, lastOrErr, fromJustOrErr)
import Util(fst3)
import IntLit
import IntegerUtil(mask)
import Classic(isBSV)
import Flags(Flags)
import PFPrint
import Id
import FStringCompat
import PreStrings(fsEmpty)
import PreIds
import Position(Position(..), noPosition)
import Error(internalError, ErrMsg(..))
import ContextErrors
import Type
import Subst
import Pred hiding (name)
import qualified Pred(name)
import Scheme
import Assump
import TIMonad
import TCPat
import TCMisc
import CtxRed
import CSyntax
import CSyntaxUtil
import CFreeVars(getFVDl, getFVE, fvSetToFreeVars)
import CType(noTyVarNo, getTyVarId, getArrows, isTConArrow, leftTyCon,
             isTypeBit, isTypeString, isTypeUnit, isTypePrimAction, isTVar, isUpdateable,
             isTypeActionValue, isTypeActionValue_, getActionValueArg,
             splitTAp, tyConArgs, cTVarKind)
import VModInfo(VSchedInfo, VFieldInfo(..), VArgInfo(..), VPort)
import SchedInfo(SchedInfo(..), MethodConflictInfo(..))
import SymTab
import Pragma(PProp(..))
import CSubst
import ForeignFunctions(toAVId)
import CFreeVars(getFQTyVarsT)
-------

import Util(traces)
import Debug.Trace(traceM)
import IOUtil(progArgs)

doRTrace :: Bool
doRTrace = elem "-trace-type" progArgs
doRTrace2 :: Bool
doRTrace2 = length (filter (== "-trace-type") progArgs) > 1
doETrace :: Bool
doETrace = elem "-trace-type-expl" progArgs
rtrace :: String -> a -> a
rtrace s x = if doRTrace then traces s x else x
etrace :: String -> a -> a
etrace s x = if doETrace then traces s x else x

doTraceSatisfy :: Bool
doTraceSatisfy= elem "-trace-tc-satisfy" progArgs
-- satTrace s x = if doTraceSatisfy then traces s x else x
satTraceM :: String -> TI ()
satTraceM s = when (doTraceSatisfy) $ traceM s

warnMethArgMismatch :: Bool
warnMethArgMismatch = elem "-warn-meth-arg-mismatch" progArgs

-------

-- used to force-bit Integer types
bit32 :: Type
bit32 = TAp tBit t32

{- Unused:
int32 :: Type
int32 = TAp tInt t32
-}


data ImplReadTag = NoRead | ImplRead (Maybe Id)

-- tiExpr: type-infer an expression
--   first argument (as):    type environment (a.k.a., assumptions)
--   second argument (td):   expected type of exp
--   third argument (exp):   expression to typecheck
-- returns: TI (preds, exp') where
--   preds: context requirements
--   exp':  exp, possibly rewritten
tiExpr :: CheckT CExpr

tiExpr as td exp@(CLam ei e) = do
      --posCheck "A" i
      v <- newTVar "tiExpr CLam" KStar ei
      (rt, eq_ps) <- unifyFnTo ei exp td v
      s <- getSubst
      let v'  = apSub s v
      let rt' = apSub s rt
      -- trimSubst?
      (ps, e') <- case ei of
                    Right i -> tiExpr ((i :>: toScheme v') : as) rt' e
                    Left _  -> tiExpr as rt e -- don't bind
      def_id <- newVar (getPosition ei) "tiExprCLam"
      let ipat = either CPAny CPVar ei
          def_ty = (CQType [] (v' `fn` rt'))
          def = CDefT def_id [] def_ty [CClause [ipat] [] e']
      -- trace ("CLam " ++ ppReadable (ei, def_id)) $ return ()
      return (eq_ps ++ ps, Cletrec [CLValueSign def []] (CVar def_id))

{- XXX not quite right
tiExpr as td exp@(CLamT i qt e) = do
    sc <- mkSchemeNoBVs qt
    (qs :=> ty, ts) <- freshInst i sc
    qs'             <- mapM (mkVPred (getPosition exp)) qs

    trace (ppReadable(qs, ty, ts)) $ return ()

    v <- unifyFnTo i exp td ty
    (ps, e') <- tiExpr ((i :>: toScheme ty) : as) v e
    il <- newVar (getPosition i) "tiExprCLamT"
    return (qs' ++ ps, Cletrec [CLValueSign (CDefT il [] (CQType [] td) [CClause [CPVar i] [] e']) []] (CVar il))
-}

tiExpr as td exp@(CLamT ei (CQType [] ty) e) = do
    (v, eq_ps) <- unifyFnTo ei exp td ty
    (ps, e') <- case ei of
                  Right i -> tiExpr ((i :>: toScheme ty) : as) v e
                  Left _  -> tiExpr as v e -- don't bind
    --posCheck "B" i
    def_id <- newVar (getPosition ei) "tiExprCLamT"
    let ipat = either CPAny CPVar ei
        def = CDefT def_id [] (CQType [] td) [CClause [ipat] [] e']
    -- trace ("CLamT " ++ ppReadable (ei, def_id)) $ return ()
    return (eq_ps ++ ps, Cletrec [CLValueSign def []] (CVar def_id))

tiExpr as td exp@(CLamT ei (CQType _ ty) e) = do
    x <- (err (getPosition ei, (internalError "TCheck.tiExpr: CLamT with context")))
    return x

-- Monomorphic let binding used by deriving code
-- XXX Is this necessary?  Instead of "ei" should this just match "Right i"?
tiExpr type_env expected_type (CApply (CLam ei b) [e]) = do
    --trace ("mono let") $ return ()
    type_var <- newTVar "tiExpr CLam" KStar ei
    (ps, e') <- tiExpr type_env type_var e
    (qs, b') <- case ei of
                  Right i -> tiExpr ((i :>: toScheme type_var) : type_env) expected_type b
                  Left _ -> tiExpr type_env expected_type b -- don't bind
    let res_e = case ei of
                  Right i -> let def = CDefT i [] (CQType [] type_var) [CClause [] [] e']
                             in  Cletrec [CLValueSign def []] b'
                  Left _ -> b'
    return (ps ++ qs, res_e)

tiExpr type_env expected_type expr@(Cletseq defs body) = do
    -- desugar pattern matching in let defs
    defs_without_patterns <- mapM expCLMatch defs >>= return . concat
    (provisos_from_defs, type_env_from_defs, rewritten_defs)
        <- tiSeq tiLetseqDef type_env defs_without_patterns
    (provisos_from_body, rewritten_body)
        <- tiExpr (type_env_from_defs ++ type_env) expected_type body
    return (provisos_from_defs ++ provisos_from_body,
            Cletseq rewritten_defs rewritten_body)

tiExpr as td expr@(Cletrec ds e) = do
    (ps, as', ds') <- tiDefls as ds
    (qs, e')       <- tiExpr (as' ++ as) td e
    return (ps ++ qs, Cletrec ds' e')

tiExpr as td (CSelect e i) = tiSelect (ImplRead Nothing) as td e i id
tiExpr as td (CSelectTT ti e i) = tiSelect NoRead as td e i (const t)
  where t = TCon (TyCon ti (Just KStar) TIabstract)

tiExpr as td exp@(CCon c es) = do
    (c' :>: sc, ti) <- findCons td c
    (ps :=> t, ts) <- freshInstT "C" c sc td
    s <- getSubst
    let finalTD = apSub s td
        numTDExpected = genericLength $ fst $ getArrows $ finalTD
        numConExpected =
          case fst $ getArrows t of
            [argTy] | isTypeUnit argTy -> 0
                    | Just (TyCon _ _ (TIstruct (SDataCon _ False) fs)) <- leftTyCon argTy -> genericLength fs
            _ -> 1
        numGiven = genericLength es
        numRemaining = numConExpected - numGiven
    -- traceM ("CCon: " ++ ppReadable c ++ " " ++ show t ++ " " ++ show numExpected ++ " " ++ show numGiven)
    if numGiven > numConExpected
      -- XXX Errors about consturctor argument mismatches should contain the type of
      -- the constructor, but this is overly hard to actually compute.
      then err (getPosition exp, EConMismatchNumArgs (show c') numConExpected numGiven)
      else if not (isTVar finalTD) && numGiven < numConExpected && numRemaining /= numTDExpected
      then err (getPosition exp, EPartialConMismatchNumArgs (show c') (pfpReadable finalTD) numConExpected numGiven numTDExpected)
      else do extraArgs <- sequence $
                   map ((newVar $ getPosition c) . ("a" ++) . show) $
                   range (0, numRemaining - 1)
              let res =
                    case es ++ map CVar extraArgs of
                      []  -> let unit = setIdPosition (getPosition c) idPrimUnit
                             in CApply (CCon0 Nothing c) [CStruct (Just True) unit []]
                      [e] -> CApply (CCon0 Nothing c) [e]
                      es  ->
                        let ies = zipWith (\ i e -> (setIdPosition (getPosition e) i, e)) tupleIds es
                        in  CApply (CCon0 Nothing c) [CStruct (Just True) (mkTCId ti c) ies]
              tiExpr as td $ foldr CLam res $ map Right extraArgs

tiExpr as td (CCon1 ti c e) = tiExpr as td (CApply (CCon0 (Just ti) c) [e])

tiExpr as td exp@(CCon0 mti c) = do
    --trace ("CCon0: " ++ ppReadable c) $ return ()
    -- XXX not so nice, but must get result type to findCons
    tdc <- case mti of
           Nothing -> do
                        (_, tdc) <- unifyFnFromTo c exp td
                        return tdc
           Just ti -> return (TCon (TyCon ti Nothing TIabstract))
    --
    (c' :>: sc, ti) <- findCons tdc c
    (ps :=> t, ts) <- freshInstT "C" c sc td
    eq_ps <- unify exp t td
    ps'            <- concatMapM (mkVPred (getPosition exp)) ps
    return (eq_ps ++ ps', iAPs (CConT ti c' []) ts ps')

tiExpr as td exp@(CStruct mb c ies) = do
    --trace ("CStruct " ++ ppReadable exp) $ return ()
    disamb <- disambiguateStruct mb td c (map fst ies)
    case disamb of
      Left tc -> handleStruct tc
      Right ti  -> handleCons ti
 where
   handleCons ti = tiExpr as td (CApply (CCon0 Nothing c) [CStruct (Just True) ti ies])
   handleStruct tyc@(TyCon c' (Just k) (TIstruct ss qfs)) = do
            -- find any defaults
            defaults <- concatMapM (findFieldDefault td c c') qfs
            let mkTS t KStar = return t
                mkTS t (Kfun ka k) = do v <- newTVar "tiExpr CStruct" ka c; mkTS (TAp t v) k
                mkTS _ _ = internalError "TCheck.tiExpr mkTS"
                -- Given a field name from the type, find its definition
                -- in the CStruct (if a def isn't found, return don't-care).
                -- (Compare unqualified because "f" is unqualified and "i"
                -- might be qualified -- GenWrap creates qualified names.)
                mkIE f =
                  let -- lookup from a map, in case the number of fields is large
                      -- (this preserves the qualified name, since that's what the
                      -- previous code did; is it necessary?)
                      ies_map = M.fromList [ (unQualId i, (i,e)) | (i,e) <- ies ]
                      dflts_map = M.fromList defaults  -- defaults are unqualified
                      pos = getPosition c
                      und = anyExprAt pos
                  in
                    case (M.lookup f ies_map) of
                      Just (i,e) -> (i,e)
                      Nothing ->
                        case (M.lookup f dflts_map) of
                          Just e -> (f,e)
                          Nothing -> (setIdPosition pos f, und)
            -- We will want to perform "is \\ qfs" to find fields
            -- mentioned by the user which are not in the type.
            -- Since "is" can be qualified (by GenWrap, at least),
            -- we need to define what equality means and use "deleteFirstsBy"
            -- instead of "\\".
            let eq_func type_id user_id =
                    let (uqual, ubase) = getIdFStrings user_id
                        (tqual, tbase) = getIdFStrings type_id
                    in  (ubase == tbase) &&
                        (uqual == fsEmpty || uqual == tqual)
                del_func = deleteFirstsBy eq_func
            let is = map fst ies
                dfs = map unQualId is
                fs = map unQualId qfs
            case findDup dfs of
             i : _ -> err (getPosition i, EDupField (pfpString i))
             [] -> case (is `del_func` qfs) of
                   i : _ -> -- report the qualified type name (c')
                            err (getPosition i, ENotField (pfpString c') (pfpString i))
                   [] -> do
                    -- identify the missing fields
                    -- (except those with default values)
                    let missing_fs = fs \\ (dfs ++ map fst defaults)
                    -- warn about any missing defs which are not defaulted
                    let mkWarn i = twarn (getPosition c,
                                          WMissingField (pfpString i))
                    mapM_ mkWarn (filter (not . isRdyId) missing_fs)
                    st <- mkTS (TCon tyc) k
                    eq_ps <- unify exp st td
                    -- we already know that "i" is a member of "fs",
                    -- so call tiField1 directly
                    --psies <- mapM (tiField c fs as st) (map mkIE fs)
                    psies <- mapM (tiField1 as st) (map mkIE fs)
                    let (pss, ies') = unzip psies
                    --trace (show (fs, map fst ies)) $ return ()
                    return (concat (eq_ps:pss), CStructT st ies')
   handleStruct _ = internalError ("tiExpr: struct disambig didn't return expected TyCon")

tiExpr as td exp@(CStructUpd e []) = tiExpr as td e
tiExpr as td exp@(CStructUpd e ies@((i,_):_)) = do
    (ps, e') <- tiExpr as td e
    -- XXX should use all fields to disambiguate
    (_, ti, _) <- findFields td i
    sy <- getSymTab
    case findType sy ti of
     Just (TypeInfo _ _ _ (TIstruct sst qfs)) | isUpdateable sst -> do
        --posCheck "C" e
        x <- newVar (getPosition e) "tiExprCStructUpd"
        let v = CVar x
            fs = map unQualId qfs
            new = CStruct (Just True) ti (map mk fs)
            mk i = case lookup i ies of
                   Just e -> (i, e)
                   Nothing -> (i, CSelectTT ti v i)
            updids = map (unQualId . fst) ies
        case findDup updids of
            i : _ -> err (getPosition i, EDupField (pfpString i))
            [] -> case updids \\ fs of
                   i : _ -> err (getPosition i, ENotField (pfpString ti) (pfpString i))
                   [] -> do
                            (qs, new') <- tiExpr ((x :>: toScheme td) : as) td new
                            return (ps ++ qs, cLet [(x, td, e')] new')
     _ -> -- findFields would fail if the type was not a struct
          -- so this should only be reachable if the subtype is not SStruct
          err (getPosition e, ENotStructUpd (pfpString e))

-- case statement must have at least one arm
tiExpr as td exp@(Ccase pos _ []) = err (pos, EEmptyCase)
tiExpr as td exp@(Ccase pos e arms) =
  do
    -- traceM("original case: " ++ ppReadable exp)
    e_type <- newTVar "tiExpr.CCase scrutinee" KStar e
    (ps, e') <- tiExpr as e_type e
    let clause_type = e_type `fn` td
    let clauses = [CClause [cca_pattern arm] (cca_filters arm)
                   (cca_consequent arm) | arm <- arms]
    (ps', clauses') <- tiClauses as clause_type clauses
    s <- getSubst
    -- traceM("substitution: " ++ ppReadable s)
    -- bvs <- getBoundTVs
    -- traceM("bound tyvars" ++ ppReadable bvs)
    -- convert constraints to concrete predicates & remove duplicates
    let cpreds = nub (map (predToCPred . toPred) (apSub s (ps ++ ps')))
    let cqt_clause_type = (CQType cpreds (apSub s clause_type))
    -- addBoundTVs (tv cqt_clause_type)
    let ic = id_case pos
    -- desugar into *type-checked* CLValueSign of a function applied to the scrutinee
    -- NOTE: none of the variables in the cqt are to be generalized over (hence the [] in CDefT)
    let ccase = (Cletrec [CLValueSign (CDefT ic [] cqt_clause_type clauses') []]
                      (cApply 3 (CVar ic) [e']))
    -- traceM("desugared case: " ++ ppReadable ccase)
    -- (ps ++ ps', exp') <- tiExpr as td ccase
    -- popBoundTVs
    let ret_ps = ps ++ ps'
    ret_ps' <- updateContexts pos ret_ps  -- because tiApply does this
    return (ret_ps', ccase)

tiExpr as td (CAny pos uk) = do
    return ([], CAnyT pos uk td)

tiExpr as td exp@(CVar i) =
    -- it is ok to add register read to the variable
    tiVar (ImplRead Nothing) as td exp

tiExpr as td (CApply (CVar f) [exp]) | f `qualEq` idAsIfc =
    case (exp) of
        var@(CVar i) -> tiVar NoRead as td var
        sub@(CSub pos e1 e2) -> tiSub NoRead as td pos e1 e2
        sel@(CSelect e i) -> tiSelect NoRead as td e i id
        _ -> tiExpr as td exp

tiExpr as td exp@(CApply f@(CVar gn) es@[(CVar i)]) | gn `qualEq` idPrimGetName = do
  unifyNoEq "primGetName" exp tName td
  -- need to make sure to qualify the primitive identifier for IConv
  return ([], (CApply (CVar idPrimGetName) es))

tiExpr as td exp@(CApply f@(CVar vo) [e@(CHasType _ t)]) | vo == idValueOf = do
    let vs = nub (tv t)
    bvs <- getBoundTVs
    case vs \\ bvs of
        [] -> tiApply as td exp f e
        v : _ -> err (getPosition exp, EValueOf (pfpString v))

tiExpr as td exp@(CApply f@(CVar vo) [e@(CHasType _ t)]) | vo == idStringOf = do
    let vs = nub (tv t)
    bvs <- getBoundTVs
    case vs \\ bvs of
        [] -> tiApply as td exp f e
        v : _ -> err (getPosition exp, EStringOf (pfpString v))

tiExpr as td (CApply e []) = tiExpr as td e
tiExpr as td exp@(CApply f [e]) = tiApply as td exp f e
tiExpr as td (CApply e es) = tiExpr as td (foldl ap e es)
  where ap f a = CApply f [a]

-- lookup system-task handler in taskCheckMap and run
tiExpr as td exp@(CTaskApply f@(CVar task) es) =
  let undeftask as td f es = err (getPosition task, EUndefinedTask (pfpString task))
      checker = lookupWithDefaultBy qualEq taskCheckMap undeftask task
  in checker as td f es

-- already type-checked - just ensure expected type is PrimAction
-- and qualify the task identifier
-- unify is not needed since these are wrapped with a fromAction or fromPrimAction
tiExpr as td exp@(CTaskApplyT (CVar task) t es) =
  do
    -- pick out the matching qualified task identifier
    let task' = headOrErr ("TCheck.tiExpr: unmatched task: " ++
                           pfpString task)
                (filter (qualEq task) taskIds)
    let task'' = setIdPosition (getPosition task) task'
    --unify exp tPrimAction td
    --unify exp tAction td
    return([],(CTaskApplyT (CVar task'') t es))

-- apply "fromString" to string literals when the syntax is BSV
-- (Classic has a syntax for distinguishing Char from String)
-- XXX we could do this in the BSV parse, except that CPLit doesn't have
-- XXX a place to put the expression; so we put it here (after CPLit has
-- XXX been converted to CLit in a pattern clause)
tiExpr as td (CLit l@(CLiteral pos (LString _))) =
  let lt = CLitT tString l
  in  if (isBSV())
      then tiExpr as td (cVApply (idFromString pos) [lt])
      else tiExpr as td lt
tiExpr as td (CLit l@(CLiteral pos (LChar _))) = tiExpr as td (CLitT tChar l)

-- insert fromInteger for unsized integer literals
tiExpr as td exp@(CLit l@(CLiteral pos
                          (LInt iv@(IntLit { ilWidth = Nothing })))) = do
    --traceM("tiExpr: CLiteral: fromInteger")
    tiExpr as td (cVApply (idFromInteger pos) [CLitT tInteger l])

-- insert fromSizedInteger for sized integer literals
tiExpr as td exp@(CLit l@(CLiteral pos
                          (LInt iv@(IntLit { ilWidth = Just nBits,
                                             ilValue = val })))) = do
    --traceM("tiExpr: CLiteral: fromSizedInteger")
    let ty = tBitN nBits pos
        qty = CQType [] ty
    -- detect if the value is out of range
    let sizeErr = let lit = pfpString (iv { ilWidth = Nothing })
                  in  err (pos, EInvalidSizedLiteral lit nBits)
    if (nBits < 0)
       then internalError("TCheck.tiExpr: negative sized literal: " ++
                          ppReadable iv)
       else if (nBits == 0)
            then when (val /= 0) sizeErr
            else when ((val >= 2^nBits) || (val < -(2^(nBits-1)))) sizeErr
    -- convert the possibly negative integer to a bit vector
    let l' = CLiteral pos (LInt (iv { ilValue = mask nBits val }))
    tiExpr as td (cVApply (idFromSizedInteger pos)
                  [(CHasType (CLitT ty l') qty)])

-- insert fromReal for real literals
tiExpr as td exp@(CLit l@(CLiteral pos (LReal iv))) = do
    --traceM("tiExpr: CLiteral: fromReal")
    tiExpr as td (cVApply (idFromReal pos) [CLitT tReal l])

tiExpr as td (CLit l@(CLiteral pos LPosition)) = tiExpr as td (CLitT tPosition l)

tiExpr as td e@(CLitT t _) = do
    eq_ps <- unify e t td
    return (eq_ps, e)

tiExpr as td e@(CAnyT _ _ t) = do
    eq_ps <- unify e t td
    return (eq_ps, e)

tiExpr as td (CBinOp e1 comma e2) | comma == idComma =
    let pos = getIdPosition comma
    in  tiExpr as td (CStruct (Just True) (setIdPosition pos idPrimPair)
                [(setIdPosition pos (unQualId idPrimFst), e1), (setIdPosition pos (unQualId idPrimSnd), e2)])

tiExpr as td (CBinOp e1 op e2) = tiExpr as td (cVApply op [e1, e2])

-- XXX This handles the "hacky encoding of dict" by convInst
tiExpr as td (CHasType (CAny {}) qt@(CQType [_] nt)) | nt == noType = do
    qual_type <- mkQualType qt
    case qual_type of
      [PredWithPositions p poss] :=> _ -> do
          -- poss is probably a list of only one position
          VPred i pwp <- mkVPredFromPred poss p
          let pwp' = addPredPositions pwp poss
          return ([VPred i pwp'], CVar i)
      _ -> internalError ("tiExpr: unexpected mkQualType result")

{- fast special case
tiExpr as td (CHasType (CLit pos l@(LInt _)) (TAp b n)) | b == tBit =
-}

tiExpr as td exp@(CHasType e ct) = do
    --posCheck "D" e
    x <- newVar (getPosition e) "tiExprCHasType"
--    trace ("CHasType " ++ ppReadable (x, e, ct)) $ return ()
    (ps, e') <- tiExpr as td (Cletrec [CLValueSign (CDef x ct [CClause [] [] e]) []] (CVar x))
    return (ps, optTrivLet e')

tiExpr as td (Cif pos e e1 e2) = tiExpr as td (cVApply (id_if pos) [e, e1, e2])

--tiExpr as td exp@(CSub e1 e2) = tiExpr as td (cVApply (id_asub (getPosition e2)) [e1, e2])

tiExpr as td exp@(CSub2 e1 e2 e3) = do
        eq_ps <- case guessBitSize e2 e3 of
                   NoGuess -> return []
                   Guess t -> unify exp t td
                   BadSize sz pos -> err (pos, EBadExtractSize sz)
                   BadIndex idx pos -> err (pos, EBadExtractIndex idx)
        let extractPos = getPosition e2
        (ps, e') <- tiExpr as td (cVApply (idExtract extractPos) [posLiteral extractPos, e1, e2, e3])
        return (eq_ps ++ ps, e')

tiExpr as td exp@(CSubUpdate pos e_vec (e_hi, e_lo) e_rhs) = do
  e_rhs' <- case guessBitSize e_hi e_lo of
              NoGuess -> return e_rhs
              Guess t -> return $ CHasType e_rhs (CQType [] t)
              BadSize sz pos -> err (pos, EBadExtractSize sz)
              BadIndex idx pos -> err (pos, EBadExtractIndex idx)
  let e' = CApply (CVar (idPrimUpdateRangeFn pos)) [posLiteral pos, e_vec, e_hi, e_lo, e_rhs']
  tiExpr as td e'

tiExpr as td exp@(CSub pos e1 e2) = tiSub (ImplRead Nothing) as td pos e1 e2

tiExpr as td exp@(Cinterface pos Nothing ds) = internalError "TCheck.tiExpr: Cinterface Nothing"

-- Converts an interface expr to a struct expr and typechecks that.
-- An interface is a list of definitions, but a struct is a list of exprs,
-- so each def "i = e" is converted to "let {i = e} in i".  Thus, if the
-- def has no explicit type, even though the struct field has a type,
-- the "i" in the expr for the struct field is not nailed down (only its
-- use becomes nailed down).  Thus, ambiguities in "e" are not resolved.
--
-- (The choice of "let {i=e} in i" allows two things: implicit conditions
--  on the method to be preserved, and a user-specified explicit type to
--  be preserved.  If no explicit type was given by the user, you might
--  consider converting the CDefl to just an expr, but there is currently
--  no CSyntax "when" expr to retain the CQual part of the CDefl.)
--
-- Possible solutions:
-- * Typecheck interfaces directly
-- * Do enough checking of the interface type to put explicit types on
--   the field defs
--
-- Chosen solution:
-- * Do nothing here.  Instead, inside typechecking of CStruct fields,
--   in tiField1, we notice that the expr's are then converted again
--   to a def, to call tiExpl'.  There's no point into converting an ifc
--   def to an expr just to converted in forward into a def again.
--   So ... in tiField, look for "let {i=e} in i" and just extract
--   the "e" (to convert backwards, rather than convert forward).
--   The one downside, is that auto adding of _read to variables, won't
--   apply once we remove the "in i" part.
--
tiExpr as td exp@(Cinterface pos (Just ti) ds) = do
    let
        mkFieldPair d = let i = getLName d
                        in  (i, Cletseq [d] (CVar i))
        ifc = CStruct (Just True) ti (map mkFieldPair ds)
    -- check that the user's argument names match those in the type
    -- declaration, and warn if not (if the warning is turned on)
    checkMethodArgNames ti ds
    -- return type-check of the result
    tiExpr as td ifc

tiExpr as td exp@(Cmodule modulePos ms) = do
    s <- getSubst
    v <- newTVar "tiExpr Cmodule" (KStar `Kfun` KStar) exp
    -- let pos = getPosition exp
    case expandSyn (apSub s td) of
      TAp tc t ->  do ms' <- fixup
                      stmts <- mapM toStmt ms'
                      tiExpr as td (Cdo True stmts)
        where isMifc (CMinterface _) = True
              isMifc (CMTupleInterface _ _) = True
              isMifc _ = False
              forceIsMod e = cVApply (idForceIsModuleAt (getPosition e)) [e]
              toStmt (CMStmt (CSExpr n e)) = return (CSExpr n (forceIsMod e))
              toStmt (CMStmt s) = return (s)
              toStmt (CMrules e) = return (CSExpr Nothing (cVApply (idAddRules (getPosition e)) [e]))
              toStmt (CMinterface e@(Cinterface pos Nothing ies)) =
                case leftCon t of
                  Nothing -> err (getPosition exp, ENoTypeSign (pfpString exp))
                  Just ti -> return (CSExpr Nothing (cVApply
                                              (idReturn pos)
                                              [Cinterface pos (Just (setIdPosition pos ti)) ies]))
              toStmt (CMinterface e) = return (CSExpr Nothing (cVApply (idReturn (getPosition e)) [e]))
              toStmt (CMTupleInterface pos es) = return (CSExpr Nothing (cVApply (idReturn pos) [mkTuple pos es]))
              isMExpr (CMStmt (CSExpr _ _)) = True
              isMExpr _ = False
              fixup = case partition isMifc ms of
                        ([], _:_) | isMExpr (last ms) -> return (ms)
                        ([], _)                       -> return (ms ++ [CMinterface (Cinterface modulePos Nothing [])])
                        (m@[ifc], ms')                -> return (ms' ++ m)
                        _                             -> err(getPosition exp, EMultipleInterfaces)
      t -> err (getPosition exp, ENoTypeSign (pfpString exp))

tiExpr as td exp@(CmoduleVerilog name ui clks rsts args fields sch ps) = do
    (nps, name') <- tiExpr as tString name
    v <- newTVar "tiExpr CmoduleVerilog" KStar exp
    eq_ps <- unify exp (TAp tModule v) td
    s <- getSubst
    sy <- getSymTab

    -- some common definitions for error messages
    let getString (CLit (CLiteral _ (LString x))) = x
        getString x = internalError ("Cmoduleverilog not lit: " ++ show x)
    let name_str = getString name
        name_pos_str = ppReadable (getPosition name)

    -- param or port argument typecheck
    -- params allow strings, ports do not (see ACheck)
    let tiVerilogParam e = do
          v <- newTVar "tiExpr CmoduleVerilog 2 param" KStar e
          let e' = cVApply (idPrimToParam (getPosition e)) [e]
          res <- tiExpr as v e'
          t'  <- expandFullType v
          return (res, t')
    let tiVerilogPort e = do
          v <- newTVar "tiExpr CmoduleVerilog 2 port" KStar e
          let e' = cVApply (idPrimToPort (getPosition e)) [e]
          res <- tiExpr as v e'
          t'  <- expandFullType v
          return (res, t')

    let tiInoutArg e = do
           v <- newTVar "tiExpr CmoduleVerilog 3" KStar e
           res <- tiExpr as v e
           t'  <- expandFullType v
           if isInout_ t'
              then return (res, t')
              else internalError("TCheck: tiInoutArg: " ++ show t')

    -- type-check primitive module argument
    let tiArg (a, e) = do
            ((ps, e'), t) <- case a of
                          (Param _)    -> tiVerilogParam e
                          (Port _ _ _) -> tiVerilogPort e
                          (ClockArg _) -> tiExpr as tClock e >>= (\res -> return (res, tClock))
                          (ResetArg _) -> tiExpr as tReset e >>= (\res -> return (res, tReset))
                          (InoutArg {}) -> tiInoutArg e
            return (ps, t, (a, e'))

        -- This checks the types and number of Verilog ports,
        -- and updates Classic VFI to BSV format
        chkVeriIfc :: [Id] -> VFieldInfo -> TI (VFieldInfo)
        chkVeriIfc self_sbs vfi = do
                let f = vf_name vfi
                    f_str = pfpString f

                (_ :>: sc, _, _) <- findFields v f
                -- traceM(ppReadable sc)
                (_ :=> ft, _)    <- freshInst "D" f sc
                (t, eq_ps) <- unifyFnTo f exp ft v
                when (not . null $ eq_ps) $
                  internalError("TCheck.chkVeriIfc: " ++ ppReadable (exp,v,f,ft,t))
                s <- getSubst
                let mtype = expandSyn (apSub s t)
                let (argTypes, resType) = getArrows mtype

                -- This function checks that the number of port names
                -- matches the number of arguments in the type.
                let chkArgs :: [VPort] -> [Type] -> TI ()
                    chkArgs ports types =
                        if (length ports > length types)
                        then -- The extra port names could be used in the error
                             err (getPosition f,
                                  EForeignModTooManyPorts f_str)
                        else if (length ports < length types)
                        then err (getPosition f,
                                  EForeignModTooFewPorts f_str)
                        else mapM_ chkArgType types

                -- This function checks that the argument types are bitable
                    chkArgType t =
                        if isBit t then
                            return ()
                        else
                            err (getPosition f,
                                 EForeignModBadArgType
                                     (pfpString t) name_str name_pos_str)

                -- Check that the return type is either bitable,
                -- an Action, or an ActionValue, and that the port info
                -- matches the types.
                let
                    -- XXX These errors should give more info
                    chkResType :: [VPort] -> Maybe VPort -> Maybe VPort -> Type ->
                                  TI ([VPort], Maybe VPort, Maybe VPort)
                    chkResType ps me@(Just _) mo@Nothing t =
                        if (isActionWithoutValue t) then return (ps, me, mo)
                        else if (isActionWithValue t)
                        then errMissingValue "ActionValue" t
                        else if (isBit t)
                        then errUnexpectedEnable "value" t
                        else errBadResType t
                    chkResType ps me@Nothing mo@(Just _) t =
                        if (isBit t) then return (ps, me, mo)
                        else if (isActionWithValue t)
                        then errMissingEnable "ActionValue" t
                        else if (isActionWithoutValue t)
                        then errUnexpectedValue "Action" t
                        else errBadResType t
                    chkResType ps me@(Just _) mo@(Just _) t =
                        if (isActionWithValue t) then return (ps, me, mo)
                        else if (isActionWithoutValue t)
                        then errUnexpectedValue "Action" t
                        else if (isBit t)
                        then errUnexpectedEnable "value" t
                        else errBadResType t
                    chkResType ps Nothing Nothing t = do
                        -- must have more than 0 ports
                        when (null ps) $
                          err (getPosition f,
                               EForeignModTooFewPorts (pfpString f))
                        -- update the Classic fieldinfo to BSV format
                        let inputs = initOrErr "chkResType" ps
                        let final_port = lastOrErr "chkResType" ps
                        -- XXX kill PrimAction once imports in Prelude are converted over
                        if (isActionWithoutValue t) || (isPrimAction t)
                         then return (inputs, Just final_port, Nothing)
                         else if (isBit t)
                               then return (inputs, Nothing, Just final_port)
                               else errBadResType t

                    errBadResType t =
                        err (getPosition f,
                             EForeignModBadResType
                                 (pfpString t) name_str name_pos_str)
                    errMissingValue desc t =
                        err (getPosition f,
                             EForeignModMissingValuePort desc name_str f_str)
                    errMissingEnable desc t =
                        err (getPosition f,
                             EForeignModMissingEnablePort desc name_str f_str)
                    errUnexpectedValue desc t =
                        err (getPosition f,
                             EForeignModUnexpectedValuePort
                                 desc name_str f_str)
                    errUnexpectedEnable desc t =
                        err (getPosition f,
                             EForeignModUnexpectedEnablePort
                                 desc name_str f_str)

                    errActionSelfSB f =
                        err (getPosition f, EActionSelfSB [f_str])

                    errNotClockType t =
                        err (getPosition f, EForeignModNotClockType
                                              f_str (pfpString t)
                                              name_str name_pos_str)
                    errNotResetType t =
                        err (getPosition f, EForeignModNotResetType
                                              f_str (pfpString t)
                                              name_str name_pos_str)
                    errClockHasArgs =
                        err (getPosition f, EForeignModClockHasArgs
                                              f_str name_str name_pos_str)
                    errResetHasArgs =
                        err (getPosition f, EForeignModResetHasArgs
                                              f_str name_str name_pos_str)
                    errNotInoutType t =
                        err (getPosition f, EForeignModNotInoutType
                                              f_str (pfpString t)
                                              name_str name_pos_str)
                    errInoutHasArgs =
                        err (getPosition f, EForeignModInoutHasArgs
                                              f_str name_str name_pos_str)

                case vfi of
                    Clock {} -> if (not (isClock resType))
                                then errNotClockType resType
                                else if (null argTypes)
                                then return vfi
                                else errClockHasArgs
                    Reset {} -> if (not (isReset resType))
                                then errNotResetType resType
                                else if (null argTypes)
                                then return vfi
                                else errResetHasArgs
                    Inout {} -> if (not (isInout_ resType))
                                then errNotInoutType resType
                                else if (null argTypes)
                                then return vfi
                                else errInoutHasArgs
                    Method { vf_inputs = inputs, vf_enable = me, vf_output = mo } ->
                            do -- updates inputs, me and mo when processing Classic format
                               (inputs', me', mo') <- chkResType inputs me mo resType
                               -- check if any actions are SB with themselves
                               when (((isActionWithValue resType) ||
                                      (isActionWithoutValue resType) ||
                                      (isPrimAction resType)) &&
                                      (f `elem` self_sbs))
                                    (errActionSelfSB f)
                               chkArgs inputs' argTypes
                               return (vfi { vf_inputs = inputs', vf_enable = me', vf_output = mo' })
    -- paramResults <- mapM tiParam es
    qsses <- mapM tiArg args
--  let   (pses, tys) = unzip paramResults
--        (pss, es') = unzip pses
    let (qss, ts, ses') = unzip3 qsses
    let methnames  = [n | (Method { vf_name = n }) <- fields]
    let clocknames = [c | (Clock c) <- fields]
    let resetnames = [r | (Reset r) <- fields]
    let inoutnames = [n | (Inout { vf_name = n }) <- fields]
    let self_sb_methods =
             let mci = methodConflictInfo sch
             in  [ m | (m,m') <- sSB mci, m == m' ]
    chkSchedInfo methnames sch
    let fieldnames = methnames ++ clocknames ++ resetnames ++ inoutnames
--    traceM("Field names: " ++ ppReadable(fieldnames))
    -- monadic evaluations for ty below
--    tyM1 <- mapM (\ e -> newTVar "tiExpr CmoduleVerilog 4" KStar e) es
--    tyM2 <- mapM (\ t -> newTVar "tiExpr CmoduleVerilog 5" KStar t) ts
    case leftCon (expandSyn (apSub s v)) of
     Just ti | mfs /= Nothing ->
                -- check for extra fields first
                case fieldnames \\ fs of
                  i:_ -> err (getIdPosition i, EForeignModNotField
                                                   (pfpString ti) (pfpString i))
                  [] -> -- now check for missing fields
                      case fs \\ fieldnames of
                        i:_ -> err (getIdPosition i,
                                    EForeignModMissingField (pfpString i)
                                        name_str name_pos_str)
                        _ -> do fields' <- mapM (chkVeriIfc self_sb_methods) fields
                                let e' = CmoduleVerilogT ty name' ui clks rsts
                                                         ses' fields' sch ps
                                return (eq_ps ++ nps {- ++ concat pss -} ++ concat qss, e')
        where mfs = getIfcFields ti sy
              Just fs0 = mfs
              fs = {- trace ("fields:" ++ ppReadable fs0) $ -} map unQualId fs0
              ty = foldr fn td ts
     _ -> err (getPosition exp, ENotAnInterface)

tiExpr as td exp@(CForeignFuncC link_id wrap_cqt) = do
    -- the "wrap_type" should be identical to "td"
    s <- getSubst
    let src_type = expandSyn (apSub s td)
        (argTypes, resType) = getArrows src_type
        -- for positions for new CSyntax constructs
        pos = getPosition link_id
    let bits = CTypeclass idBits

    -- functions for analyzing the argument and result type
    let isPrimArg t = (isTypeBit t) || (isTypeString t)
        isPrimRes t = (isTypeBit t) ||
                      (isTypePrimAction t) || (isTypeActionValue_ t)

    -- given a type, find its bit-size
    let findBitSize t = do
            szv <- newTVar "findBitSize" KNum t
            let ctx = CPred bits [t, szv]
            return ([ctx], szv)

    -- determine the prim types and csyntax wrappers
    let -- return the primitive type, any contexts, and the csyntax
        -- for converting the wrapper argument to the primitive
        mkArg (t,i) | isPrimArg t = return ([], t, CVar i)
        mkArg (t,i) = do (ctxs, prim_sz) <- findBitSize t
                         let prim_t = TAp tBit prim_sz
                             cexpr = cVApply idPack [CVar i]
                         return (ctxs, prim_t, cexpr)

        -- determine the result wrapper based on the return type.
        -- returns (ctxs, prim type, csyntax expr func)
        mkRes =
                -- return type cannot be a string
                if (isTypeString resType)
                then err (getPosition pos, EForeignFuncStringRes)
                -- primitive types don't need conversion
                else if (isPrimRes resType)
                then return ([], resType, \e -> e)
                -- convert ActionValue types
                else if (isTypeActionValue resType)
                then do let cexpr = \e -> cVApply idFromActionValue_ [e]
                            av_arg = getActionValueArg resType
                        when (isTypeString av_arg) $
                            err (getPosition pos, EForeignFuncStringRes)
                        (ctxs, prim_sz) <- findBitSize av_arg
                        let prim_t = TAp tActionValue_ prim_sz
                        return (ctxs, prim_t, cexpr)
                -- anything else must be bitifiable
                else do let cexpr = \e -> cVApply idUnpack [e]
                        (ctxs, prim_sz) <- findBitSize resType
                        let prim_t = TAp tBit prim_sz
                        return (ctxs, prim_t, cexpr)

    -- get the pieces of the CSyntax
    pattern_var_ids <-
        mapM (\t -> newVar (getPosition t) "tiExprCForeignFuncC") argTypes
    let pat_args = map CPVar pattern_var_ids

    -- construct info for the arguments
    arg_triples <- mapM mkArg (zip argTypes pattern_var_ids)
    let (arg_ctxss, arg_prim_tys, arg_cexprs) = unzip3 arg_triples
    let arg_ctxs = concat arg_ctxss

    -- construct info for the result
    (res_ctxs, res_prim_ty, res_cexpr_func) <- mkRes

    let prim_basetype = foldr fn res_prim_ty arg_prim_tys
        --ctxs = res_ctxs ++ arg_ctxs
        --prim_type = CQType ctxs prim_basetype

    -- ----------
    -- for better error message reporting, check the "ctxs" here

    -- get the available epreds
    epreds <- getExplPreds

    -- function to extract the type which is not bitifiable
    let extractType vp =
            case (toPred vp) of
                (IsIn c [t,_]) | (Pred.name c == bits) -> t
                p -> internalError ("tiExpr CForeignFuncC: extractType: " ++
                                    ppReadable p)
    -- for polymorphic types, suggest that the user add a proviso
    let hasTyVar t = not (null (tv t))

    -- function to check predicates
    let checkCtxs ctxs errmsg = do
            (vqs :=> _) <- mkQualType (CQType ctxs prim_basetype)
            vpreds <- concatMapM (mkVPred (getPosition exp)) vqs
            -- see whether they can be satisfied
            (unsat_vpreds, _) <- satisfy epreds vpreds
            -- report any unsatisfied preds as errors
            let mkPair vp = let t = extractType vp
                            in  (pfpString t, hasTyVar t)
            when (not (null unsat_vpreds)) $
                err (pos, errmsg (map mkPair unsat_vpreds))

    checkCtxs arg_ctxs EForeignFuncBadArgType
    -- there should not be more than one result ctx
    let resErr [(t,b)] = EForeignFuncBadResType t b
        resErr _ = internalError ("tiExpr CForeignFuncC: res ctx")
    checkCtxs res_ctxs resErr

    -- ----------

    -- put the CSyntax together
    il <- newVar pos "tiExprCForeignFuncC"
    let -- the foreign is given the basetype, without the contexts
        prim_expr = CForeignFuncCT link_id prim_basetype
        wrapper_expr = res_cexpr_func (CApply prim_expr arg_cexprs)
        clause = CClause pat_args [] wrapper_expr
        defl_cqt = CQType [] src_type
        defl = CLValueSign (CDef il defl_cqt [clause]) []
        new_expr = Cletseq [defl] (CVar il)
    --traceM("new_expr = " ++ ppReadable new_expr)
    -- rather than duplicate the dictionary work that tiExpl does,
    -- just call tiExpr on the new_expr here
    tiExpr as td new_expr

-- This is needed because we call tiExpr on the new_expr in type checking
-- for CForeignFuncC, which contains CForeignFuncCT.
tiExpr as td exp@(CForeignFuncCT link_id prim_ty) = do
    eq_ps <- unify exp prim_ty td
    return (eq_ps, exp)

tiExpr as td e@(Cdo False ss) = do
    v <- newTVar "tiExpr Cdo False" (KStar `Kfun` KStar) e
    tiStmts v Nothing as td ss

tiExpr as td e@(Cdo True ss) = do
    v <- newTVar "tiExpr Cdo True" (KStar `Kfun` KStar) e
    ss' <- recStmts ss
    tiStmts v Nothing as td ss'

tiExpr as td e@(Caction pos ss) = tiRecoveringFromError
                                  (tiAction as td pos ss)
                                  (return ([],e))

tiExpr as td e@(Crules ps rs) = do
    unifyNoEq "Crules" e tRules td
    psrs <- mapM (tiRule as) rs
    let (pss, rs') = unzip psrs
    return (concat pss, Crules ps rs')

tiExpr as td e@(Cattributes pps) = do
    unifyNoEq "Cattributes" e tAttributes td
    return ([], e)

tiExpr as td e0@(Cwrite write_pos lhs rhs) = do
    unifyNoEq "Cwrite" e0 tAction td
    -- traceM ("Cwrite top before: " ++ ppReadable e0)
    new_e <- rebuild lhs
               -- pre_ifc_cont
               ifc_error
               (\t -> (CApply (CSelect lhs (write_id t)) [rhs]))
               id
    -- traceM ("Cwrite top after: " ++ ppReadable new_e)
    tiExpr as td new_e

  where write_id t = let wid = id_write write_pos
                     -- if we have a TyCon, get its qualifier,
                     -- otherwise leave id unqualified
                     -- supports <= magic on interfaces whose fields
                     -- might not be visible (see 1213)
                     in case (leftCon t) of
                          Nothing -> wid
                          Just i -> setIdQual wid (getIdQual i)

        ifc_error t = err (write_pos, EAssignNotReg (pfpString t))
        -- x[i] <= v
        rebuild e_sel@(CSub pos select_lhs i) pre_ifc_cont ifc_cont pure_expr =
          rebuild
            select_lhs
            -- pre_ifc_cont
            (\_ -> do -- don't need the interior type for error reporting
               -- traceM("Cwrite select: " ++ ppReadable e_sel)
               t <- tiForType as (noRead e_sel)
               -- traceM ("Cwrite select t: " ++ ppReadable t)
               flags <- getFlags
               r <- getSymTab
               if writeableIfc flags r t || isTVar t then
                  return (ifc_cont t)
                else
                  pre_ifc_cont t)
            -- ifc_cont
            (\t ->
               let v' = pure_expr rhs -- finish feeding rhs into stacked updates
               in (CApply (CVar (idPrimWriteFn pos)) [posLiteral pos, (noRead select_lhs), i, v']))
            -- pure_expr
            (\rhs -> let v' = pure_expr rhs
                     in (CApply (CVar (idPrimUpdateFn pos)) [posLiteral pos, select_lhs, i, v']))

        -- x.a <= v
        rebuild e_dot@(CSelect expr id) pre_ifc_cont ifc_cont pure_expr =
          rebuild
            expr
            -- pre_ifc_cont
            (\_ -> do -- don't need the interior type for error reporting
               -- traceM("Cwrite struct: " ++ ppReadable e_dot)
               t <- tiForType as (noRead e_dot)
               -- traceM("Cwrite struct t: " ++ ppReadable e_dot)
               flags <- getFlags
               r <- getSymTab
               if writeableIfc flags r t || isTVar t then
                 return (ifc_cont t)
                else
                 pre_ifc_cont t)
          -- ifc_expr
          (\t ->
             let v' = pure_expr rhs
                 struct' = (CStructUpd (CSelect (noRead expr) (id_read (getPosition expr)))
                                     [(id, v')])
             in (CApply (CSelect expr (write_id t)) [struct']))
          -- pure_expr
          (\rhs -> let v' = pure_expr rhs
                   in (CStructUpd expr [(id, v')]))

        rebuild e_range@(CSub2 expr eh el) pre_ifc_cont ifc_cont pure_expr = do

          rebuild
            expr
            ifc_error
            (\t -> (CApply (CSelect expr (write_id t)) [range_update rhs]))
            range_update
         where pos = getPosition e_range
               range_update rhs = CSubUpdate pos expr (eh, el) v'
                  where v' = pure_expr rhs

        -- x <= v (base case)
        rebuild lhs pre_ifc_cont ifc_cont pure_expr = do
          t <- tiForType as (noRead lhs)
          -- traceM ("Cwrite base t: " ++ ppReadable t)
          flags <- getFlags
          r <- getSymTab
          if writeableIfc flags r t || isTVar t then
             return (ifc_cont t)
           else
             pre_ifc_cont t

tiExpr _ td exp = internalError ("TCheck.tiExpr: no match: " ++
                                 ppReadable (td, exp) ++
                                 "DEBUG:\n" ++
                                 ppDebug (td,exp) ++ "\n" ++
                                 (show exp))

tiAction :: [Assump] -> Type -> Position -> CStmts -> TI ([VPred], CExpr)
tiAction as td pos ss = do
    let ss' = case reverse ss of
                CSExpr _ _ : _ -> ss
                _ -> ss ++ [CSExpr Nothing $
                              cVApply (idReturn pos)
                                [CStruct (Just True) (setIdPosition pos idPrimUnit) []]]
    --trace (ppReadable (td, ss')) $ return ()
    unifyNoEq "tiAction" (Caction pos ss) tAction td
    ss'' <- recStmts ss'
    tiStmts tActionValue (Just tAction) as tAction ss''

-- system task checking functions
taskCheckNormal :: TaskCheckT
taskCheckNormal as td f es =
    do
      tiExpr as td (CApply f es)

litOne :: Position -> CExpr
litOne pos = CLit (CLiteral pos (LInt (ilDec 1)))

taskCheckRandom :: [Assump] -> Type -> CExpr -> [CExpr] -> TI ([VPred],CExpr)
taskCheckRandom as td f [] =
      do
        let pos = (getPosition f)
        let tav = TAp (tActionValueAt pos) (TAp tInt t32)
        eq_ps <- unify f tav td

        finishSWriteAV as td t32 f [] [] eq_ps

taskCheckRandom as td f es@[e] =
      do
        let pos = (getPosition f)
        let tav = TAp (tActionValueAt pos) (TAp tInt t32)
        eq_ps <- unify f tav td

        let pos' = getPosition e

        v <- newTVar "taskCheckRandom" KNum e
        let targ = TAp tInt v
        res <- tiExpr as targ e

        let e' = cVApply (setIdPosition pos' idPack) [e]
        let targ' = TAp tBit v
        res' <- tiExpr as targ' e'
        t' <- expandFullType targ'
        let pr =(res', t', [])

        finishSWriteAV as td t32 f es [pr] eq_ps

taskCheckRandom as td f es =
    do x <- err (getPosition f, (ETaskMismatchNumArgs "$random" "0 or 1" (toInteger (length es))))
       return x

taskCheckFinish :: [Assump] -> Type -> CExpr -> [CExpr] -> TI ([VPred],CExpr)
-- make finish() into finish(1)
taskCheckFinish as td f [] = tiExpr as td (CApply f [litOne pos])
  where pos = getPosition f
taskCheckFinish as td f es = tiExpr as td (CApply f es)

taskCheckFatal :: [Assump] -> Type -> CExpr -> [CExpr] -> TI([VPred], CExpr)
taskCheckFatal as td f [] = taskCheckFatal as td f [litOne pos]
  where pos = getPosition f
taskCheckFatal as td f (code:es) = do
  -- the code is really the same as a finish argument,
  -- so check is as Bit 2, but pass it on as Bit 32
  let pos    = getPosition f
  let code'  = CHasType code (CQType [] (tBitN 2 pos))
  let ext    = CVar (setIdPosition pos idPrimZeroExt)
  let code'' = CHasType (CApply ext [code']) (CQType [] bit32)
  taskCheckDisplay as td f (code'':es)

-- Checks on display param, and converts it to a "native" bit or string type along with
-- any other VPred as needed.
-- [VPred]
-- CExpr
-- Type
-- CStmts are generated for action value functions (e.g. $time) in argument list.
checkDisplayParam :: Bool -> Bool -> [Assump] -> CExpr
                  -> TI (([VPred], CExpr), Type, CStmts)
checkDisplayParam av_ok fmt_ok as e =
    do
      v <- newTVar "checkDisplayParam start" KStar e
      res@(ps, e') <- tiExpr as v e
      t <- expandFullType v
      let pos = getPosition e

      case t of
        _ | fmt_ok && isFmt t -> return (res, t, [])
        _ | isBit t || isString t || isReal t -> return (res, t, [])
        _ | isChar t ->
          do res' <- tiExpr as tString (cVApply (idPrimCharToString pos) [e])
             return (res', tString, [])
        -- if it is an Integer force to (signed) 32 bits
        -- XXX: should we force laundering through Int 32 (but maybe it is cleaner)
        _ | isInteger t ->
          do res' <- tiExpr as bit32 (CApply (CVar (idSigned pos)) [(cVApply (idFromInteger pos) [e])])
             return (res', bit32, [])
        -- force signed display of Int
        _ | isInt t ->
          do
            v' <- newTVar "checkDisplayParam pack Int" KStar e
            res' <- tiExpr as v' (CApply (CVar (idSigned pos))
                                       [(cVApply (setIdPosition pos idPack) [e])])
            t' <- expandFullType v'
            return (res', t', [])
        -- force unsigned display of UInt
        _ | isUInt t ->
          do
            v' <- newTVar "checkDisplayParam pack UInt" KStar e
            res' <- tiExpr as v' (CApply (CVar (idUnsigned pos))
                                       [(cVApply (setIdPosition pos idPack) [e])])
            t' <- expandFullType v'
            return (res', t', [])
        -- bind an ActionValue and display the result
        _ | av_ok && isActionValue t ->
          do
            -- traceM("ActionValue: " ++ ppReadable (t,e) )
            freshId <- newVar (getPosition e) "checkDisplayParam"
            let boundtype = getAVType t
            -- traceM("Bound type: " ++ ppReadable boundtype)
            let cqtype = CQType [] boundtype -- XXX what if there are provisos?
            -- traceM("CQType: " ++ ppReadable cqtype)
            let scheme = toScheme boundtype
            -- traceM("Scheme: " ++ ppReadable scheme)
            let stmt = CSBindT (CPVar freshId) Nothing [] cqtype e
            -- traceM("stmt: " ++ ppReadable stmt)
            (res', t', stmts) <- checkDisplayParam av_ok fmt_ok [freshId :>: scheme] (CVar freshId)
            -- the original expression will be rechecked as part of typechecking the resulting action block
            return (res', t', stmt:stmts)
        _ -> -- fall through and look at provisos
           do
             ps' <- apSubTI ps
             let ptvars = tv ps'
             case t of
               -- the original tvar has been constrained by a proviso
               TVar tvar | tvar `elem` ptvars -> do
                 -- traceM ("proviso variable: " ++ (ppReadable t))
                 bits <- bitCls
                 literal <- literalCls
                 realLiteral <- realLiteralCls
                 sizedLiteral <- sizedLiteralCls
                 stringLiteral <- stringLiteralCls
                 -- duplicate provisos are possible, so remove them
                 let preds = nub [ pred | (VPred _ pp) <-  ps',
                                          let pred = removePredPositions pp,
                                          tvar `elem` (tv pred)]
                 -- traceM("proviso predicates: " ++ (ppReadable preds))
                 let bitsprovisos = [tnum | (IsIn c [tbind, tnum]) <- preds,
                                            c == bits, tbind == t]
                 let literalprovisos = [p | p@(IsIn c [tbind]) <- preds,
                                            c == literal, tbind == t]
                 let rlprovisos = [p | p@(IsIn c [tbind]) <- preds,
                                       c == realLiteral, tbind == t]
                 let szprovisos = [tnum | (IsIn c [tbind, tnum]) <- preds,
                                          c == sizedLiteral, tbind == t]
                 let strprovisos = [p | p@(IsIn c [tbind]) <- preds,
                                        c == stringLiteral, tbind == t]
                 if (not . null) bitsprovisos then do
                     -- traceM("bits provisos: " ++ (ppReadable bitsprovisos))
                     -- XXX can we just let defaulting handle this?
                     let bit_t = TAp tBit (headOrErr "checkDisplayParam: bitsprovisos" bitsprovisos)
                     -- consider the value as unsigned
                     res' <- tiExpr as bit_t e
                     return (res', bit_t, [])
                  else if ((not . null) literalprovisos) then do
                     -- traceM("literal provisos: " ++ (ppReadable literalprovisos))
                     _ <- unify e bit32 t
                     -- consider the value signed
                     -- also: insert the fromInteger here, even though there
                     -- is one around the literals, because there may also be
                     -- operators and we want to force the conversion to bit32
                     -- at the last possible minute, in case the ops are only
                     -- defined for Integer (e.g. "2 ** -1")
                     res' <- tiExpr as bit32 (CApply (CVar (idSigned pos))
                                                     [cVApply (idFromInteger pos) [e]])
                     return (res', bit32, [])
                  else if ((not . null) rlprovisos) then do
                     -- traceM("real literal provisos: " ++ (ppReadable rlprovisos))
                     _ <- unify e tReal t
                     -- fromReal is not needed because the value is already Real
                     res' <- tiExpr as tReal e
                     return (res', tReal, [])
                  else if ((not . null) szprovisos) then do
                     -- traceM("sized literal provisos: " ++ ppReadable szprovisos)
                     -- XXX can we just let defaulting handle this?
                     let bit_t = TAp tBit (headOrErr "checkDisplayParam: szprovisos" szprovisos)
                     _ <- unify e bit_t t
                     -- fromSizedLiteral is not needed because the value is already Bit
                     res' <- tiExpr as bit_t e
                     return (res', bit_t, [])
                  else if ((not . null) strprovisos) then do
                     -- XXX let defaulting handle it?
                     _ <- unify e tString t
                     res' <- tiExpr as tString e
                     return (res', tString, [])
                  else do -- traceM("default to pack")
                          packResult as e
               -- default is to explicitly pack the result
               _ ->
                   do
                     packResult as e

checkAssertParam :: [Assump] -> CExpr -> TI (([VPred], CExpr), Type, CStmts)
checkAssertParam as e =
    do
      v <- newTVar "checkAssertParam start" KStar e
      res@(ps, e') <- tiExpr as v e
      t <- expandFullType v
      let pos = getPosition e

      case t of
        _ | isString t -> return (res, t, [])
        _ | isChar t ->
          do
            res' <- tiExpr as tString (cVApply (idPrimCharToString pos) [e])
            return (res', tString, [])
        _ | isBool t || isUInt t ->
          do
            v' <- newTVar "checkAssertParam pack" KStar e
            res' <- tiExpr as v' (cVApply (setIdPosition pos idPack) [e])
            t' <- expandFullType v'
            return (res', t', [])
        _ -> -- fall through and look at provisos
           do
             ps' <- apSubTI ps
             let ptvars = tv ps'
             case t of
               -- the original tvar has been constrained by a proviso
               TVar tvar | tvar `elem` ptvars -> do
                 -- traceM ("proviso variable: " ++ (ppReadable t))
                 do
                   -- duplicate provisos are possible, so remove them
                   let preds = nub [ pred | (VPred _ pp) <-  ps',
                                            let pred = removePredPositions pp,
                                            tvar `elem` (tv pred)]
                   -- traceM("proviso predicates: " ++ (ppReadable preds))
                   literal <- literalCls
                   stringLiteral <- stringLiteralCls
                   let literalprovisos = [p | p@(IsIn c [tbind]) <- preds,
                                              c == literal, tbind == t]
                   let stringprovisos = [p | p@(IsIn c [tbind]) <- preds,
                                             c == stringLiteral, tbind == t]
                   (if ((not . null) literalprovisos) then
                     do
                       -- traceM("literal provisos: " ++ (ppReadable literalprovisos))
                         _ <- unify e tInteger t
                         res' <- tiExpr as tInteger e
                            -- res' <- tiExpr as bit32 e
                         return (res', tInteger, [])
                    else if ((not . null) stringprovisos) then do
                       _ <- unify e tString t
                       res' <- tiExpr as tString e
                       return (res', tString, [])
                    else do internalError ("TCheck.SVAParam: " ++ show e))
               _ ->
                   do internalError ("TCheck.SVAParam: " ++ show t)

-- CStmts are null
-- the incantation to pack the result is repeated
packResult :: [Assump] -> CExpr -> TI (([VPred], CExpr), Type, CStmts)
packResult as e =
    do
      v' <- newTVar "checkDisplayParam packResult pack" KStar e
      let e' = (cVApply (setIdPosition (getPosition e) idPack) [e])
      res' <- tiExpr as v' e'
      t' <- expandFullType v'
      return (res', t', [])


-- Check a display task were the first argument must be of type File
taskCheckFDisplay :: [Assump] -> Type -> CExpr -> [CExpr] -> TI ([VPred],CExpr)
taskCheckFDisplay as td f []  = err (getPosition f, (EMissingFileArgument (ppReadable f) "File" "first" ))
taskCheckFDisplay as td f (file:es)  =
      do
        -- the first argument must be a file,  handle all rest in the same way
        _ <- tiExpr as tFile file
        --
        taskCheckDisplay as td f (file:es)

taskCheckDisplay :: [Assump] -> Type -> CExpr -> [CExpr] -> TI ([VPred],CExpr)
taskCheckDisplay as td f es =
      do
        _ <- unify f tAction td -- check type so fromPrimAction will succeed
                           -- f is used for its position only
        paramResults <- mapM (checkDisplayParam True True as) es
        finishDisplay as td f es paramResults

taskCheckAssert :: [Assump] -> Type -> CExpr -> [CExpr] -> TI ([VPred],CExpr)
taskCheckAssert as td f es =
      do
        _ <- unify f tAction td -- check type so fromPrimAction will succeed
                                -- f is used for its position only
        paramResults <- mapM (checkAssertParam as) es
        -- OK to use finishDisplay here:
        finishDisplay as td f es paramResults

-- Check a display task where the first argument must be an interface
-- with a write method.
taskCheckSWrite :: [Assump] -> Type -> CExpr -> [CExpr] -> TI ([VPred],CExpr)
taskCheckSWrite as td f es =
      do
        expr <- createAVExpr as td f es
        tiExpr as td expr

-- Convert a call to a standard swrite, etc into a call to the AV version
-- and an invocation of the write method on the supplied interface.
createAVExpr :: [Assump] -> Type -> CExpr -> [CExpr] -> TI CExpr
createAVExpr _  _  f []        = err (getPosition f, (EMissingFileArgument (ppReadable f) "interface" "first"))
createAVExpr as td f (dest:es) =
      do
        let pos = (getPosition f)
        let (CVar task) = f
        let id_av = toAVId(task)
        v <- newTVar "createAVExpr" KStar f
        _ <- tiExpr as v dest
        s' <- getSubst
        let ifc = (apSub s' v)
        let (con, args) = splitTAp ifc
        con_id <- case (leftCon con) of
                     Nothing -> err (pos, (EMissingFileArgument (ppReadable f) "interface" "first" ))
                     Just x  -> return x
        sy <- getSymTab
        info <- case (findFieldInfo sy con_id (id_write pos)) of
                     Nothing -> err (pos, (EMissingFileArgument (ppReadable f) "interface (with an _write method)" "first" ))
                     Just x  -> return x
        let (_ :>: (Forall _ qt)) = fi_assump info
        let (_ :=> tt) = inst args qt
        let ((_:rest), _) = getArrows tt
        t <- case (rest) of
                [x] -> return x
                _   -> err (pos, (EMissingFileArgument (ppReadable f) "interface (with an _write method)" "first" ))
        id_new <- createIdNew dest pos
        let expr = (Caction pos [(CSBindT (CPVar id_new) Nothing []
                                  (CQType [] t)
                                  (CTaskApply (CVar id_av) es)),
                                 (CSExpr Nothing (Cwrite pos dest (CVar id_new)))])
        return expr

createIdNew :: CExpr -> Position -> TI Id
createIdNew dest pos =
    do
      let mkNewId id = setIdBase id (concatFString [getIdBase id, (mkFString "_AV")])
      id_new <- case (dest) of
                  (CApply (CVar f) [CVar id]) | ((getIdBase f) == (getIdBase idAsIfc))
                                                  -> return (mkNewId id)
                  (CApply (CVar f) [CVar id]) | ((getIdBase f) == (getIdBase idAsReg))
                                                  -> return (mkNewId id)
                  (CVar id) -> return (mkNewId id)
                  _         -> newVar pos "createIdNew"
      return id_new

taskCheckSWriteAV :: [Assump] -> Type -> CExpr -> [CExpr] -> TI ([VPred],CExpr)
taskCheckSWriteAV as td f es =
      do
        v <- newTVar "taskCheckSWriteAV" KNum f
        let pos = (getPosition f)
        let tav = TAp (tActionValueAt pos) (TAp tBit v)
        eq_ps <- unify f tav td

        paramResults <- mapM (checkDisplayParam True True as) es
        finishSWriteAV as td v f es paramResults eq_ps


finishDisplay :: [Assump] -> Type -> CExpr -> [CExpr] -> [(([VPred], CExpr), Type, CStmts)] -> TI ([VPred],CExpr)
finishDisplay as td f es paramResults =
     do
        s' <- getSubst

        -- want to squash all known type variables
        let paramResults' = (apSub s' paramResults)
        let (pses, tys, stmtss) = unzip3 paramResults'
        let stmts = concat stmtss

        -- pss are the provisos, es' are the transformed expressions
        let (pss, es') = unzip pses

        let taskty = foldr fn tPrimAction tys

        -- XXX: quantifying in IConv instead so free type vars are caught correctly
        -- duplicate provisos are possible so remove them
        -- let cpreds = ((map predToCPred) .  nub) [ pred | (VPred _ pred) <-  (concat pss), (not . null) ((tv taskty) `intersect` (tv pred))]
        -- let taskcqt = (CQType [] taskty)
        --traceM (ppReadable taskcqt)
        --traceM (ppReadable (tv taskcqt))

        -- XXX: using (tv taskcqt) would assume all type vars found are free in taskcqt
        -- but free in taskcqt does not imply free altogether (may be constrained externally)
        --                    [(CTaskApplyT (CVar task) taskcqt (map TVar (tv taskcqt)) es')])

        -- insert fromPrimAction so $display & friends have type Action
        let action_exp = (cVApply (setIdPosition (getPosition f) idFromPrimAction)
                                  [(CTaskApplyT f taskty es')])
        --let action_exp = (CTaskApplyT f taskty es')

        let exp' = if (null stmts) then
                      action_exp
                   else
                      (Caction (getPosition f) (stmts ++ [CSExpr Nothing action_exp]))


        (ps', exp'') <- tiExpr as td exp'
        -- traceM("finishDisplay done")
        -- duplicate provisos are possible so squash them
        return (concat (ps':pss), exp'')

finishSWriteAV :: [Assump] -> Type -> Type -> CExpr -> [CExpr] -> [(([VPred], CExpr), Type, CStmts)] -> [VPred] -> TI ([VPred],CExpr)
finishSWriteAV as td v f es paramResults eq_ps =
     do
        s' <- getSubst

        -- want to squash all known type variables
        let paramResults' = (apSub s' paramResults)
        let (pses, tys, stmtss) = unzip3 paramResults'
        let stmts = concat stmtss

        -- pss are the provisos, es' are the transformed expressions
        let (pss, es') = unzip pses

--        v <- newTVar "XXX" KNum f
        let tav = TAp tActionValue_ v
        let taskty = foldr fn tav tys

        -- XXX: quantifying in IConv instead so free type vars are caught correctly
        -- duplicate provisos are possible so remove them
        -- let cpreds = ((map predToCPred) .  nub) [ pred | (VPred _ pred) <-  (concat pss), (not . null) ((tv taskty) `intersect` (tv pred))]
        -- let taskcqt = (CQType [] taskty)
        --traceM (ppReadable taskcqt)
        --traceM (ppReadable (tv taskcqt))

        -- XXX: using (tv taskcqt) would assume all type vars found are free in taskcqt
        -- but free in taskcqt does not imply free altogether (may be constrained externally)
        --                    [(CTaskApplyT (CVar task) taskcqt (map TVar (tv taskcqt)) es')])

        -- insert fromActionValue_ so $swtriteAV & friends have type ActionValue
        let av_exp = (cVApply (setIdPosition (getPosition f) idFromActionValue_)
                                  [(CTaskApplyT f taskty es')])
        --let action_exp = (CTaskApplyT f taskty es')

        let exp' = if (null stmts) then
                  av_exp
                  else
--                (Caction (getPosition f) (stmts ++ [CSExpr Nothing av_exp]))
                  (Cdo False (stmts ++ [CSExpr Nothing av_exp]))

        (ps', exp'') <- tiExpr as td exp'

        -- duplicate provisos are possible so squash them
        return (concat (eq_ps:ps':pss), exp'')


-- $fflush can be either fflush :: PrimAction or fflush :: File -> PrimAction
taskCheckFFlush :: TaskCheckT
taskCheckFFlush as td f [] =
    do
      let fty = tPrimAction
          applied = (CTaskApplyT f  fty   [])
      let t = cVApply (setIdPosition (getPosition f) idFromPrimAction) [applied]
      --
      tiExpr as td t
taskCheckFFlush as td f [file] =
    do
      -- first arg must be file type
      _ <- tiExpr as tFile file
      ((vp,packedfile),tx,cm) <- packResult as file
      --
      let fty = tx `fn` tPrimAction
          applied = (CTaskApplyT f  fty   [packedfile])
      let t = cVApply (setIdPosition (getPosition f) idFromPrimAction) [applied]
      --
      (pred,exp) <- tiExpr as td t
      return (pred++vp, exp)
taskCheckFFlush as td f args = err (getPosition f, (EMissingFileArgument (ppReadable f) "File" "only" ))


-- Builds fromActionValue_ ( $fopen ( string {,string} ))
taskCheckFOpen :: TaskCheckT
taskCheckFOpen as td f [filen] =
    do
      (vp,filentc) <- tiExpr as tString filen
      --
      let avfile = (TAp (tActionValueAt (getPosition f)) tFile)
          tav32 = TAp (tActionValue_At (getPosition f))  t32
          fty = tString `fn` tav32
          applied = (CTaskApplyT f  fty    [filentc])
      let t = cVApply (setIdPosition (getPosition f) idFromActionValue_) [applied]
      --
      unifyNoEq "taskCheckFOpen"  f td avfile
      (preds,exp) <- tiExpr as td t
      return (preds++vp,exp)

taskCheckFOpen as td f [filen,mode] =
    do
      (vp1,filentc) <- tiExpr as tString filen
      (vp2,modetc)  <- tiExpr as tString mode
      --
      --
      let avfile = (TAp (tActionValueAt (getPosition f)) tFile)
          tav32 = TAp (tActionValue_At (getPosition f))  t32
          fty = tString `fn` tString `fn` tav32
          applied = (CTaskApplyT f  fty    [filentc,modetc])
      let t = cVApply (setIdPosition (getPosition f) idFromActionValue_) [applied]
      --
      unifyNoEq "taskCheckFOpen" f td avfile
      (preds,exp) <- tiExpr as td t
      return (preds++vp1++vp2,exp)


taskCheckFOpen as td f _ = err (getPosition f, (EMissingFileArgument (ppReadable f) "String" "first (two)" ))

taskCheckFormat :: [Assump] -> Type -> CExpr -> [CExpr] -> TI ([VPred],CExpr)
taskCheckFormat as td f es =
    do unifyNoEq "taskCheckFormat"  f tFmt td
       paramResults <- mapM (checkDisplayParam False True as) es
       finishFormat as td f es paramResults

finishFormat :: [Assump] -> Type -> CExpr -> a
             -> [(([VPred], CExpr), Type, CStmts)] -> TI ([VPred], CExpr)
finishFormat as td f es paramResults =
     do
        s' <- getSubst

        -- want to squash all known type variables
        let paramResults' = (apSub s' paramResults)
        -- it's OK to ignore the stmts here, because those only result from
        -- binding ActionValue arguments, which we disallowed
        let (pses, tys, _) = unzip3 paramResults'

        -- pss are the provisos, es' are the transformed expressions
        let (pss, es') = unzip pses

        let taskty = foldr fn tFmt tys

        let expr = CTaskApplyT f taskty es'

        (ps', exp'') <- tiExpr as td expr
        return (concat (ps':pss), exp'')

taskCheckMap :: [(Id, TaskCheckT)]
taskCheckMap = [(idTime,      taskCheckNormal),
                (idSTime,     taskCheckNormal),
                (idDumpon,    taskCheckNormal),
                (idDumpoff,   taskCheckNormal),
                (idDumpall,   taskCheckNormal),
                (idDumpvars,  taskCheckNormal),
                (idDumpfile,  taskCheckNormal),
                (idDumpflush, taskCheckNormal),
                (idDumplimit, taskCheckNormal),
                --
                (idDisplay,   taskCheckDisplay),
                (idDisplayo,  taskCheckDisplay),
                (idDisplayb,  taskCheckDisplay),
                (idDisplayh,  taskCheckDisplay),
                (idWrite,     taskCheckDisplay),
                (idWriteo,    taskCheckDisplay),
                (idWriteb,    taskCheckDisplay),
                (idWriteh,    taskCheckDisplay),
                --
                (idErrorTask, taskCheckDisplay),
                (idWarnTask,  taskCheckDisplay),
                (idInfoTask,  taskCheckDisplay),
                (idFatalTask, taskCheckFatal),
                --
                (idSVA,       taskCheckAssert),

                (idSVAsampled, taskCheckNormal),
                (idSVArose, taskCheckNormal),
                (idSVAfell, taskCheckNormal),
                (idSVAstable, taskCheckNormal),
                (idSVApast, taskCheckNormal),
                (idSVAonehot, taskCheckNormal),
                (idSVAonehot0, taskCheckNormal),
                (idSVAisunknown, taskCheckNormal),
                (idSVAcountones, taskCheckNormal),
                --
                (idRandom,    taskCheckRandom),
                --
                (idFDisplay,  taskCheckFDisplay),
                (idFDisplayo, taskCheckFDisplay),
                (idFDisplayb, taskCheckFDisplay),
                (idFDisplayh, taskCheckFDisplay),
                (idFWrite,    taskCheckFDisplay),
                (idFWriteo,   taskCheckFDisplay),
                (idFWriteb,   taskCheckFDisplay),
                (idFWriteh,   taskCheckFDisplay),
                (idSWriteAV,  taskCheckSWriteAV),
                (idSWrite,    taskCheckSWrite),
                (idSWritebAV, taskCheckSWriteAV),
                (idSWriteb,   taskCheckSWrite),
                (idSWriteoAV, taskCheckSWriteAV),
                (idSWriteo,   taskCheckSWrite),
                (idSWritehAV, taskCheckSWriteAV),
                (idSWriteh,   taskCheckSWrite),
                (idSFormatAV, taskCheckSWriteAV),
                (idSFormat,   taskCheckSWrite),
                --
                (idFormat  , taskCheckFormat),
                --
                (idFinish,    taskCheckFinish),
                (idStop,      taskCheckFinish),
                --
                (idFOpen,     taskCheckFOpen),
                (idFFlush,    taskCheckFFlush),
                --
                (idFGetc,     taskCheckNormal),
                (idUngetc,    taskCheckNormal),
                (idFClose,    taskCheckNormal),
                (idTestPlusargs, taskCheckNormal),
                --
                (idRealToBits, taskCheckNormal),
                (idBitsToReal, taskCheckNormal)]

tiApply :: [Assump] -> Type -> a -> CExpr -> CExpr -> TI ([VPred], CExpr)
tiApply as td exp f e = do
    -- give the tyvar the position of the argument?
    -- if the variable pos becomes the position of a pred, this could
    -- result in multiple positions (each argument) for one func call
    --te       <- newTVar "tiExpr CApply" KStar f
    te       <- newTVar "tiExpr CApply" KStar e
    (ps, f') <- tiExpr as (te `fn` td) f
    (qs, e') <- tiExpr as te e

    let ret_ps = ps ++ qs
    ret_ps' <- updateContexts (getPosition f) ret_ps

    --trace ("CApply " ++ ppReadable (exp,te,td)) $ return ()
    return ( ret_ps', cApply 3 f' [e'] )

-- apply register read method to a variable, if the type allows
-- The first argument is whether there is a surrounding selection already
-- being applied.  Do not apply the read selection if any method of the
-- interface is already being applied (a read, a write, or other method).
-- This avoids infinitely applying the read method and it allows users to
-- write to the reg and to apply other methods on Reg-like interfaces.
tiVar :: ImplReadTag -> [Assump] -> Type -> CExpr -> TI ([VPred], CExpr)
tiVar readTag as td exp@(CVar i) = do
    (i' :>: sc) <- findAssump i as

{-
    traceM ("tiVar " ++ pvpReadable i ++ " assumption (vart) " ++
            pvpReadable (apSub s vart) ++ " expects (td) " ++
            pvpReadable (apSub s td))
    traceM ("tiVar isReadType i = " ++
            pvpReadable (isReadType r (apSub s vart)))
    traceM ("tiVar isReadType td = " ++
            pvpReadable (isReadType r (apSub s td)))
-}

    -- prepare the base expression: typecheck the variable
    let base_expr = do
            (ps :=> t, ts) <- freshInstT "E" i sc td
            ps' <- concatMapM (mkVPred (getPosition exp)) ps
            when doRTrace2 $ traceM ("CVar " ++ ppReadable (i,sc,iAPs (CVar i) ts ps'))
            return (t,
                    ps',
                    iAPs (CVar (setIdPosition (getIdPosition i) i')) ts ps')

    let readTag' = if (isRenamingId i) then NoRead else readTag
    tryReadDesugar base_expr readTag' as td exp

{-
    -- Do automagic deref if the variable is a register type and the
    -- context is not a register type, and the variable is not a
    -- renamed identifier (introduced by the BSV parser)
    case (mfield, isReadType r (apSub s vart), isReadType r (apSub s td)) of
      (Just msel, Just ti, Nothing) | not (isRenamingId i) ->
        -- Do automagic deref (except for renamed identifiers)
        let -- the _read should have the same qualifier as the ifc type
            unqual_id_read = id_read (getPosition i)
            qual_id_read = setIdQual unqual_id_read (getIdQual ti)
            -- the result of typechecking i._read
            res = tiExpr as td (CSelectTT ti exp qual_id_read)
        in
            -- don't add _read if a method is being called on the reg ifc
            case (msel, getIfcFields ti r) of
                (Just method, Just fs) ->
                    -- do an unqualified comparison, because the qualifier
                    -- has probably been added by the surrounding typecheck
                    let unqual_fs = map unQualId fs
                    in  if (unQualId method `elem` unqual_fs)
                        then def_res  -- don't insert _read
                        else res      -- insert _read
                _ -> res  -- no surrounding method call, so insert _read
      _ -> def_res
-}

tiVar _ _ _ _ = internalError "TCheck.tiVar"

-- tiVar_NoImplRead = tiVar NoRead

-- tiVar_WithImplRead sel = tiVar (ImplRead sel)

noDesugar :: Type -> TI (Type, [VPred], CExpr)
          -> CExpr -> TI ([VPred], CExpr)
noDesugar td base_expr orig_expr = do
  (t, ps, e) <- base_expr
  eq_ps <- unify orig_expr t td
  s <- getSubst
  return (eq_ps ++ apSub s ps, apSub s e)

tryReadDesugar :: TI (Type, [VPred], CExpr) -> ImplReadTag -> CheckT CExpr
tryReadDesugar base_expr NoRead _ td orig_expr = noDesugar td base_expr orig_expr
tryReadDesugar base_expr (ImplRead msel) as td orig_expr = do
   (t, ps, e) <- base_expr
   let def_res = noDesugar td base_expr orig_expr

   r <- getSymTab
   s <- getSubst

   case (isReadType r (apSub s t), isReadType r (apSub s td)) of
     (Just ti, Nothing) -> do
       let unqual_id_read = id_read (getPosition e)
       -- qualify by the package of the type constructor
       -- so that the desugaring works even if the _read field is not in scope
       let qual_id_read   = setIdQual unqual_id_read (getIdQual ti)
       let read_res = tiExpr as td (CSelectTT ti orig_expr qual_id_read)
       case (msel, getIfcFields ti r) of
         -- compare unqualified because we just care that there is
         -- a matching field - scope is taken care of elsewhere
         -- by the read or write desugaring or normal typechecking
         (Just sel, Just fs) | (unQualId sel) `elem` (map unQualId fs) -> def_res
         _ -> read_res
     _ -> def_res

tiSub :: ImplReadTag -> [Assump] -> Type -> Position -> CExpr -> CExpr
      -> TI ([VPred], CExpr)
tiSub readTag as td pos e1 e2 = tryReadDesugar (tiWithType as exp) readTag as td exp
  where exp = (cVApply (idPrimSelectFn pos) [posLiteral pos, e1, e2])

-----------------------------------------------------------------------------

type TiStmts = Type -> Maybe Type -> [Assump] -> Type -> [CStmt] -> TI ([VPred], CExpr)

-- Transform recursive statements as follows:
-- Let x1,...,xk be the identifiers in forward reference
-- s1; ... sn; e
--   -->
-- n <- mfix (\ t -> let (r,x1,...,xk) = t in do s1; ...; sn; r <- e; return (r, x1, ... xk))
-- return r

recStmts :: [CStmt] -> TI [CStmt]
recStmts = return
{-
recStmts ss = do
    let vs = S.fromList (concatMap getStmtBind ss)
        rchk s r@(rvs, vs) =
            case s of
            CSBindT p _ e -> (rvs `S.union` (snd (getFVE e) `S.intersection` vs), S.difference vs (getPV p))
            CSBind  p   e -> (rvs `S.union` (snd (getFVE e) `S.intersection` vs), S.difference vs (getPV p))
            CSletrec      ds -> let vs' = set_deleteMany (concatMap getLDefs ds) vs
                             in  (rvs `S.union` ((S.unions (map (snd . getFVDl) ds) `S.intersection` vs')), vs')
            _             -> r
        (rvs, _) = foldr rchk (S.empty, vs) (reverse ss)
        ls = S.toList rvs
    -- XXX check dupl
    if null ls then
        return ss
     else do
        let re = case last ss of
                 CSExpr x -> x
                 other -> internalError $ "[BUG #23] recStmts: at " ++ ppString (getPosition other) ++ ":\n" ++ ppReadable other
            pos = getPosition re
        r <- newVar pos
        tid <- newVar pos
        nid <- newVar pos
        let ids = r : ls
            ss' = init ss ++ [CSBind (CPVar r) re, CSExpr (cVApply (idReturn pos) [mkTuple pos (map CVar ids)])]
            ptup = pMkTuple pos (map CPVar ids)
            lame = CLam tid (Cletrec [CLMatch ptup (CVar tid)] (Cdo False ss'))
            rss = [CSBind (CPVar nid) (cVApply idMfix [lame]), CSExpr (cVApply (idReturn pos) [CSelect (CVar nid) idPrimFst])]
--        trace (ppReadable (S.toList vs, ls)) $ return ()
--        trace (ppReadable rss) $ return ()
        return rss
-}

tiStmts :: TiStmts
--tiStmts mon mt as td ss = trace (concatMap (("\nDEBUG: " ++) . show) ss) $ tiStmts' chke mon mt as td ss
tiStmts mon mt as td ss = tiStmts' chke mon mt as td ss
  where chke mon mt as td (CSExpr name e : ss) = do
                v <- newTVar "tiStmts" KStar e
                tiStmtsExpr chke mon mt as td (TAp mon v) name e ss
        chke _ _ _ _ _ = internalError "TCheck.tiStmts chke"

addStateName :: Maybe CExpr -> CExpr -> CExpr
addStateName Nothing e = e
addStateName (Just nameExpr) e =
    let pos = getPosition nameExpr
    in  CApply (CVar (idSetStateNameAt pos)) [nameExpr, e]

tiStmts' :: TiStmts -> TiStmts
tiStmts' chke mon _ as td [CSExpr name e] =
        -- XXX can "name" ever be non-Nothing here?
        tiExpr as td (addStateName name e)
tiStmts' chke mon _ as td [s] = err (getPosition s, ENotExpr)
tiStmts' chke mon mt@(Just te) as td (CSExpr name e : ss) =
        tiStmtsExpr chke mon mt as td te name e ss
tiStmts' chke mon mt as td ss@(CSExpr _ _ : _) = chke mon mt as td ss
tiStmts' chke mon _ as td (e@(CSBindT _ _ _ (ty@(CQType (_:_) _)) _) : _) =
        -- XXX this used to report the position of "ty"
        -- XXX is that ever the right thing to do?
        err (getPosition e, EStmtContext (pfpString ty))
tiStmts' chke mon mt as td (CSBindT (CPVar i) maybeName pprops (CQType [] ty) e : ss) = do
        bs <- getBoundTVs
        -- Of the type variables in the explicit declaration, separate the
        -- free type variables (fvs) from those bound by the context (bvs)
        let (bvs, fvs) = partition (\x -> elem x bs) (tv ty)
        -- Check that the variables bound in this declaration (bvs)
        -- have the same kind as where they were bound
        let kindCheckBV v =
              case (find (== v) bs) of
                Nothing -> internalError ("tiStmts': find should not fail")
                Just u -> if (kind u == kind v)
                          then return ()
                          else errBoundTyVarKindMismatch i v u
        mapM_ kindCheckBV bvs
        -- check that there are no free vars in ty
        unless (null fvs) $
            let TyVar v _ _ : _ = fvs
            in  err (getPosition v,  EUnboundTyVar (pfpString v))
        tiStmtBind chke mon mt as td i maybeName pprops e ss ty
tiStmts' chke mon mt as td (CSBindT p name pprops qt e : ss) = do
        nid <- newVar (getPosition p) "tiStmts1"
        tiStmts' chke mon mt as td (CSBindT (CPVar nid) name pprops qt e : CSletrec [CLMatch p (CVar nid)] : ss)
tiStmts' chke mon mt as td (CSBind (CPVar i) maybeName pprops e : ss) = do
        ty <- newTVar "tiStmts' CSBind" KStar e                -- XXX
        tiStmtBind chke mon mt as td i maybeName pprops e ss ty
tiStmts' chke mon mt as td (CSBind p name pprops e : ss) = do
        nid <- newVar (getPosition p) "tiStmts2"
        tiStmts' chke mon mt as td (CSBind (CPVar nid) name pprops e : CSletrec [CLMatch p (CVar nid)] : ss)
tiStmts' chke mon mt as td (CSletrec ds : ss) = do
        (ps, as', ds') <- tiDefls as ds
        (qs, ss')      <- tiStmts' chke mon mt (as' ++ as) td ss
        return (ps ++ qs, Cletrec ds' ss')
tiStmts' chke mon mt type_env expected_type (CSletseq defs : rest_stmts) = do
        defs_without_patterns <- mapM expCLMatch defs >>= return . concat
        (provisos_from_defs, type_env_from_defs, rewritten_defs)
            <- tiSeq tiLetseqDef type_env defs_without_patterns
        (provisos_from_stmts, rewritten_stmts)
            <- tiStmts' chke mon mt (type_env_from_defs ++ type_env)
                        expected_type rest_stmts
        return (provisos_from_defs ++ provisos_from_stmts,
                Cletseq rewritten_defs rewritten_stmts)
tiStmts' _ _ _ _ _ stmt = internalError ("TCheck.tiStmts': " ++ show stmt)

tiStmtsExpr :: TiStmts -> Type -> Maybe Type -> [Assump] -> Type -> Type ->
               Maybe CExpr -> CExpr -> [CStmt] -> TI ([VPred], CExpr)
tiStmtsExpr chke mon mt as td te name e ss = do
        (ps, e') <- tiExpr as te (addStateName name e)
        (qs, ss') <- tiStmts' chke mon mt as td ss
        (rs, f) <- tiVar NoRead as (te `fn` td `fn` td) (CVar (idBind_ (getPosition e)))
        return (ps ++ qs ++ rs, cApply 4 f [e', ss'])

tiStmtBind :: TiStmts -> Type -> Maybe Type -> [Assump] -> Type -> Id -> Maybe CExpr -> [(Position, PProp)] -> CExpr -> [CStmt] -> Type -> TI ([VPred], CExpr)
tiStmtBind chke mon mt as td i maybeName pprops e ss ty = do
        -- traceM ("mon: " ++ ppReadable mon)
        let te = TAp mon ty
            as' = (i :>: toScheme ty) : as
        -- inject state-naming primitive (if name is available)
        -- i.e. we are on a module monad
        let e0 = case pprops of
                   [] -> e
                   pps -> let -- take the first good position
                              pos = getPosition (map fst pprops)
                              ppropExpr = Cattributes pprops
                          in  cApply 19 (CVar (idSetStateAttribAt pos)) [ppropExpr, e]
        let e1 = case maybeName of
                   Nothing       -> e0
                   Just nameExpr ->  let pos = getPosition nameExpr
                                         hide = hasHide pprops
                                         hideAll = hasHideAll pprops
                                         nameExpr'  = if (hide || hideAll) then (applyToCExprIds setHideId nameExpr) else nameExpr
                                         nameExpr'' = if (hideAll) then (applyToCExprIds setHideAllId nameExpr') else nameExpr'
                                     in (cApply 18 (CVar (idSetStateNameAt pos)) [nameExpr'', e0])
        (ps, e') <- tiExpr as te e1
        (qs, ss') <- tiStmts' chke mon mt as' td ss
        let tl = ty `fn` td
        -- traceM ("tl: " ++ ppReadable tl)
        (rs, f) <- tiVar NoRead as (te `fn` tl `fn` td) (CVar (idBind (getPosition e)))
        --posCheck "E" i
        il <- newVar (getPosition i) "tiStmtBind1"
        -- traceM ("tl': " ++ ppReadable tl')
        let ee = Cletseq [CLValueSign (CDefT il [] (CQType [] tl) [CClause [CPVar i] [] ss']) []] (CVar il)
        return (ps ++ qs ++ rs, cApply 6 f [e', ee])

hasHide :: [(Position, PProp)] -> Bool
hasHide ((_, PPinst_hide):_) = True
hasHide (_:rest)             = hasHide rest
hasHide []                   = False

hasHideAll :: [(Position, PProp)] -> Bool
hasHideAll ((_, PPinst_hide_all):_) = True
hasHideAll (_:rest)             = hasHideAll rest
hasHideAll []                   = False

-----------------------------------------------------------------------------

tiRule :: [Assump] -> CRule -> TI ([VPred], CRule)
tiRule as cr = tiRecoveringFromError (tiRule' as cr)
               (return ([], cr))

tiRule' :: [Assump] -> CRule -> TI ([VPred], CRule)
tiRule' as cr@(CRule rps mi quals0 e) = do
    --trace ("TC rule " ++ ppReadable mi) $ return ()
    (ps, mi') <- case mi of Nothing -> return ([], Nothing); Just i -> do (ps, e) <- tiExpr as tString i; return (ps, Just e)

    qualss <- mapM rmQualLit quals0
    let quals = concat qualss
    (qs, as', quals') <- tiQuals as [] [] quals
    (rs, e') <- tiExpr as' tPrimAction (cVApply (setIdPosition (getPosition e) idToPrimAction) [e])

    return (ps ++ qs ++ rs, CRule rps mi' quals' e')

tiRule' as cr@(CRuleNest rps mi quals0 rs) = do
    --trace ("TC rule nest " ++ ppReadable mi) $ return ()
    (ps, mi') <- case mi of Nothing -> return ([], Nothing); Just i -> do (ps, e) <- tiExpr as tString i; return (ps, Just e)

    qualss <- mapM rmQualLit quals0
    let quals = concat qualss
    (qs, as', quals') <- tiQuals as [] [] quals

    psrs <- mapM (tiRule as') rs
    let (pss, rs') = unzip psrs

    return (ps ++ qs ++ concat pss, CRuleNest rps mi' quals' rs')

-----------------------------------------------------------------------------

-- XXX use less tyvars
tiSelect :: ImplReadTag -> [Assump] -> Type -> CExpr -> Id -> (Type -> Type) -> TI ([VPred], CExpr)
tiSelect readTag as td e i f = do
    -- For tracing:
    -- let exp = CSelect e i

    te        <- newTVar "tiSelect" KStar i
    let tf    =  te `fn` td
    let recReadTag = ImplRead (Just i)
    (ps, e')  <- case e of
                   -- Typechecking on a desugarable expression
                   -- Avoid an infinite loop! by passing "i" to
                   -- in recReadTag so it can decide whether to add "_read"
                   -- to register objects.  If the current selection is
                   -- already "_read" then it should not be added again.
                   -- Similarly, don't add "_read" if we're trying to
                   -- call "_write" or any other method on the reg ifc.
                   CVar _ ->
                     tiVar recReadTag as te e
                   CSub pos e1 e2 -> tiSub recReadTag as te pos e1 e2
                   CSelect e_in i_in -> tiSelect recReadTag as te e_in i_in id
                   _ ->
                     tiExpr as te e

    --do s <- getSubst; trace ("sel1 " ++ ppReadable ((exp, apSub s td), (e, apSub s te), (i, apSub s tf))) $ return ()
    (i' :>: sc, ti, n)  <- findFields (f te) i
    (qs :=> t, ts)  <- freshInstT "F" i sc tf
    -- do s <- getSubst; trace ("sel2 " ++ ppReadable (exp, apSub s t, apSub s tf)) $ return ()
    case t of
      TAp (TAp (TCon arr) te0) td0 | isTConArrow arr -> do
           eq_ps <- unify e te te0
           qs'             <- concatMapM (mkVPred (getPosition e)) qs
           let (tts, fts)  = splitAt n ts
           let base_expr = return (td0, eq_ps++ps++qs', iAPs (CApply (cTApply (CSelectT ti i') tts) [e']) fts qs')
           tryReadDesugar base_expr readTag as td (CSelect e i)
      _ -> internalError ("tiSelect non-function field type: " ++ ppReadable (te, i, t))

-----------------------------------------------------------------------------

{-
tiField :: Id -> [Id] -> CheckT (Id, CExpr)
tiField si fs as rt (i, e) =
    if i `notElem` fs then
        err (getPosition i, ENotField (pfpString si) (pfpString i))
    else
        tiField1 as rt (i, e)
-}

tiField1 :: CheckT (Id, CExpr)
tiField1 as rt (f, e) = do
    -- traceM("tiField1 enter")
    (f' :>: sc, _, n) <- findFields rt f
    (qs :=> ft0, xts) <- freshInstT "G" f sc rt
    -- Fields might be defined using type constructors (like SizeOf),
    -- so replace them with vars and return the preds that determine the vars
    -- XXX disable expanding of type synonyms until failures with TLM
    -- XXX (type synonyms which drop parameters) is resolved
    -- XXX (tcon_ps, ft) <- expPrimTCons (expandSyn ft0)
    (tcon_ps, ft) <- expPrimTCons ft0
    -- Unify the field type and the context expected return type,
    -- possibly returning preds which express type equality
    (t,eq_ps) <- unifyFnTo f e ft rt
    s                <- getSubst
    --posCheck "F" f
    i'               <- newVar (getIdPosition f) "tiField1"
    -- trace ("tiField1 " ++ ppReadable (f, i')) $ return ()
    let fvs = map (\ (TVar v) -> v) (drop n xts)
        TAp _ ft' = ft
        fsc = quantify fvs (apSub s (qs :=> ft'))
        -- if "e" is just a wrapper for a tiExpl anyway, call tiExpl on
        -- the wrapped def (see comments for tiExpr on Cinterface)
        (alts, me) =
            case (e) of
                Cletseq [CLValue i1 clauses quals] (CVar i2) | (i1 == i2)
                  -> (clauses, quals)
                _ -> ([CClause [] [] e], [])
        as' = (i' :>: fsc) : as
    -- trace ("tiField1: " ++ ppReadable (apSub s rt, i', e, fsc)) $ return ()
    (ps, d')         <- tiExpl' as' (i', fsc, alts, me)
    let e' = case d' of
                CLValueSign (CDefT _ [] _ [CClause [] [] e]) [] -> e
                _ -> Cletseq [d'] (CVar i')

    -- A struct construction should not take on the contexts of its fields
    -- if the context is already part of the type declaration for the struct.
    -- The context should only appear when the field value is used.  So,
    -- don't add "qs" to the contexts introduced by the field:
    --   qs'              <- mapM (mkVPred (getPosition f)) qs
    --   return (ps ++ qs', (f', e'))

    --traces ("tiField1 " ++ ppReadable ((i, ft), (e'), rt, fsc)) $ return ()
    return (tcon_ps ++ eq_ps ++ps, (f', e'))

-----------------------------------------------------------------------------

{-
tiClauses :: CheckT [CClause]
tiClauses as td alts@(cl@(CClause ps _ e) : ralts) = do
    ts <- mapM (\ p -> newTVar KStar p) ps
    t  <- newTVar KStar e
    unify cl (foldr fn t ts) td

    let np = length ps
    case [ c | c@(CClause ps _ _) <- ralts, length ps /= np ] of
        c : _ -> err (getPosition c, EWrongArity)
        [] -> return ()
    pstcs <- mapM (tiClause as ts t) alts
    let (pss, cs) = unzip pstcs
    return (concat pss, cs)

--tiClause :: CheckT CClause
tiClause as ts t cl@(CClause pats quals e) = do
    (ps, as', pats', quals') <- tiPatsQuals as ts pats quals
    (qs, e')           <- tiExpr as' t e
    return (ps++qs, CClause pats' quals' e')
-}

-- tiClauses should always be called with at least one clause
-- otherwise generate an error at the call site (because it has the position for the error message)
tiClauses :: CheckT [CClause]
tiClauses as td alts@(CClause ps _ _ : ralts) = do
--    trace (ppReadable (alts, td)) $ return ()
    let np = length ps
    case [ c | c@(CClause ps _ _) <- ralts, length ps /= np ] of
        c : _ -> err (getPosition c, EWrongArity)
        [] -> return ()
    pstcs <- mapM (tiClause as td) alts
    let (pss, cs) = unzip pstcs
    --trace ("tiClauses " ++ ppReadable (zip pss alts)) $return ()
    return (concat pss, cs)

tiClauses as td [] = internalError("tiClauses: no clauses\n")

-- XXX use less tyvars
tiClause :: CheckT CClause
tiClause as td cl@(CClause pats quals e) = do
    --trace ("tiClause: " ++ ppReadable (td, cl)) $ return ()
    ts                 <- mapM (\ p -> newTVar "tiClause ts" KStar p) pats
    t                  <- newTVar "tiClause t" KStar e
    --trace ("tiClause " ++ ppReadable (e, td, t)) $ return ()
    eq_ps <- unify cl (foldr fn t ts) td
    (ps, as', pats', quals') <- tiPatsQuals as ts pats quals
    --s <- getSubst; trace (ppReadable (td,foldr fn t ts,s)) $ return ()
    (qs, e')           <- tiExpr as' t e
    --trace ("tiClause " ++ ppReadable (e', td)) $ return ()
    --s <- getSubst; trace (ppReadable s) $ return ()
    return (eq_ps++ps++qs, CClause pats' quals' e')

tiPatsQuals :: [Assump] -> [Type] -> [CPat] -> [CQual] -> TI ([VPred], [Assump], [CPat], [CQual])
tiPatsQuals as ts pats0 quals0 = do
    pqs                <- mapM rmPatLit pats0
    let (pats, pqualss) = unzip pqs
    qualss             <- mapM rmQualLit quals0
    let quals = concat pqualss ++ concat qualss
    (ps, as', pats')   <- tiPats ts pats
    (qs, as'', quals') <- tiQuals (as' ++ as) [] [] quals
    return (ps++qs, as'', pats', quals')

tiQuals :: [Assump] -> [VPred] -> [CQual] -> [CQual] -> TI ([VPred], [Assump], [CQual])
tiQuals as ps r [] = return (ps, as, reverse r)
tiQuals as ps r (q:quals) = do
    (rs, as',q') <- tiQual as q
    tiQuals (as' ++ as) (rs++ps) (q':r) quals

tiQual :: [Assump] -> CQual -> TI ([VPred], [Assump], CQual)
tiQual as (CQGen _ p e) = do
    t             <- newTVar "tiQual" KStar p
    (qs, e')      <- tiExpr as t e
    (ps, as', p') <- tiPat t p
    return (ps++qs, as', CQGen t p' e')
tiQual as (CQFilter e) = do
    (ps, e') <- tiExpr as tBool e
    return (ps, [], CQFilter e')

-----------------------------------------------------------------------------

type Expl = (Id, CQType, [CClause], [CQual])

tiExpl :: [Assump] -> Expl -> TI ([VPred], CDefl)
tiExpl as expl@(i, cqt, alts, me) =
    tiRecoveringFromError
      (tiExpl_1 as expl)
      (return ([],
               (CLValueSign (CDefT
                             i
                             (S.toList(getFQTyVarsT cqt))
                             cqt
                             alts)
                me)))


tiExpl_1 :: [Assump] -> Expl -> TI ([VPred], CDefl)
tiExpl_1 as (i, cqt, alts, me) = do
{-
    --trace ("tiExpl " ++ ppReadable i) $ return ()
    sc           <- mkScheme cqt
    tiExpl'' as i sc alts
-}

    -- Take the CSyntax type declaration and convert it into the
    -- internal data structure for a qualified type.  This does
    -- some kind checking, etc.
    qt@(qs :=> t) <- mkQualType cqt

    -- We're going to generalize this type over the type variables,
    -- so figure out which ones are bound.
    bs           <- getBoundTVs

    -- Of the type variables in the explicit declaration, separate the
    -- free type variables (vs) from those bound by the context (bvs)
    let (bvs, vs) = partition (\x -> elem x bs) (tv qt)

    -- Check that the variables bound in this declaration (bvs)
    -- have the same kind as where they were bound
    let kindCheckBV v =
            case (find (== v) bs) of
                Nothing -> internalError ("tiExpl: find should not fail")
                Just u -> if (kind u == kind v)
                          then return ()
                          else errBoundTyVarKindMismatch i v u
    mapM_ kindCheckBV bvs

    -- Generalize the qualified type to form a type scheme
    let sc       = quantify vs qt

    -- If there any explicit predicates with unsolvable variables,
    -- report an error
    -- XXX do we need to apply the subst?
    --s <- getSubst
    --let fvs = tv (apSub s as) `union` bs
    let fvs = tv as `union` bs
    checkForAmbiguousPreds i fvs qt

{-
    -- Make an instance "qt" and get back the names ("ts") of the type
    -- vars which were introduced in qt in place of the anonymous generics
    ii@(qt, ts)  <- freshInst "H" i sc

    -- Make a substitution from the "vs" of the original type decl
    -- to the "ts" as they are now named, and apply it to the definition
    -- (the clauses and condition)
    let s        = mkSubst (zip vs ts)
        alts'    = apSub s alts
        me'      = apSub s me

    -- Push the newly bound variables (the "ts") onto the bound var stack
    addBoundTVs (map (\ (TVar v) -> v) ts)

    -- Proceed to the next step
    --traceM ("tiExpl " ++ ppReadable (i, s, cqt, alts, alts'))
    tiExpl'' as i sc alts' me' ii
-}

    -- Convert "qs" into local instances
    eqs <- mapM (mkEPred . removePredPositions) qs

    -- Push the variables bound at this level onto the bound var stack
    addBoundTVs vs
    addExplPreds eqs

    -- Proceed to the next step
    tiExpl'' as i sc alts me (qt, map TVar vs)


-- This appears to be the entry point for situations where the type scheme
-- was worked out by the compiler, and does not need to be created from the
-- user-specified type declaration.  For example, once tiImpl has determined
-- the type.  Another caller is tiField, which has also done its own
-- quantifying.  This situation also does not have bound type variables.
tiExpl' :: [Assump] -> (Id, Scheme, [CClause], [CQual]) -> TI ([VPred], CDefl)
tiExpl' as (i, sc, alts, me) = do

    bvs <- getBoundTVs  -- vars bound outside

    ii@(qt@(qs :=> _), inst_types) <- freshInst "I" i sc -- create a copy of the type scheme

    eqs <- mapM (mkEPred . removePredPositions) qs

    -- the instantiated scheme creates bound type variables
    addBoundTVs (tv inst_types)
    addExplPreds eqs

    tiExpl'' as i sc alts me ii

-- tiExpl'' was added (by Lennart) as a front-end to tiExpl'''
-- to trim the substitution.  It takes advantage of the fact that
-- type variables are created in increasing numeric order.  It records
-- the current highest number, and after type-checking, it knows that it
-- can throw away all variables created during checking.  So it trims the
-- substitution back to the recorded point.
tiExpl'' :: [Assump] -> Id -> Scheme -> [CClause] -> [CQual] ->
            (Qual Type, [Type]) -> TI ([VPred], CDefl)
tiExpl'' as0 i sc alts me oqtvts = do
    -- Create a new variable to mark the start of the newly created
    (trim_point, _) <- newTVarId "tiExpl''" KStar i
    -- Typecheck
    r@(ps, d) <- tiExpl''' as0 i sc alts me oqtvts
    -- Get the substitution
    s <- getSubst

    --when (length (getSubstDomain s) > 100) $
    --    traceM (show (length (getSubstDomain s)) ++ "\n" ++ ppReadable s)

    -- Trim the substitution back to the recorded point
    updSubst (trimSubst trim_point)

    --s' <- getSubst
    --traceM (show (i, sizeSubst s, sizeSubst s'))

    let domain = S.fromList (getSubstDomain s)
    let fix_vars_rs = filter (flip S.member domain) (tv ps)
    when (doETrace && (not . null $ fix_vars_rs)) $
      traceM ("tiExpl'' fixup ps: " ++ ppReadable (fix_vars_rs, s, ps, apSub s ps))
    let fix_vars_d = filter (flip S.member domain) (tv d)
    when (doETrace && (not . null $ fix_vars_d)) $
      traceM ("tiExpl'' fixup d: " ++ ppReadable (fix_vars_d, s, d, apSub s d))

    -- Since the result "r" may contain some of the new (trimmed) variables
    -- which were found to be concrete types, we must apply the untrimmed
    -- substitution to remove any mention of the trimmed variables
    return r

--
-- as        the (local) environment
-- i        name of definition
-- sc        type signature of definition
-- alts        clauses of definition
-- me   the implicit condition patterns of an interface definition
--      (an empty list for non-interfaces)
-- oqt        instantiated scheme
-- vts        variables used to instantiate sc to oqt
tiExpl''' :: [Assump] -> Id -> Scheme -> [CClause] -> [CQual] ->
             (Qual Type, [Type]) -> TI ([VPred], CDefl)
tiExpl''' as0 i sc alts me (oqt@(oqs :=> ot), vts) = do

    etrace ("tiExpl: " ++ ppReadable (i, getIdPosition i, length as0, sc)) $
        return ()

    -- Typecheck the implicit condition (only for interfaces)
    -- mps = introduced predicates (VPred)
    -- as  = as0 plus new assumptions introduced
    -- me' = the conditions after checking
    (mps, as, me') <- tiQuals as0 [] [] me

    -- Typecheck the definition clauses
    -- ps    = introduced predicates (VPred)
    -- alts' = the clauses after checking
    (ps0, alts') <- tiClauses as ot alts

    satTraceM ("tiExpl " ++ ppReadable i ++ " ps0: " ++ ppReadable ps0)

    -- type functions like SizeOf could have crept into the predicates
    -- via unification, so we expand them out so that they can be satisfied
    ps <- concatMapM (expTConPred . expandSynVPred) ps0

    satTraceM ("tiExpl " ++ ppReadable i ++ " ps: " ++ ppReadable ps)

    -- ---------------

    -- locally bound tyvars and instances
    vs_bound_here <- getTopBoundTVs
    eqs0 <- getTopExplPreds

    -- drop local tyvars (but not instances)
    popBoundTVs

    bvs            <- getBoundTVs       -- and grab those bound outside

    s0 <- getSubst                      -- grab what we know now

    -- but put the tyvars bound here back on the stack, so that later
    -- calls to "satisfy" are aware of all the bound vars
    addBoundTVs vs_bound_here

    let eqs = apSub s0 eqs0

    ---- Begin: Section which Lennart marked with XXXX

    -- Try to solve as many of the constraints "ps" as possible,
    -- from the given constraints "eqs"
    -- ps' = the unsolved constraints
    -- bs2 = new bindings (new dictionaries defined from given dictionaries)
    (ps', bs2)     <- satisfy eqs (apSub s0 ps)

    satTraceM ("tiExpl " ++ ppReadable i ++ " ps'(satisfy): " ++ ppReadable ps')

    s              <- getSubst                        -- get full subst

    let
        -- Compute the fixed variables
        -- These are the variables in the assumptions and the bound vars
        fvs0       =  tv (apSub s as) `union` bvs
        -- Extend the fixed variables to include any variables which
        -- are fixed due to functional dependencies
        fvs        =  closeFD ps' fvs0 \\ vs_bound_here

        -- Apply the subst to the qualified type
        -- qt'@(qs' :=> t') = apSub s oqt
        qt'        = apSub s oqt

        -- Separate the unsolved predicates into two groups:
        -- ds2 = preds, all of whose tyvars are all fixed (we will
        --       defer them to the enclosing bindings)
        -- rs1 = preds which contain tyvars general/bound at this level
        -- "d" for deferred and "r" for retained
        (ds2, rs1) =  splitF fvs ps'                -- non-local, local constraints

        -- All the tyvars ("avs") = the vars of qt' ("lvs") and
        -- the fixed vars ("fvs")
        lvs        =  tv qt'                        -- local tyvars
        avs        =  lvs `union` fvs                -- all tyvars

    ----

    -- The "dvs" argument to "satisfyFV"
    let dvs = avs

    -- Try again to solve more constraints,
    -- this time, solving only for "rs1", the preds which contain
    -- tyvars bound at this level, and we don't generate TAdd, TLog, etc
    -- for the tyvars "dvs".
    -- ps' = the remaining unsolved constraints
    -- bs3 = new bindings for the solved constraints
    (ps', bs3)     <- satisfyFV dvs eqs (apSub s rs1)

    satTraceM ("tiExpl " ++ ppReadable i ++ " ps'(satisfyFV) " ++ ppReadable ps')

    s              <- getSubst                        -- get full subst

    let
        -- Compute the fixed variables
        -- These are the variables in the assumptions and the bound vars
        fvs0       =  tv (apSub s as) `union` bvs
        -- Extend the fixed variables to include any variables which
        -- are fixed due to functional dependencies
        fvs        =  closeFD ps' fvs0 \\ vs_bound_here

        -- Apply the subst to the qualified type
        qt'@(qs' :=> t') = apSub s oqt

        -- Separate the unsolved predicates into two groups:
        -- ds3 = preds, all of whose tyvars are all fixed (we will
        --       defer them to the enclosing bindings)
        -- rs2 = preds which contain tyvars general/bound at this level
        -- "d" for deferred and "r" for retained
        (ds3, rs2) =  splitF fvs ps'                -- non-local, local constraints

        -- All the tyvars ("avs") = the vars of qt' ("lvs") and
        -- the fixed vars ("fvs")
        lvs        =  tv qt'                        -- local tyvars
        avs        =  lvs `union` fvs                -- all tyvars

    let
        -- Bindings for solved constraints have been generated twice,
        -- consolidate them under one name
        bs23 = bs2 ++ bs3

        -- Constraints with only fixed variables have been removed twice,
        -- consolidate them under one name.  "d" for deferred
        --
        -- The constraints "ds" are those with variables which are
        -- all fixed (in "fvs").  Non-local contexts which have tyvars
        -- from an enclosing binding will be deferred, to be solved by
        -- the enclosing binding.  Contexts which have no vars at all
        -- may also appear in this list and are handled below as "uds".
        ds  = ds2 ++ ds3

    ---- End: Section which Lennart marked with XXXX

    ---- Begin: Added for defaulting

    -- Try to solve some remaining constraints by defaulting.
    -- rs  = remaining unsolved constraints
    -- bs4 = bindings for any constraints solved by defaulting
    (rs, bs4, amb_vars)
        <- if (null rs2)  -- whether there are any unresolved contexts
           then return (rs2,[],[])  -- don't do work if not necessary
           else defaultClasses avs eqs rs2

    -- defaulting extends the substitution
    s <- getSubst

    -- Consolidate the bindings under one final name
    let bs1 = bs23 ++ bs4

    -- The final remaining constraints are now named "rs"
    --trace ("tiExpl''': rs, rs2: " ++ ppReadable (rs,rs2)) $ return ()

    ---- End: Added for defaulting

    let
        -- Contexts which have no vars at all may also appear in the
        -- list "ds".  These contexts were not solved, which means a
        -- context reduction failure (no instance was found for those
        -- types).  Report an error if this list "uds" is not empty.
        uds        =  filter (null . tv) ds        -- no tyvars and not solvable

        -- Ambiguous predicates
        -- An expression is ill-formed if its most general type ps => t
        -- includes an ambiguous variable in "ps"; that is, a generic
        -- variable (one not in the assumptions) which does not appear in
        -- the base type "t".  The classic example is "show (read x)".
        -- The intermediate type is ambiguous.
        (rs_amb, rs_unamb) = partition (any (`elem` amb_vars) . tv) rs

    -- Apply the substitution to the code fragments
    let alts''     =  apSub s alts'             -- new alternatives
        abs        =  apSub s bs1               -- new dict bindings
        me''       =  apSub s me'               -- update guards

    -- Determine the generic variables and produce the inferred type scheme
    let
        -- The generic vars are the local vars ("tv t") which are not fixed
        gs = lvs \\ fvs
        -- The inferred type scheme quantifies over "gs"
        -- (note that qt' is just oqt with the subst applied)
        sc' = quantify gs qt'
        -- The expected type scheme (subst with the new info, first)
        xsc = apSub s sc

    rtrace ("tiExpl:\n" ++ (pretty 120 100 $ let d = PDReadable in
        (text "i =" <+> pPrint d 0 i) $+$
        (text "|as0| =" <+> pPrint d 0 (length as0)) $+$
        (text "as0 =" <+> pPrint d 0 as0) $+$
        (text "|as| =" <+> pPrint d 0 (length as)) $+$
        (text "as =" <+> pPrint d 0 as) $+$
        (text "alts =" <+> pPrint d 0 alts) $+$
        (text "(oqt, vts) =" <+> pPrint d 0 (oqt, vts)) $+$

        (text "s0 =" <+> pPrint d 0 s0) $+$
        (text "eqs0 = " <+> pPrint d 0 eqs0) $+$
        (text "eqs =" <+> pPrint d 0 eqs) $+$
        (text "dvs =" <+> pPrint d 0 dvs) $+$
        (text "ps,s.ps,ps' =" <+> pPrint d 0 (ps, apSub s0 ps, ps')) $+$
        (text "bs1 =" <+> pPrint d 0 bs1) $+$
        (text "alts' =" <+> pPrint d 0 alts') $+$

        (text "bvs =" <+> pPrint d 0 bvs) $+$
        (text "fvs0 =" <+> pPrint d 0 fvs0) $+$
        (text "fvs =" <+> pPrint d 0 fvs) $+$
        (text "qt' =" <+> pPrint d 0 qt') $+$
        (text "s =" <+> pPrint d 0 s) $+$
        (text "lvs =" <+> pPrint d 0 lvs) $+$
        (text "avs =" <+> pPrint d 0 avs) $+$

        (text "uds =" <+> pPrint d 0 uds) $+$
        (text "rs_amb =" <+> pPrint d 0 rs_amb) $+$

        (text "alts'' =" <+> pPrint d 0 alts'') $+$

        (text "ds,rs =" <+> pPrint d 0 (ds, rs)) $+$

        (text "gs =" <+> pPrint d 0 gs) $+$

        (text "abs =" <+> pPrint d 0 abs) $+$
        (text "sc,xsc,sc' =" <+> pPrint d 0 (sc, xsc, sc'))
        )) $ return ()

    -- Give better names to some variables
    let
        -- "n" stands for "new"?
        -- Here: nqt@(nqs :=> nt) = apSub s oqt
        nqt = qt'
        nqs = qs'
        nt = t'
        -- The generic variables
        ngs = gs
        -- The given type scheme
        nsc = sc'

        -- The dictionary names of the predicates
        vs = map (\ (EPred (CVar i) _) -> i) eqs

    -- The predicates which will be returned, to be handled by the
    -- enclosing binding.  It includes the deferred predicates "ds"
    -- and the predicates for the interface method ready expression
    -- "mps" (if this is in an interface).
    let rds = mps ++ ds

    -- Does the expected type scheme match the given scheme?
    if xsc /= nsc then
        -- Report an error
        -- Use niceTypes to name the variables 'a', 'b', 'c', ...
        -- Use instSC2 to instantiate the generics with fresh tyvars not
        -- found in either type
        let (xsc', nsc') = niceTypes (instSC2 (xsc, nsc))
        in  err (getPosition i, ETooGeneral (pfpString xsc') (pfpString nsc'))
     else
     -- Are any of the retained predicates unsolved?
     if not (null rs_unamb) then
        -- Report errors for the contexts
        -- (later calls to "niceTypes" will replace generated tyvar names)
        let rs' = map toPredWithPositions rs
            ds' = map toPred ds
        in  handleWeakContext (getPosition i) t' qs' ds' rs'
     else
     -- any ambiguous variables?
     if not (null rs_amb) then
        handleAmbiguousContext (getPosition i) amb_vars rs_amb
     else
     -- Were any contexts without variables left unsatisfied?
     if not (null uds) then
        -- Report reduction errors
        handleContextReduction (getPosition i) uds
     else
        -- No ambiguous variables, so...
        -- Produce the return values (deferred preds, CDefl)
        do
           --traceM("tiExpl " ++ ppReadable (i,eqs,ps))

           -- remove the bound tyvars and instances for this level
           popBoundTVs
           popExplPreds

           -- XXX More comments and review needed beyond this point
           let
                -- inline simple bindings
                (vmap, rem_abs) = simplifyDictBindings abs
                -- we're only substituting variables, not constructors
                s :: CSEnv
                s = (M.empty, M.empty, vmap, M.empty)
                alts''' = cSubstN s alts''
                me''' = cSubstQualsN s me''
            in --traces (ppReadable s) $
               if null nqs && null rem_abs then
                   -- simplify special case (no context, no new bindings)
                   let ldef = CLValueSign
                                 (CDefT i ngs (CQType [] nt) alts''') me'''
                   in  return (rds, ldef)
               else do
                  --posCheck "G" i
                  ii <- newVar (getPosition i) "tiExpl"
                  let ldef = CLValueSign
                                 (CDefT ii [] (CQType [] nt) alts''') []
                      -- produce let in topologically sorted order
                      -- (since ldef uses bindings, but not vice-versa)
                      body = CClause (map CPVar vs) []
                                 (Cletrec (rem_abs ++ [ldef]) (CVar ii))
                  --traceM ("tiExpl''' " ++ ppReadable (i, ii, abs))
                  return (rds, CLValueSign
                                 (CDefT i ngs (CQType [] (qualToType nqt))
                                     [body]) me''')


-- The way we typecheck, sub-expr checking doesn't know what bindings
-- exist, so a fresh dict binding is made for each predicate even if a
-- dict already exists for it.  This leads to "silly bindings" (as
-- Lennart said in rev 2901) like this:
--    _tcdict1002 = _tcdict1001
-- This leads to problems for IConv when it substs these away.
--
-- In rev 2901, Lennart added an optimization, but was unsure of the
-- benefit.  In rev 2904, he commented it out, due to a bug.  In his
-- code, a simple binding included functions.  We don't include those,
-- and thus don't have to deal with recursive bindings.
simplifyDictBindings :: [CDefl] -> (M.Map Id CExpr, [CDefl])
simplifyDictBindings all_bs =
    let
        (simple_bs, rem_bs0) = partition simpleD all_bs

        simpleD (CLValueSign (CDefT _ [] (CQType [] _)
                                  [CClause [] [] e]) []) = simpleE e
        simpleD _ = False

        simpleE (CTApply e _) = simpleE e
        simpleE (CVar _) = True
        -- Lennart included this
        --simpleE (CApply f es) = all simpleE (f:es)
        simpleE _ = False

        -- sort the simple bindings in usage order
        -- (so that we can apply the subst once)
        defpairs =
            [ (i, e)
              | (CLValueSign (CDefT i _ _ [CClause _ _ e]) _) <- simple_bs ]
        defmap = M.fromList defpairs
        isdef i = i `M.member` defmap
        usegraph = [ (i, is) | (i, e) <- defpairs,
                               let is0 = fvSetToFreeVars (getFVE e),
                               let is = filter isdef is0 ]
        ordered_def_ids =
            case (GW.tSort usegraph) of
              Right is -> is
              Left sccs ->
                  internalError ("ordered_def_ids: " ++ ppReadable sccs)

        mkEnv vm = (M.empty, M.empty, vm, M.empty)

        vmap = let fn accum_map i =
                      let e0 = fromJustOrErr "vmap" (M.lookup i defmap)
                      in  M.insert i (cSubst (mkEnv accum_map) e0) accum_map
               in  foldl fn M.empty ordered_def_ids
    in
       (vmap, cSubstN (mkEnv vmap) rem_bs0)


{-
-- instantiate a type scheme on temporary type variables
instSC :: Scheme -> (Qual Type)
instSC (Forall ks t) = inst vars t
  where bad_tmptyvar_ids = map getTyVarId (tv t)
        tmptyvar_ids = [i | i <- tmpTyVarIds, not (i `elem` bad_tmptyvar_ids)]
        vars = zipWith (\ i k -> TVar (TyVar i noTyVarNo k)) tmptyvar_ids ks
-}

-- instantiate two type schemes on temporary type variables
instSC2 :: (Scheme, Scheme) -> (Qual Type, Qual Type)
instSC2 (Forall ks1 t1, Forall ks2 t2) =
    let bad_tmptyvar_ids = map getTyVarId (tv (t1,t2))
        tmptyvar_ids = [i | i <- tmpTyVarIds, not (i `elem` bad_tmptyvar_ids)]
        (tmptvs1, tmptvs2) = splitAt (length ks1) tmptyvar_ids
        vars1 = zipWith (\ i k -> TVar (TyVar i noTyVarNo k)) tmptvs1 ks1
        vars2 = zipWith (\ i k -> TVar (TyVar i noTyVarNo k)) tmptvs2 ks2
    in  (inst vars1 t1, inst vars2 t2)

-----------------------------------------------------------------------------

-- a definition without a type (i.e., with an "implicit" type)
type Impl   = (Id, ([CClause], [CQual]))

-- a function to typecheck a single definition
--   type_env  = current type environment
--   type_var  = the type variable for this def
--   clauses =   the clauses of the definition
--   quals =     the implicit condition patterns
--               (an empty list if the def is not for a method)
tiImpl :: [Assump] -> Type -> (Id, ([CClause], [CQual]))
       -> TI ([VPred], ([CClause], [CQual]))
tiImpl type_env type_var (_, (clauses, quals)) = do
        -- Typecheck the implicit condition (only for interfaces)
        -- pqs = introduced predicates (VPred)
        -- type_env_quals = type_env plus new assumptions from quals
        -- qs' = the conditions after checking
        (provisos_quals, type_env_quals, rewritten_quals)
            <- tiQuals type_env [] [] quals
        -- Typecheck the definition clauses
        -- provisos_clauses = introduced predicates (VPred)
        -- rewritten_clauses = the clauses after checking
        (provisos_clauses, rewritten_clauses)
            <- tiClauses type_env_quals type_var clauses
        -- return the predicates and the new defs
        return (provisos_quals ++ provisos_clauses,
                (rewritten_clauses, rewritten_quals))

-- typecheck a set of possibly interdependent definitions
tiImpls :: Bool -> Infer2 [Impl] [Assump] [CDefl]
tiImpls recursive as [] = return ([], [], [])
tiImpls recursive as ibs = do
    --trace ("IMPLICIT " ++ ppReadable (map fst ibs)) $ return ()

    -- Get the type variables which are bound by a surrounding context
    bvs            <- getBoundTVs

    -- create new type variables for the types of the definitions
    ts <- mapM (newTVar "tiImpls" KStar) ibs

    let
        -- the ids of the definitions
        is    = map fst ibs
        -- create a scheme for each definition
        scs   = map toScheme ts
        -- if the defs are interdependent/recursive:
        -- create an assumption from each scheme (associating id to scheme)
        -- and add them to the environment
        as_initial | recursive = zipWith (:>:) is scs ++ as
                   | otherwise = as

    -- typecheck all the defs
    pscs <- sequence (zipWith (tiImpl as_initial) ts ibs)

    -- pss = all the predicates
    -- altss' = all the new defs (clauses and quals)
    let (pss, altss') = unzip pscs

    s   <- getSubst

    let ps = apSub s (concat pss)
    when (not . null $ ps) $ satTraceM ("tiImpls " ++ ppReadable is ++ " ps: " ++ ppReadable ps)

    -- try to solve as many constraints as possible,
    --   ps' = unsolved predicates
    --   bs  = new bindings (for dictionaries of any predicates solved)

    -- We used to call "satisfy" with an empty list for eqs, but now we try
    -- to reduce predicates more aggressively, so that we generate better
    -- provisos when we re-type-check with tiExpl

    eqsFV <- getExplPreds
    (ps', bs1) <- satisfyFV bvs eqsFV ps

    when (not . null $ ps) $ do
      if (not . null $ ps') then
        satTraceM ("tiImpls " ++ ppReadable is ++ " ps': " ++ ppReadable ps')
       else
        satTraceM ("tiImpls " ++ ppReadable is ++ " satisfied")

    s   <- getSubst

    -- "satisfy" returns the original preds that could not be resolved;
    -- however, some preds may reduce to simpler provisos (which could not
    -- be resolved).  so we do that reduction here.

    let eqs = []
    (ps'', bs2, s_agg) <- reducePredsAggressive Nothing eqs ps'

    when (not . null $ ps') $ do
      if (not . null $ ps'') then
        satTraceM ("tiImpls " ++ ppReadable is ++ " ps'': " ++ ppReadable ps'')
       else
        internalError ("tiImpls aggressively reduced? " ++ ppReadable (ps', ps'', s, s_agg))

    extSubst "tiImpls reducePredsAgg" s_agg

    let
        -- Expand the types with any new information
        ts'     = apSub s ts

        -- Compute the free variables ("fixed" variables?)
        -- These are the variables in the assumptions
        fs      = tv (apSub s as) `union` bvs
        -- XXX we don't close them over functional dependencies, as in tiExpl?

        vss       = map tv ts'
        -- local variables
        lvs       = foldr1 union vss
        --gs      = lvs \\ fs

        -- Separate the unsolved predicates into two groups:
        -- ds = preds, all of whose tyvars are fixed (in fs)
        --      (we will defer them to the enclosing bindings)
        -- rs = preds which contains tyvars general/bound at this level
        -- "d" for deferred and "r" for retained
        (ds,rs) = splitF fs ps''                        -- non-local, local constraints


    -- Begin: find unresolvable variables

    (rs2, bs3, amb_vars)
        <- -- this will be a no-op if there are no ambiguous vars
           defaultClasses (fs `union` lvs) [] rs

    when (not (null amb_vars)) $
        let pos = getPosition (fst (headOrErr "tiImpls: pos" ibs))
        in  handleAmbiguousContext pos amb_vars rs2

    -- update the info we computed above
    s <- getSubst
    let bs_final = apSub s (bs1 ++ bs2 ++ bs3)
        ts_final = apSub s ts'
        fs_final = tv (apSub s as) `union` bvs
        vss_final = map tv ts_final
        lvs_final = foldr1 union vss_final
        rs_final = rs2

    -- End: find unresolvable variables

    -- Apply the substitution to the code fragments
    let altss_final = map (apSub s) altss'          -- new alternatives

    -- Determine the generic variables and produce the inferred type scheme
    let
        -- The generic vars are the local vars (tv of the ts and the rs)
        -- which are not fixed
        gs = (lvs_final `union` tv rs_final) \\ fs_final
        -- The inferred type scheme quantified over "gs"
        scs' =
            map (quantify gs . (map toPredWithPositions rs_final :=>)) ts_final

        -- The final assumptions (associating ids to schemes)
        res_as = zipWith (:>:) is scs'

    rtrace ("tiImpl:\n" ++ (pretty 120 100 $ let d = PDReadable in
        (text "s =" <+> pPrint d 0 s) $+$
        (text "ibs =" <+> pPrint d 0 ibs) $+$
        (text "pss,ps',ps'' =" <+> pPrint d 0 (pss, ps', ps'')) $+$
        (text "fs =" <+> pPrint d 0 fs) $+$
        (text "ds,rs_final =" <+> pPrint d 0 (ds, rs_final)) $+$
        (text "res_as =" <+> pPrint d 0 res_as)
        )) $ return ()

    -- Are there any local constraints?
    -- Either any retained (rs) or any predicates satisfied (bs)
    if (null rs_final) && (null bs_final) then
        -- no local constraints, so use bindings as is
        let
            -- Create an explicitly typed definition for a given i
            -- The generic variables are (tv t \\ fs_final)
            mkExpl (i,_) t (alts, me) =
                CLValueSign (CDefT i (tv t \\ fs_final) (CQType [] t) alts) me
            defs = zipWith3 mkExpl ibs ts_final altss_final
        in
            -- return the deferred predicates, the assumptions for the
            -- ids bound here, and the typed defs
            return (ds, res_as, defs)
     else do
        -- Else, we need to handle the proviso dictionaries and dict bindings.
{-
        -- This used to be done by converting to an explicitly-type let expr
        -- and re-typechecking, but that was inefficient
        --
        let (css, qss) = unzip (map snd ibs)
        -- re-check as explicitly-typed bindings, with the original "as"
        xs <- mapM (tiExpl' as) (zip4 is scs' css qss)
        -- qss = predicates to be propagated (like "ds"?)
        -- eds = the new explicit defs (after checking)
        let (qss, eds) = unzip xs
        return (concat qss, res_as, eds)
-}
        let
            mkExpl i t0 (alts, me) = do
              let
                  -- the "original" type, resulting from typecheck
                  qs0 = map toPredWithPositions rs_final
                  oqt = (qs0 :=> t0)

                  -- the variables in the type
                  vs = tv oqt
                  -- the generic variables in the type
                  -- (in the order they appear in "oqt")
                  gs_used_here = filter (`elem` gs) vs

              -- make new names for the generic variables
              -- XXX TODO: do we need to? or can we just continue to use "gs"?
              let mkFreshVar v = newTVar ("tiImpls fresh") (kind v) v
              vs_bound_here <- mapM mkFreshVar gs_used_here
              -- the same list, but as TyVar
              let vts_bound_here = map (\ (TVar v) -> v) vs_bound_here
              -- a mapping from the old names to the new names
              -- (need to apply this subst to everything -- types and exprs)
              -- (CSubst was extended to support TVar specifically for this)
              let gs_map = zip gs_used_here vs_bound_here

              -- the new type for this let-binding
              let nqt@(_ :=> nt) = apSub (mkSubst gs_map) oqt

              -- the variable names for the dictionary arguments
              let dict_vs = let getVPredId (VPred i _) = i
                            in  map getVPredId rs_final

              let
                  -- inline simple dictionary bindings
                  (vmap, rem_bs_final) = simplifyDictBindings bs_final
                  -- substitute for the simple dict bindings (vmap)
                  -- and for the new generic variable names (gs_map)
                  csenv :: CSEnv
                  csenv = (M.empty, M.empty, vmap, M.fromList gs_map)
                  alts' = cSubstN csenv alts
                  me' = cSubstQualsN csenv me
                  -- the dict bindings can refer to "gs"
                  rem_bs_final' = cSubstN csenv rem_bs_final

              inner_i <- newVar (getPosition i) "tiImpl"
              let ldef = CLValueSign
                             (CDefT inner_i [] (CQType [] nt) alts') []
                  -- produce let in topologically sorted order
                  -- (since ldef uses bindings, but not vice-versa)
                  body = CClause (map CPVar dict_vs) []
                             (Cletrec (rem_bs_final' ++ [ldef]) (CVar inner_i))
              return (CLValueSign
                          (CDefT i vts_bound_here (CQType [] (qualToType nqt))
                               [body]) me')
        defs <- sequence $ zipWith3 mkExpl (map fst ibs) ts_final altss_final
        return (ds, res_as, defs)

-----------------------------------------------------------------------------

-- binding group: some explicitly typed and some implicitly typed definitions
type BindGroup  = ([Expl], [[Impl]])

-- typecheck a binding group, with possibly mutually recursive bindings
tiBindGroup :: Infer2 BindGroup [Assump] [CDefl]
tiBindGroup as (typed_bindings, untyped_bindingss) = do
                -- as': type env containing explicitly-typed bindings
                as' <- mapM (\ (v,t,_,_) -> do sc <- mkSchemeNoBVs t
                                               return (v:>:sc))
                            typed_bindings
                (ps, as'', ds')
                    <- tiSeq (tiImpls True) (as'++as) untyped_bindingss
                xs <- mapM (tiExpl (as''++as'++as)) typed_bindings  --- XXX
                let (qss, ds'') = unzip xs
                return (ps++concat qss, as''++as', ds' ++ ds'')

-- typecheck a list of sequentially dependent elements, such as letseq
-- definitions or independent binding groups from letrec
--   arguments:
--     ti:        the typechecker to use for the typechecking
--     type_env:  initial type environment
--     all_defs:  definitions or binding groups to check sequentially
--   returns:
--     (provisos, type_env, rewritten_defs) where
--       provisos:       provisos required by the definitions
--       type_env:       type environment with all definitions
--       rewritten_defs: original definitions, possibly rewritten
tiSeq :: Infer2 bg [Assump] [d] -> Infer2 [bg] [Assump] [d]
tiSeq ti type_env [] = return ([], [], [])
tiSeq ti type_env all_defs@(def : rest_defs) = do
    (provisos, type_env',  rewritten_defs) <- ti type_env def
    (provisos_rest, type_env'', rewritten_defs_rest)
        <- tiSeq ti (type_env'++type_env) rest_defs
    return (provisos ++ provisos_rest, type_env''++type_env',
            rewritten_defs ++ rewritten_defs_rest)

-- tiLetseqDef: type-check a single non-recursive let definition
--   arguments:
--     type_env: type environment assumptions
--     def:      definition to typecheck (must not be CLMatch)
--   returns:
--     (provisos, type_env, rewritten_defs) where
--       provisos:       provisos required by this definition
--       type_env:       a binding for this definition
--       rewritten_defs: original definition, possibly rewritten
tiLetseqDef :: [Assump] -> CDefl -> TI ([VPred], [Assump], [CDefl])
tiLetseqDef type_env def@(CLValueSign (CDef var_name def_type clauses) quals) =
    do -- check RHS without defining the variable it's assigned to;
       -- fix type variables in the explicit signature while checking RHS
       let explicit_def = (var_name, def_type, clauses, quals)
       (provisos, rewritten_def) <- tiExpl type_env explicit_def
       -- create a type scheme for this definition and return it
       def_type_scheme <- mkSchemeNoBVs def_type
       return (provisos, [var_name :>: def_type_scheme], [rewritten_def])
tiLetseqDef type_env def@(CLValueSign (CDefT _ _ _ _) _) =
  -- CDefT implies that the def has already been type-checked
  -- and so should not need re-typechecking
  internalError ("tiLetSeqDef: CDefT " ++ ppReadable def)
tiLetseqDef type_env def@(CLValue var_name clauses quals) =
    tiImpls False type_env [(var_name, (clauses, quals))]
tiLetseqDef type_env arm@(CLMatch pattern expression) =
    internalError
        ("TCheck.tiLetseqDef: CLMatch should have been desugared:\n" ++
         pfpReadable arm)

-- tiDefls: type-infer a set of letrec definitions
--   first argument:         assumptions about type environment
--   second argument (exp):  definitions to typecheck
-- returns: TI (provisos, type_env', defs') where
--   provisos:  context requirements
--   type_env': type environment, possibly extended with the definitions
--   defs':     definitions, possibly rewritten
tiDefls :: [Assump] -> [CDefl] -> TI ([VPred], [Assump], [CDefl])
tiDefls type_env defs = do
    dss        <- mapM expCLMatch defs -- convert pattern-matches to regular defs
    let ds = concat dss
    let -- impl: untyped (implicitly typed) definitions
        impl = doSCC ds
        -- expl: explicitly typed definitions
        expl = [ (i, t, cs, me) | CLValueSign (CDef i t cs) me <- ds ]
    case filter (not . null) (map chkIRec impl) of -- detect recursion
     all_is@(_:_) : _ ->
         -- XXX we only report one cycle?
         -- Don't report internal names that come from expanding
         -- pattern matches
         let user_is = filter (not . isBadId) all_is
             mkErr :: [Id] -> TI a
             mkErr is = err (getPosition is, ELocalRec (map pfpString is))
         in  case user_is of
               (_ : _) -> mkErr user_is
               _       -> mkErr all_is
     [] -> tiBindGroup type_env (expl, impl)
     _ -> internalError "TCheck.tiDefls"

-- find untyped definitions which refer to themselves
chkIRec :: [Impl] -> [Id]
chkIRec [(i, (cs, me))] =
    if S.member i (snd (getFVDl (CLValue i cs me))) then [i] else []
chkIRec ics = map fst ics

{- Unused:
chkERec d@(CLValueSign (CDef i _ _) _) = S.member i (snd (getFVDl d))
chkERec _ = False
-}

-- extract untyped let-defs and sort them into interdependent groups
doSCC :: [CDefl] -> [[Impl]]
doSCC ds =
        let g = [ (i, S.toList (snd (getFVDl d) `S.intersection` is)) | d@(CLValue i _ _) <- ds ]                -- XXX CLMatch
            is = S.fromList (map fst g)
            iss = scc g
            get i = (i, (headOrErr ("TCheck.doSCC: missing CLValue " ++
                                    pfpString i)
                         ([ (cs, me) | CLValue i' cs me <- ds, i == i'])))
        in  map (map get) iss

-----------------------------------------------------------------------------

-- funny, this sees a system task application
iAPs :: CExpr -> [Type] -> [VPred] -> CExpr
iAPs f ts ps = cApply 7 (cTApply f ts) (map (\ (VPred i _) -> CVar i) ps)

optTrivLet :: CExpr -> CExpr
optTrivLet (Cletseq [CLValueSign (CDefT x [] _ [CClause [] [] e]) []] (CVar x')) | x == x' = e
optTrivLet (Cletrec [CLValueSign (CDefT x [] _ [CClause [] [] e]) []] (CVar x')) | x == x' = e
optTrivLet e = e

ifcFieldIdToTConId :: Id -> SymTab -> CType -> Maybe Id
ifcFieldIdToTConId i r t =
    case leftCon (expandSyn t) of
    Nothing -> Nothing
    Just ti ->
        case findType r ti of
        -- this pattern requires that the type be an interface
        Just (TypeInfo _ _ _ (TIstruct (SInterface {}) is)) ->
            if (unQualId i) `elem` map unQualId is
                then Just ti
                else Nothing
        _ -> Nothing

-- Whether _read/_write desugaring can be applied
-- (it is an interface type and it has _read/_write as a method)
isReadType :: SymTab -> CType -> Maybe Id
isReadType  = ifcFieldIdToTConId (id_read noPosition)
isWriteType :: SymTab -> CType -> Maybe Id
isWriteType = ifcFieldIdToTConId (id_write noPosition)

-- check if an interface has a ._write method
-- or is in PrimWriteable
writeableIfc :: Flags -> SymTab -> CType -> Bool
writeableIfc flags r t
    | Just _ <- isWriteType r t = True
    -- incoherent matches are resolved *after* reducePred
    | Right (Just _) <- fst $ runTI flags False r checkWriteable = True
    | otherwise = False
  where checkWriteable = do
          wCls <- findCls (CTypeclass idPrimWriteable)
          v <- newTVar "writeableIfc" KStar t
          vp <- mkVPredFromPred [] (IsIn wCls [t, v])
          reducePred [] Nothing vp

getIfcFields :: Id -> SymTab -> Maybe [Id]
getIfcFields ti sy =
    case findType sy ti of
    Just (TypeInfo _ _ _ (TIstruct SInterface{} fs)) -> Just fs
    _ -> Nothing

chkSchedInfo :: [Id] -> VSchedInfo -> TI ()
chkSchedInfo field_ids si@(SchedInfo mci rms rbm ccm) = do
    -- traceM ("chkSchedInfo" ++ ppReadable si)
    let field_set = S.fromList field_ids
    -- check methodConflictInfo
    chkMethConf field_set mci
    -- check unsynchronized clock crossing methods
    chkUnsyncMeths field_set ccm
    -- check rulesBetweenMethods and rulesBeforeMethods
    -- XXX these should never come from the user, so it's an internal error?
    -- XXX also, we have no way of checking if the rule names exist
    -- XXX (if we allowed it in import-BVI, the rule name field would need
    -- XXX to be a different type)
    let unknown = [ i | ((i1,i2),rs) <- rms, i <- [i1, i2],
                        not (i `S.member` field_set) ] ++
                  [ i | (i,rs) <- rbm, not (i `S.member` field_set) ]
    case unknown of
        [] -> return ()
        i : _ -> err (getIdPosition i, EUnboundField (pfpString i))

chkMethConf :: S.Set Id -> MethodConflictInfo Id -> TI ()
chkMethConf field_set mci@(MethodConflictInfo cf sb me p sbr c ext) =
    let unknown =
            [ i | iis <- [cf, sb, p, sbr, c],
                  (i1,i2) <- iis, i <- [i1, i2], not (i `S.member` field_set) ] ++
            [ i | is <- me, i <- is, not (i `S.member` field_set) ] ++
            [ i | i <- ext, not (i `S.member` field_set) ]
    in  case unknown of
            [] -> return ()
            i : _ -> err (getIdPosition i, EUnboundField (pfpString i))

chkUnsyncMeths :: S.Set Id -> [Id] -> TI ()
chkUnsyncMeths field_set ms =
    let unknown = [ i | i <- ms, not (i `S.member` field_set) ]
    in  case unknown of
            [] -> return ()
            i : _ -> err (getIdPosition i, EUnboundField (pfpString i))

-----------------------------------------------------------------------------

cLet :: [(Id, CType, CExpr)] -> CExpr -> CExpr
cLet ites e = Cletrec [ CLValueSign (CDefT i [] (CQType [] t) [CClause [] [] e]) [] | (i, t, e) <- ites ] e

-- convert a CLMatch binding to non-pattern-matching let-bindings
expCLMatch :: CDefl -> TI [CDefl]
expCLMatch (CLMatch p e) =
    case expComma p of
    CPAny {} -> return []
    CPVar v -> return [bind v e]
    CPAs v p -> expand [bind v e] (CVar v) (expComma p)
    p' -> do
        --posCheck "H" p'
        v <- newVar (getPosition p) "expCLMatch"
        expand [bind v e] (CVar v) p'
  where bind i e = CLValue i [CClause [] [] e] []
        expand ds v (CPstruct mb ti fs)
          | mb /= (Just False) = do
                dss <- mapM (\ (f, p) -> expCLMatch (CLMatch p (CSelectTT ti v f))) fs
                return (concat (ds:dss))
        expand _ _ p = err (getPosition p, EBadMatch (pfpString p))
        expComma (CPCon comma [p1, p2]) | comma == idComma =
                CPstruct (Just True) (setIdPosition (getIdPosition comma) idPrimPair)
                    [(setIdPosition (getPosition p1) idPrimFst, p1),
                     (setIdPosition (getPosition p2) idPrimSnd, p2)]
        expComma p = p
expCLMatch d = return [d]

{-
posCheck s x =
    if getPosition x == noPosition then trace ("posCheck " ++ s) $ return () else return ()
-}

-------

-- XXX should do matching of t and td to avoid tyvars
freshInstT :: (HasPosition a, PPrint a, PVPrint a)
           => String -> a -> Scheme -> Type -> TI (Qual Type, [Type])
freshInstT msg x (Forall [] qt@(_ :=> t)) td = return (qt, [])
freshInstT msg x (Forall ks qt@(_ :=> t)) td = do
    s <- getSubst
    -- The whole purpose of fmatch is to avoid to create type variables when
    -- they are not needed.  It is purely an optimization; the Nothing branch
    -- of the case is always safe.
    case fmatch t (apSub s td) of
        Nothing -> do
--          traces ("freshInstT\n" ++ ppReadable t ++ ppReadable (apSub s td) ++ ppReadable (fmatch t (apSub s td))) return ()
            ts <- mapM (flip (newTVar ("freshInstT N " ++ msg)) x) ks
            return (inst ts qt, ts)
        Just its -> do
            let f (i, k) =
                    case [ t | (i', t) <- its, i == i' ] of
                        (t:ts) | kind t == k -> unifys t ts
                        _ -> newTVar ("freshInstT J " ++ msg) k x
                unifys t [] = return t
                unifys t (t':ts) = do _ <- unify x t t'; unifys t ts
            ts <- mapM f (zip [0..] ks)
            return (inst ts qt, ts)

fmatch :: Type -> Type -> Maybe [(Int, Type)]
fmatch _ _ = Nothing
{-
-- XXX broken, check /usr/users/lennart/proj/Sandburst/mojavebs/units/ma_am_uc/js
-- bsc +RTS -H100M -RTS -u -v PiDefs.bs
fmatch (TAp f a) (TAp f' a') = do
    fs <- fmatch f f'
    as <- fmatch a a'
    return (fs ++ as)
fmatch (TGen _ n) t = return [(n, t)]
fmatch (TCon tc) (TCon tc') | tc == tc' = return []
fmatch _ _ = Nothing
-}

-------

-- Error message for kind mismatch of bound type variables

errBoundTyVarKindMismatch :: Id -> TyVar -> TyVar -> TI ()
errBoundTyVarKindMismatch i v u =
    err (getPosition i, EBoundTyVarKindMismatch (pfpString v)
                            (pfpString (kind v)) (getPosition v)
                            (pfpString (kind u)) (getPosition u))

-------

-- typecheck and expression just to find out what type it has
-- trimming the substitution seems to be excessive work here
tiWithType :: [Assump] -> CExpr -> TI (Type, [VPred], CExpr)
tiWithType as e = do
   (v_id, v) <- newTVarId "tiForType" KStar e
   (ps, e') <- tiExpr as v e
   s <- getSubst
   let t = apSub s v
   -- when doTrim $ updSubst (trimSubst v_id)
   t' <- expandFullType t
   return (t', ps, e')

tiForType :: [Assump] -> CExpr -> TI (Type)
tiForType as e = fmap fst3 (tiWithType as e)

-------

findFieldDefault :: CType -> Id -> Id -> Id -> TI [(Id, CExpr)]
findFieldDefault td c c' qf = do
  sy <- getSymTab
  -- c might be an alias, where c' is the expanded type
  case (findFieldInfo sy c' qf) of
    Just (FieldInfo { fi_id = fid,
                      fi_assump = (_ :>: fscheme),
                      fi_default = cs }) ->
      if (null cs)
      then return []
      else do
        -- make the name for the Defl
        new_i <- newVar (getPosition c) "findFieldDefault"
        -- make the type for the Defl (if possible)
        -- (this is like what "convInst" does)
        td' <- expandFullType td
        let mqt = case (leftCon td') of
                    Nothing -> Nothing
                    Just tc ->
                      let structTVs = tyConArgs td'
                          (Forall ks qt) = fscheme
                          -- relying on the struct arguments being
                          -- the first vars
                          ks' = drop (length structTVs) ks
                          extraTVs = zipWith cTVarKind tmpVarIds ks'
                          ts = structTVs ++ extraTVs
                      in
                          -- drop the struct arguments
                          case (qualTypeToCQType (inst ts qt)) of
                            (CQType ps (TAp (TAp (TCon arr) a) r)) |
                                isTConArrow arr -> Just (CQType ps r)
                            x -> internalError ("findFieldDefault: inst: " ++
                                                ppReadable x)
        -- make the Defl
        let defl = case (mqt) of
                     Nothing -> CLValue new_i cs []
                     Just qt -> CLValueSign (CDef new_i qt cs) []
        -- XXX this is probably the wrong place to clean up the kinds,
        -- but it is convenient for now
        e <- ctxRed (Cletseq [defl] (CVar new_i))
        return [(unQualId qf, e)]
    Nothing -> internalError ("findFieldDefault: findFieldInfo: " ++
                              ppReadable (c,c',qf))

-------

checkMethodArgNames :: Id -> [CDefl] -> TI ()
checkMethodArgNames ti ds = do
    sy <- getSymTab

    -- -----------
    -- extract which fields of the ifc have names

    let
        -- Given a def for a field of the ifc, determine if it has
        -- explicit arguments.  Only accept fields defined by a single
        -- clause without argument qualifiers (since this is all that
        -- BSV accepts).
        getArgNames :: CDefl -> [(Id, [Id])]
        getArgNames (CLValue i [clause] _) = getArgNamesFromClause i clause
        getArgNames (CLValueSign (CDef i _ [clause]) _) =
            getArgNamesFromClause i clause
        getArgNames (CLValueSign (CDefT i _ _ [clause]) _) =
            getArgNamesFromClause i clause
        getArgNames _ = []

        getArgNamesFromClause :: Id -> CClause -> [(Id, [Id])]
        getArgNamesFromClause mId (CClause ps [] _) =
            let isPatVar (CPVar _) = True
                isPatVar _ = False
                getVarId (CPVar i) = i
                getVarId _ = internalError ("getVarId")
            in  if (not (null ps)) && (all isPatVar ps)
                then [(mId, map getVarId ps)]
                else []
        getArgNamesFromClause _ _ = []

    -- ----------
    -- look up each in the symtab and return the pairs which are found
    -- (any not found will be an error later)

    let checkNames qti (mId, def_ids) =
            let decl_ids = getMethodArgNames sy qti mId
                pairs = zip def_ids decl_ids
                areSame (a,b) = (a == b)
            in  case (partition areSame pairs) of
                  (_, []) -> return ()
                  (_, mismatches) ->
                      let toString (i1,i2) = (getIdString i1, getIdString i2)
                      in  twarn (getPosition mId,
                                 EMethodArgNameMismatch (getIdBaseString mId)
                                     (map toString mismatches))

    when (warnMethArgMismatch) $
      do -- make sure the interface name is qualified
         let qti = case (findType sy ti) of
                     Just (TypeInfo { ti_qual_id = Just i }) -> i
                     _ -> internalError ("tiExpr: Cinterface: " ++
                                         ppReadable ti)
         mapM_ (checkNames qti) (concatMap getArgNames ds)

-------