-- | The type checker
{-# LANGUAGE
      DeriveDataTypeable,
      FlexibleContexts,
      FlexibleInstances,
      GeneralizedNewtypeDeriving,
      ImplicitParams,
      MultiParamTypeClasses,
      ParallelListComp,
      PatternGuards,
      QuasiQuotes,
      ScopedTypeVariables,
      TemplateHaskell,
      TypeSynonymInstances,
      UndecidableInstances,
      ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
module Statics (
  -- * The type checking monad
  TC, runTC, tcMapM,
  -- * Static environments
  S, env0,
  -- ** Environment construction
  addVal, addType, addMod, addDecl,
  -- * Type checking
  tcProg, tcDecls,
  -- * Type checking results for the REPL
  runTCNew, Module(..), getExnParam, tyConToDec,
  getVarInfo, getTypeInfo, getConInfo,
) where

import Meta.Quasi
import Util
import qualified Syntax
import qualified Syntax.Decl
import qualified Syntax.Expr
import qualified Syntax.Notable
import qualified Syntax.Patt
import Syntax hiding (Type, Type'(..), tyAll, tyEx, tyUn, tyAf,
                      tyTuple, tyUnit, tyArr, tyApp,
                      TyPat, TyPat'(..))
import Loc
import Env as Env
import Ppr ()
import Type
import TypeRel
import Coercion (coerceExpression)

import Control.Monad.RWS    as RWS
import Data.Data (Typeable, Data)
import Data.Generics (everywhere, mkT)
import Data.List (transpose)
import Data.Monoid
import qualified Data.Map as M
import qualified Data.Set as S

import System.IO.Unsafe (unsafePerformIO)
pP :: Show a => a -> b -> b
pP a b = unsafePerformIO (print a) `seq` b
pM :: (Show a, Monad m) => a -> m ()
pM a = if pP a True then return () else fail "wibble"

-- The kind of names we're using.
type R = Renamed

---
--- Type checking environment
---

-- | Mapping from identifiers to value types (includes datacons)
type VE      = Env (BIdent R) Type
-- | Mapping from type constructor names to tycon info
type TE      = Env (Lid R) TyCon
-- | Mapping from module names to modules
type ME      = Env (Uid R) (Module, E)
-- | Mapping from module type names to signatures
type SE      = Env SIGVAR (Module, E)
-- | An environment
data E       = E {
                 vlevel :: VE, -- values
                 tlevel :: TE, -- types
                 mlevel :: ME, -- modules
                 slevel :: SE  -- module types
               }
  deriving (Typeable, Data)

-- | To distinguish signature variables from module variables
--   in overloaded situations
newtype SIGVAR  = SIGVAR { unSIGVAR :: Uid R }
  deriving (Eq, Ord, Typeable, Data)

instance Show SIGVAR where
  showsPrec p (SIGVAR u) = showsPrec p u

-- | A module item is empty, a pair of modules, a value entry (variable
--   or data constructor), a type constructor, or a module.
data Module
  = MdNil
  | MdApp    !Module     !Module
  | MdValue  !(BIdent R) !Type
  | MdTycon  !(Lid R)    !TyCon
  | MdModule !(Uid R)    !Module
  | MdSig    !(Uid R)    !Module
  deriving (Typeable, Data, Show)

-- | Convert an ordered module into an un-ordered environment
envify :: Module -> E
envify MdNil            = genEmpty
envify (MdApp md1 md2)  = envify md1 =+= envify md2
envify (MdValue  x t)   = genEmpty =+= x =:= t
envify (MdTycon  l tc)  = genEmpty =+= l =:= tc
envify (MdModule u md)  = genEmpty =+= u =:= (md, envify md)
envify (MdSig    u md)  = genEmpty =+= SIGVAR u =:= (md, envify md)

instance Monoid Module where
  mempty  = MdNil
  mappend = MdApp

instance Monoid E where
  mempty  = E empty empty empty empty
  mappend (E a1 a2 a3 a4) (E b1 b2 b3 b4)
    = E (a1 =+= b1) (a2 =+= b2) (a3 =+= b3) (a4 =+= b4)

-- Instances for generalizing environment operations over
-- the whole environment structure

instance GenEmpty E where
  genEmpty = mempty

instance GenExtend E E where
  (=+=) = mappend
instance GenExtend E VE where
  e =+= ve' = e =+= E ve' empty empty empty
instance GenExtend E TE where
  e =+= te' = e =+= E empty te' empty empty
instance GenExtend E ME where
  e =+= me' = e =+= E empty empty me' empty
instance GenExtend E SE where
  e =+= se' = e =+= E empty empty empty se'
instance GenLookup E (BIdent R) Type where
  e =..= k = vlevel e =..= k
instance GenLookup E (Lid R) TyCon where
  e =..= k = tlevel e =..= k
instance GenLookup E (Uid R) (Module, E) where
  e =..= k = mlevel e =..= k
instance GenLookup E SIGVAR (Module, E) where
  e =..= k = slevel e =..= k
instance GenLookup E k v =>
         GenLookup E (Path (Uid R) k) v where
  e =..= J []     k = e =..= k
  e =..= J (p:ps) k = do
    (_, e') <- e =..= p
    e' =..= J ps k

---
--- Type checking context and state
---

-- | The type checking context
data Context = Context {
  environment :: !E,
  modulePath  :: ![Uid R]
}

-- | The packaged-up state of the type-checker, which needs to be
--   threaded from one interaction to the next by the REPL
data S   = S {
             -- | The environment
             sEnv    :: E,
             -- | Index for gensyms
             currIx  :: !Int
           }

instance GenLookup E k v =>
         GenLookup Context (Path (Uid R) k) v where
  cxt =..= k = environment cxt =..= k

instance GenExtend Context E where
  cxt =+= e = cxt { environment = environment cxt =+= e }
instance GenExtend Context VE where
  cxt =+= venv = cxt =+= E venv empty empty empty
instance GenExtend Context TE where
  cxt =+= tenv = cxt =+= E empty tenv empty empty
instance GenExtend Context ME where
  cxt =+= menv = cxt =+= E empty empty menv empty
instance GenExtend Context SE where
  cxt =+= senv = cxt =+= E empty empty empty senv

---
--- The type-checking monad
---

-- | The type checking monad reads an environment, writes a module,
--   and keeps track of a gensym counter (currently unused).
newtype TC m a = TC { unTC :: RWST Context Module Int m a }
  deriving (Functor, Monad)

instance Monad m => Applicative (TC m) where
  pure  = return
  (<*>) = ap

instance Monad m => MonadWriter Module (TC m) where
  tell   = TC . tell
  listen = TC . listen . unTC
  pass   = TC . pass . unTC

instance Monad m => MonadReader Context (TC m) where
  ask     = TC ask
  local f = TC . local f . unTC

-- | Like 'ask', but monadic
asksM :: MonadReader r m => (r -> m a) -> m a
asksM  = (ask >>=)

-- | Run a type checking computation with the given initial state,
--   returning the result and the updated state
runTC :: Monad m => S -> TC m a -> m (a, S)
runTC  = liftM prj <$$> runTCNew where
  prj (a, _, s) = (a, s)

-- | Run a type checking computation with the given initial state,
--   returning the result and the updated state
runTCNew :: Monad m => S -> TC m a -> m (a, Module, S)
runTCNew s action = do
  let cxt = Context (sEnv s) []
      ix  = currIx s
  (a, ix', md) <- runRWST (unTC action) cxt ix
  let e'  = sEnv s =+= envify md
  return (a, md, S e' ix')

-- | Generate a fresh integer for use as a 'TyCon' id
newIndex :: Monad m => TC m Int
newIndex = TC $ do
  i <- get
  put (i + 1)
  return i

-- | Add a module to the current module path
enterModule :: Monad m => Uid R -> TC m a -> TC m a
enterModule u = local $ \cxt ->
  cxt { modulePath = u : modulePath cxt }

currentModulePath :: Monad m => TC m [Uid R]
currentModulePath  = asks (reverse . modulePath)

-- | Add a variable binding to the generated module
bindVar :: Monad m => Lid R -> Type -> TC m ()
bindVar l t = tell (MdValue (Var l) t)

-- | Add a data constructor binding to the generated module
bindCon :: Monad m => Uid R -> Type -> TC m ()
bindCon u t = tell (MdValue (Con u) t)

-- | Add a type constructor binding to the generated module
bindTycon :: Monad m => Lid R -> TyCon -> TC m ()
bindTycon l tc = tell (MdTycon l tc)

-- | Add a module binding to the generated module
bindModule :: Monad m => Uid R -> Module -> TC m ()
bindModule u md = tell (MdModule u md)

-- | Add a module type binding to the generated module
bindSig :: Monad m => Uid R -> Module -> TC m ()
bindSig u md = tell (MdSig u md)

-- | Run some computation with the context extended by a module
inModule :: Monad m => Module -> TC m a -> TC m a
inModule md = local (=+= envify md)

-- | Run in the environment consisting of only the given module
onlyInModule :: Monad m => Module -> TC m a -> TC m a
onlyInModule = local (\cxt -> cxt { environment = mempty }) <$$> inModule

-- | Grab the module generated by a computate, and generate the empty
--   module in turn
steal :: Monad m => TC m a -> TC m (a, Module)
steal = censor (const mempty) . listen

-- | Map a function over a list, allowing the exports of each item
--   to be in scope for the rest
tcMapM :: Monad m => (a -> TC m b) -> [a] -> TC m [b]
tcMapM _ []     = return []
tcMapM f (x:xs) = do
  (x', md) <- listen (f x)
  xs' <- inModule md $ tcMapM f xs
  return (x':xs')

{- -- deprecated?
-- | Abstract the given type by removing its datacon or synonym info
withoutConstructors :: Monad m =>
                       TyCon -> TC m a -> TC m a
withoutConstructors tc = TC . M.R.local clean . unTC where
  -- Note: only filters immediate scope -- should be right.
  clean (TCEnv env) = TCEnv (map eachScope env)
  eachScope      :: Scope -> Scope 
  eachScope scope = genModify scope emptyPath flevel
  flevel         :: Level -> Level
  flevel level    = level { vlevel = eachVe (vlevel level) }
  eachVe         :: VE -> VE
  eachVe          = fromList . filter keep . toList
  keep           :: (BIdent R, Type) -> Bool
  keep (Con _, TyFun _ _ (TyApp tc' _ _)) = tc' /= tc
  keep (Con _, TyApp tc' _ _)             = tc' /= tc
  keep _                                  = True
-}

-- | Try to look up any environment binding (value, tycon, ...)
find :: (Monad m, GenLookup Context k v, Show k) =>
          k -> TC m v
find k = asksM $ \cxt -> case cxt =..= k of
  Just v  -> return v
  Nothing -> fail $
    "BUG! type checker got unbound identifier: " ++ show k

-- | Try to look up any environment binding (value, tycon, ...)
tryFind :: (Monad m, GenLookup Context k v, Show k) =>
          k -> TC m (Maybe v)
tryFind k = asks (=..= k)

---
--- Type errors
---

-- | Raise a type error, with the dynamically-bound source location
terr :: (?loc :: Loc, Monad m) => String -> m a
terr  = fail . (label ++)
  where label = if isBogus ?loc
                  then "type error: "
                  else show ?loc ++ ":\ntype error: "

-- | A type checking "assertion" raises a type error if the
--   asserted condition is false.
tassert :: (?loc :: Loc, Monad m) =>
           Bool -> String -> m ()
tassert True  _ = return ()
tassert False s = terr s

-- | A common form of type error: A got B where C expected
tgot :: (?loc :: Loc, Monad m) =>
        String -> Type -> String -> m a
tgot who got expected = terr $ who ++ " got " ++ show got ++
                               " where " ++ expected ++ " expected"

-- | Combination of 'tassert' and 'tgot'
tassgot :: (?loc :: Loc, Monad m) =>
           Bool -> String -> Type -> String -> m ()
tassgot False = tgot
tassgot True  = \_ _ _ -> return ()

-- | Run a partial computation, and if it fails, substitute
--   the given failure message for the one generated
(|!) :: (?loc :: Loc, Monad m) => Maybe a -> String -> m a
m |! s = case m of
  Just r  -> return r
  _       -> terr s
infix 1 |!

-- | Conveniently weak-head normalize a type
hnT :: Monad m => Type -> m Type
hnT  = headNormalizeTypeM 100

-- | Check type for closed-ness and and defined-ness, and add info
tcType :: (?loc :: Loc, Monad m) =>
          Syntax.Type R -> TC m Type
tcType = tc where
  tc :: Monad m => Syntax.Type R -> TC m Type
  tc [$ty| '$tv |] = do
    return (TyVar tv)
  tc [$ty| $t1 -[$q]> $t2 |] = do
    TyFun <$> qInterpretM q
          <*> tcType t1
          <*> tcType t2
  tc [$ty| ($list:ts) $qlid:n |] = do
    ts'  <- mapM tc ts
    tc'  <- find n
    checkLength (length (tcArity tc'))
    checkBound (tcBounds tc') ts'
    return (tyApp tc' ts')
    where
      checkLength len =
        tassert (length ts == len) $
          "Type constructor " ++ show n ++ " applied to " ++
          show (length ts) ++ " arguments where " ++
          show len ++ " expected"
      checkBound quals ts' =
        tassert (all2 (\qlit t -> qualConst t <: qlit) quals ts') $
          "Type constructor " ++ show n ++
          " used at " ++ show (map (qRepresent . qualifier) ts') ++
          " where at most " ++ show quals ++ " is permitted"
  tc [$ty| $quant:u '$tv . $t |] =
    TyQu u tv <$> tc t
  tc [$ty| mu '$tv . $t |] = do
    case unfoldTyMu t of
      (_, N _ (Syntax.TyVar tv')) | tv == tv' ->
        terr $ "Recursive type ‘" ++ show (Syntax.tyMu tv t) ++
               "’ is not contractive."
      _ -> return ()
    t' <- tc t
    tassert (qualConst t' == tvqual tv) $
      "Recursive type " ++ show (Syntax.tyMu tv t) ++ " qualifier " ++
      "does not match its own type variable."
    return (TyMu tv t')
  tc [$ty| $anti:a |] = $antifail

-- | Type check an A expression
tcExpr :: Monad m => Expr R -> TC m (Type, Expr R)
tcExpr = tc where
  tc :: Monad m => Expr R -> TC m (Type, Expr R)
  tc e0 = let ?loc = getLoc e0 in case e0 of
    [$ex| $id:x |] -> do
      tx    <- find x
      x'    <- case view x of
                 Left _   -> return x
                 Right qu -> return (fmap Con qu)
      return (tx, [$ex|+ $id:x' |])
    [$ex| $str:s |] -> return (tyString, [$ex|+ $str:s |])
    [$ex| $int:z |] -> return (tyInt,    [$ex|+ $int:z |])
    [$ex| $flo:f |] -> return (tyFloat,  [$ex|+ $flo:f |])
    [$ex| match $e with $list:clauses |] -> do
      (t0, e') <- tc e
      (t1:ts, clauses') <- liftM unzip . forM clauses $ \(N note ca) -> do
        (xi', md) <- steal $ tcPatt t0 (capatt ca)
        (ti, ei') <- inModule md $ tc (caexpr ca)
        checkSharing "match" (caexpr ca) md
        return (ti, caClause xi' ei' <<@ note)
      tr <- foldM (\ti' ti -> ti' \/? ti
                      |! "Mismatch in match/let: " ++ show ti ++
                          " and " ++ show ti')
            t1 ts
      return (tr, [$ex|+ match $e' with $list:clauses' |])
    [$ex| let rec $list:bsN in $e2 |] -> do
      let bs = map dataOf bsN
      (tfs, md) <- steal $ forM bs $ \b -> do
        t' <- tcType (bntype b)
        tassert (syntacticValue (bnexpr b)) $
          "Not a syntactic value in let rec: " ++ show (bnexpr b)
        tassert (qualConst t' <: Qu) $
          "Affine type in let rec binding: " ++ show t'
        bindVar (bnvar b) t'
        return t'
      (tas, e's) <- liftM unzip $ inModule md $ mapM (tc . bnexpr) bs
      zipWithM_ (\tf ta ->
                   tassert (ta <: tf) $
                      "Actual type " ++ show ta ++
                      " does not agree with declared type " ++
                      show tf ++ " in let rec")
                tfs tas
      (t2, e2') <- inModule md $ tc e2
      let b's =
            zipWith3
              (\b tf e' -> newBinding b { bntype = typeToStx tf, bnexpr = e' })
              bs tfs e's
      return (t2, [$ex|+ let rec $list:b's in $e2' |])
    [$ex| let $decl:d in $e2 |] -> do
      (d', md)  <- steal $ tcDecl d
      (t2, e2') <- inModule md $ tc e2
      return (t2, [$ex|+ let $decl:d' in $e2' |])
    [$ex| ($e1, $e2) |] -> do
      (t1, e1') <- tc e1
      (t2, e2') <- tc e2
      return (t1 .*. t2, [$ex|+ ($e1', $e2') |])
    [$ex| fun ($x : $t) -> $e |] -> do
      t' <- tcType t
      (x', md) <- steal $ tcPatt t' x
      checkSharing "lambda" e md
      (te, e') <- inModule md $ tc e
      q <- getWorthiness e0
      return (TyFun q t' te, [$ex|+ fun ($x' : $stx:t') -> $e' |])
    [$ex| $_ $_ |] -> do
      tcExApp tc e0
    [$ex| fun '$tv -> $e |] -> do
      tassert (syntacticValue e) $
        "Not a syntactic value under type abstraction: " ++ show e0
      (t, e') <- tc e
      return (tyAll tv t, [$ex|+ fun '$tv -> $e' |])
    [$ex| $e1 [$t2] |] -> do
      (t1, e1') <- tc e1
      t2'       <- tcType t2
      t1'       <- tapply t1 t2'
      return (t1', [$ex|+ $e1' [$stx:t2'] |])
    [$ex| Pack[$opt:mt1]($t2, $e) |] -> do
      t2'      <- tcType t2
      (te, e') <- tc e
      t1'      <- case mt1 of
        Just t1 -> tcType t1
        Nothing -> return (makeExType te t2')
      case t1' of
        TyQu Exists tv t11' -> do
          te' <- tapply (tyAll tv t11') t2'
          tassert (te <: te') $
            "Could not pack type " ++ show te ++
            " (abstracting " ++ show t2 ++
            ") to get " ++ show t1'
          return (t1', [$ex| Pack[$stx:t1']($stx:t2', $e') |])
        _ -> tgot "Pack[-]" t1' "ex(istential) type"
    [$ex| ( $e1 : $t2 ) |] -> do
      (t1, e1') <- tc e1
      t2'       <- tcType t2
      tassgot (t1 <: t2')
        "type ascription (:)" t1 (show t2')
      return (t2', e1')
    [$ex| ( $e1 :> $t2 ) |] -> do
      (t1, e1') <- tc e1
      t2'       <- tcType t2
      tassgot (castableType t2')
        "cast (:>)" t1 "function type"
      e1'' <- coerceExpression (e1' <<@ e0) t1 t2'
      -- tcExpr e1'' -- re-type check the coerced expression
      return (t2', e1'')
    [$ex| $anti:a |]    -> $antifail
    [$ex| $antiL:a |]   -> $antifail
  --
  -- | Assert that type given to a name is allowed by its usage
  checkSharing :: (Monad m, ?loc :: Loc) =>
                  String -> Expr R -> Module -> TC m ()
  checkSharing name e = loop where
    loop md0 = case md0 of
      MdApp md1 md2     -> do loop md1; loop md2
      MdValue (Var l) t ->
          tassert (qualConst t <: usage (J [] l) e) $
            "Affine variable " ++ show l ++ " : " ++
            show t ++ " duplicated in " ++ name ++ " body"
      _                 -> return ()
  --
  -- | What is the join of the qualifiers of all free variables
  --   of the given expression?
  getWorthiness e =
    liftM bigVee . forM (M.keys (fv e)) $ \x -> do
      mtx <- tryFind (fmap Var x)
      return $ case mtx of
        Just tx -> qualifier tx
        _       -> minBound

-- | Remove all instances of t2 from t1, replacing with
--   a new type variable 
makeExType :: Type -> Type -> Type
makeExType t1 t2 = TyQu Exists tv $ everywhere (mkT erase) t1 where
  tv       = fastFreshTyVar (TV (lid "a") (qualConst t2)) (maxtv (t1, t2))
  erase t' = if t' == t2 then TyVar tv else t'

-- Get the usage (sharing) of a variable in an expression:
usage :: QLid R -> Expr R -> QLit
usage x e = case M.lookup x (fv e) of
  Just u | u > 1 -> Qu
  _              -> Qa

-- | Type check an application, given the type subsumption
--   relation, the appropriate type checking function, and the
--   expression to check.
--
-- This is highly ad-hoc, as it does significant local type inference.
-- Ick.
tcExApp :: (?loc :: Loc, Monad m) =>
           (Expr R -> TC m (Type, Expr R)) ->
           Expr R -> TC m (Type, Expr R)
tcExApp tc e0 = do
  let foralls t1 ts = do
        let (tvs, t1f) = vtQus Forall t1 -- peel off quantification
            (tas, _)   = vtFuns t1f      -- peel off arg types
            nargs      = min (length tas) (length ts)
            tup ps     = foldl tyTuple tyUnit (take nargs ps)
        -- try to find types to unify formals and actuals, and apply
        t1' <- tryUnify tvs (tup tas) (tup ts) >>= foldM tapply t1
        arrows t1' ts
      arrows tr                   [] = return tr
      arrows t'@(view -> TyQu Forall _ _) ts = foralls t' ts
      arrows (view -> TyFun _ ta tr) (t:ts) = do
        b <- unifies [] t ta
        tassgot b "Application (operand)" t (show ta)
        arrows tr ts
      arrows (view -> TyMu tv t') ts = arrows (tysubst tv (TyMu tv t') t') ts
      arrows t' _ = tgot "Application (operator)" t' "function type"
      unifies tvs ta tf =
        case tryUnify tvs ta tf of
          Just ts  -> do
            ta' <- foldM tapply (foldr tyAll ta tvs) ts
            if (ta' <: tf)
              then return True
              else deeper
          Nothing -> deeper
        where
          deeper = case ta of
            TyQu Forall tv ta1 -> unifies (tvs++[tv]) ta1 tf
            _                  -> return False
  let (es, e1) = unfoldExApp e0            -- get operator and args
  (t1, e1')   <- tc e1                     -- check operator
  (ts, es')   <- unzip `liftM` mapM tc es  -- check args
  tr <- foralls t1 ts
  return (tr, foldl exApp e1' es')

-- | Figure out the result type of a type application, given
--   the type of the function and the argument type
tapply :: (?loc :: Loc, Monad m) =>
          Type -> Type -> m Type
tapply (view -> TyQu Forall tv t1') t2 = do
  tassert (qualConst t2 <: tvqual tv) $
    "Type application cannot instantiate type variable " ++
    show tv ++ " with type " ++ show t2
  return (tysubst tv t2 t1')
tapply t1 _ = tgot "type application" t1 "(for)all type"

-- Given the type of thing to match and a pattern, return
-- the type environment bound by that pattern.
tcPatt :: (?loc :: Loc, Monad m) =>
          Type -> Patt R -> TC m (Patt R)
tcPatt t x0 = case x0 of
  [$pa| _ |]      -> return x0
  [$pa| $lid:x |] -> x0 <$ bindVar x t
  [$pa| $quid:u $opt:mx |] -> do
    t' <- hnT t
    case t' of
      TyApp _ ts _ -> do
        tu <- find (fmap Con u)
        (params, mt, res) <- case vtQus Forall tu of
          (params, TyFun _ arg res)
            -> return (params, Just arg, res)
          (params, res)
            -> return (params, Nothing, res)
        tassgot (t' <: tysubsts params ts res)
          "Pattern" t' ("constructor " ++ show u)
        case (mt, mx) of
          (Nothing, Nothing) ->
            return [$pa|+ $quid:u |]
          (Just t1, Just x1) -> do
            let t1' = tysubsts params ts t1
            x1' <- tcPatt t1' x1
            return [$pa|+ $quid:u $x1' |]
          _ -> tgot "Pattern" t "wrong arity"
      _ | isBotType t' -> case mx of
            Nothing -> return x0
            Just x  -> tcPatt tyBot x
        | otherwise -> tgot "Pattern" t' ("constructor " ++ show u)
  [$pa| ($x, $y) |] -> do
    t' <- hnT t >>! mapBottom (tyApp tcTuple . replicate 2)
    case t' of
      TyApp tc [xt, yt] _ | tc == tcTuple -> do
        x' <- tcPatt xt x
        y' <- tcPatt yt y
        return [$pa| ($x', $y') |]
      _ -> tgot "Pattern " t' "pair type"
  [$pa| $str:_ |] -> do
      tassgot (t <: tyString)
        "Pattern" t "string"
      return x0
  [$pa| $int:_ |] -> do
      tassgot (t <: tyInt)
        "Pattern" t "int"
      return x0
  [$pa| $flo:_ |] -> do
      tassgot (t <: tyFloat)
        "Pattern" t "float"
      return x0
  [$pa| $x as $lid:y |] -> do
    x' <- tcPatt t x
    bindVar y t
    return [$pa| $x' as $lid:y |]
  [$pa| Pack('$tv, $x) |] -> do
    t' <- hnT t >>! mapBottom (tyEx tv)
    case t' of
      TyQu Exists tve te -> do
        tassert (tvqual tve <: tvqual tv) $
          "Cannot bind existential tyvar " ++ show tv ++
          " to " ++ show tve
        let te' = tysubst tve (TyVar tv) te
        x' <- tcPatt te' x
        return [$pa| Pack('$tv, $x') |]
      _ -> tgot "Pattern" t' "existential type"
  [$pa| $antiL:a |] -> $antifail
  [$pa| $anti:a |]  -> $antifail

-- | Check if type is bottom, and if so, apply the given function
--   to it
mapBottom :: (Type -> Type) -> Type -> Type
mapBottom ft t
  | isBotType t = ft t
  | otherwise   = t

-- Given a list of type variables tvs, a type t in which tvs
-- may be free, and a type t', tries to substitute for tvs in t
-- to produce a type that *might* unify with t'
tryUnify :: (?loc :: Loc, Monad m) =>
            [TyVarR] -> Type -> Type -> m [Type]
tryUnify [] _ _        = return []
tryUnify tvs t t'      = 
  case subtype 100 [] t' tvs t of
    Left s         -> giveUp (s :: String)
    Right (_, ts)  -> return ts
  where
  giveUp _ = terr $
    "\nCannot guess type" ++
    (if length tvs == 1 then " t1" else "s t1, .., t" ++ show (length tvs))
    ++ " such that\n  " ++ showsPrec 10 t "" ++
    concat [ "[t" ++ show i ++ "/" ++ show tv ++ "]"
           | tv <- tvs | i <- [ 1.. ] :: [Integer] ] ++
    "\n  >: " ++ show t'

-- | Convert qualset representations from a list of all tyvars and
--   list of qualifier-significant tyvars to a set of type parameter
--   indices
indexQuals :: (?loc :: Loc, Monad m) =>
              Lid R -> [TyVarR] -> QExp R -> TC m (QDen Int)
indexQuals name tvs qexp = do
  qden <- qInterpretM qexp
  numberQDenM unbound tvs qden where
  unbound tv = terr $ "unbound tyvar " ++ show tv ++
                      " in qualifier list for type " ++ show name

-- BEGIN type decl checking

-- | Run a computation in the context of type declarations
tcTyDecs :: (?loc :: Loc, Monad m) =>
            [TyDec R] -> TC m [TyDec R]
tcTyDecs tds0 = do
  let (atds, stds, dtds) = foldr partition ([], [], []) tds0
  -- stds <- topSort getEdge stds0
  (_, stub) <- steal $ forM (atds ++ dtds ++ stds) $ \td0 ->
    case dataOf td0 of
      TdDat name params _   -> allocStub name (map tvqual params)
      TdSyn name ((ps,_):_) -> allocStub name (map (const Qa) ps)
      TdAbs name params variances quals -> do
        quals' <- indexQuals name params quals
        ix     <- newIndex
        us     <- currentModulePath
        let tc' = mkTC ix (J us name) quals'
                       [ (tvqual parm, var)
                       | var <- variances
                       | parm <- params ]
        bindTycon name tc'
      _                     -> return ()
  let loop md = do
        ((changed, tcs), md') <-
          steal $
            inModule md $
              liftM unzip $
                mapM tcTyDec (atds ++ dtds ++ stds)
        if or changed
          then loop md'
          else return (tcs, md')
   in do
     (tcs, md') <- loop stub
     forM_ tcs $ \tc -> do
       case tcNext tc of
         Nothing      -> return ()
         Just clauses -> forM_ clauses $ \(tps, rhs) ->
           tassert (rhs /= tyPatToType (TpApp tc {tcNext = Nothing} tps)) $
             "Type synonym ‘" ++ show tc ++ "’ is not contractive."
     tell (replaceTyCons tcs md')
     return tds0
  where
    allocStub name params = do
      ix <- newIndex
      us <- currentModulePath
      let tc = mkTC ix (J us name)
                    [ (q, Omnivariant) | q <- params ]
      bindTycon name tc
    --
    getEdge td0 = case dataOf td0 of
      TdSyn name cs     -> (name, S.unions (map (tyConsOfType . snd) cs))
      TdAbs name _ _ _  -> (name, S.empty)
      TdDat name _ alts -> (name, names) where
        names = S.unions [ tyConsOfType t | (_, Just t) <- alts ]
      TdAnti a          -> $antierror
    --
    partition td (atds, stds, dtds) =
      case dataOf td of
        TdAbs _ _ _ _ -> (td : atds, stds, dtds)
        TdSyn _ _     -> (atds, td : stds, dtds)
        TdDat _ _ _   -> (atds, stds, td : dtds)
        TdAnti a      -> $antierror

-- tcTyDec types a type declaration, but in addition to
-- returnng a declaration, it returns a boolean that indicates
-- whether the type metadata has changed, which allows for iterating
-- to a fixpoint.
tcTyDec :: (?loc :: Loc, Monad m) =>
           TyDec R -> TC m (Bool, TyCon)
tcTyDec td0 = case dataOf td0 of
  TdAbs name _ _ _ -> do
    tc   <- find (J [] name :: QLid R)
    bindTycon name tc
    return (False, tc)
  TdSyn name cs -> do
    tc   <- find (J [] name :: QLid R)
    let nparams = length (fst (head cs))
    tassert (all ((==) nparams . length . fst) cs) $
      "all type operator clauses have the same number of parameters"
    (cs', quals, vqs) <- liftM unzip3 $ forM cs $ \(tps, rhs) -> do
      rhs' <- tcType rhs
      let vs1 = ftvVs rhs'
      (tps', tvses, vqs) <- liftM unzip3 $ forM tps $ \tp -> do
        tp' <- tcTyPat tp
        let tpt  = tyPatToType tp'
            vs2  = ftvVs tpt
            vs'  = M.intersectionWith (*) vs1 vs2
            var  = bigVee (M.elems vs')
            qp   = qualConst tpt
            tvs  = qDenFtv (qualifier tpt)
        return (tp', tvs, (var, qp))
      let tvmap = M.unions [ M.fromDistinctAscList
                               [ (tv, i) | tv <- S.toAscList tvs ]
                           | tvs <- tvses
                           | i <- [ 0 .. ] ]
          qual  = numberQDenMap tvqual tvmap (qualifier rhs')
      return ((tps', rhs'), qual, vqs)
    let (arity, bounds) = unzip (map bigVee (transpose vqs))
        qual    = bigVee quals
        changed = arity /= tcArity tc
               || qual  /= tcQual tc
        tc'     = tc { tcArity = arity,    tcQual = qual,
                       tcNext  = Just cs', tcBounds = bounds }
    bindTycon name tc'
    return (changed, tc')
  TdDat name params alts -> do
    tc <- find (J [] name :: QLid R)
    alts' <- sequence
      [ case mt of
          Nothing -> return (cons, Nothing)
          Just t  -> do
            t' <- tcType t
            return (cons, Just t')
      | (cons, mt) <- alts ]
    let t'      = foldl tyTuple tyUnit [ t | (_, Just t) <- alts' ]
        qual    = numberQDen params (qualifier t')
        arity   = typeVariances params t'
        changed = arity /= tcArity tc
               || qual  /= tcQual tc
        tc'     = tc { tcArity = arity, tcQual = qual,
                       tcCons = (params, fromList alts') }
    bindTycon name tc'
    bindAlts params tc' alts'
    return (changed, tc')
  TdAnti a -> $antifail

-- | Build a module of datacon types from a datatype's
--   alternatives
bindAlts :: Monad m => [TyVarR] -> TyCon -> [(Uid R, Maybe Type)] -> TC m ()
bindAlts params tc = mapM_ each where
  each (u, Nothing) = bindCon u (alls result)
  each (u, Just t)  = bindCon u (alls (t .->. result))
  alls t            = foldr tyAll t params
  result            = tyApp tc (map TyVar params)

-- | Compute the variances at which some type variables occur
--   in an open type expression
typeVariances :: [TyVarR] -> Type -> [Variance]
typeVariances d0 = finish . ftvVs where
  finish m = [ maybe 0 id (M.lookup tv m)
             | tv <- d0 ]

-- | Generic topological sort
--
-- Uses an adjacency-list graph representation.  Given a
-- function from abstract node values to comparable nodes,
-- and a list of node values, returns a list of node values (or
-- fails if there's a cycle).
topSort :: forall node m a.
           (?loc :: Loc, Monad m, Ord node, Show node) =>
           (a -> (node, S.Set node)) -> [a] -> m [a]
topSort getEdge edges = do
  (_, w) <- RWS.execRWST visitAll S.empty S.empty
  return w
  where
    visitAll = mapM_ visit (M.keys graph)
    --
    visit :: node -> RWS.RWST (S.Set node) [a] (S.Set node) m ()
    visit node = do
      stack <- RWS.ask
      tassert (not (node `S.member` stack)) $
        "unproductive cycle in type definitions, via type " ++ show node
      seen <- RWS.get
      if node `S.member` seen
        then return ()
        else do
          RWS.put (S.insert node seen)
          case M.lookup node graph of
            Just (succs, info) -> do
              RWS.local (S.insert node) $
                mapM_ visit succs
              RWS.tell [info]
            Nothing ->
              return ()
    --
    graph :: M.Map node ([node], a)
    graph = M.fromList [ let (node, succs) = getEdge info
                          in (node, (S.toList succs, info))
                       | info <- edges ]

-- | The (unqualified) tycons that appear in a syntactic type
tyConsOfType :: Syntax.Type R -> S.Set (Lid R)
tyConsOfType [$ty| ($list:ts) $qlid:n |] =
  case n of
    J [] l -> S.singleton l
    _      -> S.empty
  `S.union` S.unions (map tyConsOfType ts)
tyConsOfType [$ty| '$_ |]              = S.empty
tyConsOfType [$ty| $t1 -[$_]> $t2 |]   =
  tyConsOfType t1 `S.union` tyConsOfType t2
tyConsOfType [$ty| $quant:_ '$_. $t |] = tyConsOfType t
tyConsOfType [$ty| mu '$_. $t |]       = tyConsOfType t
tyConsOfType [$ty| $anti:a |]          = $antierror

tcTyPat :: Monad m => Syntax.TyPat R -> TC m TyPat
tcTyPat (N note (Syntax.TpVar tv var))    = do
  let ?loc = getLoc note
  tassert (var == Invariant) $
    "type pattern variable " ++ show tv ++
    " cannot have a variance annotation"
  return (TpVar tv)
tcTyPat tp@[$tpQ| ($list:tps) $qlid:qu |] = do
  let ?loc = _loc
  tc <- find qu
  tassert (isNothing (tcNext tc)) $
    "type operator pattern `" ++ show tp ++
    "' cannot also be a type operator"
  TpApp tc <$> mapM tcTyPat tps
tcTyPat [$tpQ| $antiP:a |]             = $antifail

-- END type decl checking

-- | Type check a module body
tcSigExp :: (?loc :: Loc, Monad m) =>
            SigExp R -> TC m (SigExp R)
tcSigExp [$seQ| sig $list:ds end |] = do
  ds' <- tcMapM tcSigItem ds
  return [$seQ| sig $list:ds' end |]
tcSigExp [$seQ| $quid:n $list:qls |] = do
  (md, _) <- find (fmap SIGVAR n)
  tell md
  return [$seQ| $quid:n $list:qls |]
tcSigExp [$seQ| $se1 with type $list:tvs $qlid:tc = $t |] = do
  (se1', md) <- steal $ tcSigExp se1
  t'         <- tcType t
  fibrate tvs tc t' md
  return [$seQ| $se1' with type $list:tvs $qlid:tc = $t |]
tcSigExp [$seQ| $anti:a |] = $antifail

fibrate :: (?loc :: Loc, Monad m) =>
           [TyVar R] -> QLid R -> Type -> Module -> TC m ()
fibrate tvs ql t md = do
    let Just tc = findTycon ql md
    tassert (isAbstractTyCon tc) $
      "with-type: cannot update concrete type constructor `" ++
      show ql
    tassert (length tvs == length (tcArity tc)) $
      "with-type: " ++ show (length tvs) ++
      " parameters for type " ++ show ql ++
      " which has " ++ show (length (tcArity tc))
    let amap   = ftvVs t
        arity  = map (\tv -> fromJust (M.lookup tv amap)) tvs
        bounds = map tvqual tvs
        qual   = numberQDen tvs (qualifier t)
        next   = Just [(map TpVar tvs, t)]
        tc'    = tc {
                   tcArity  = arity,
                   tcBounds = bounds,
                   tcQual   = qual,
                   tcNext   = next
                 }
    tell (replaceTyCon tc' md)
  where
    findTycon ql0 md0 = case md0 of
      MdNil          -> mzero
      MdApp md1 md2  -> findTycon ql0 md1 `mplus` findTycon ql0 md2
      MdTycon l tc   -> if J [] l == ql0 then return tc else mzero
      MdModule u md1 -> case ql0 of
        J (u':us) l | u == u' -> findTycon (J us l) md1
        _                     -> mzero
      MdSig _ _      -> mzero
      MdValue _ _    -> mzero

tcSigItem :: (?loc :: Loc, Monad m) =>
             SigItem R -> TC m (SigItem R)
tcSigItem sg0 = case sg0 of
  [$sgQ| val $lid:l : $t |] -> do
    t' <- tcType t
    bindVar l t'
    return [$sgQ| val $lid:l : $t |]
  [$sgQ| type $list:tds |] -> do
     tds' <- tcTyDecs tds
     return [$sgQ| type $list:tds' |]
  [$sgQ| module $uid:u : $se1 |] -> do
    (se', md) <- steal $ tcSigExp se1
    bindModule u md
    return [$sgQ| module $uid:u : $se' |]
  [$sgQ| module type $uid:u = $se1 |] -> do
    se' <- tcSig u se1
    return [$sgQ| module type $uid:u = $se' |]
  [$sgQ| include $se1 |] -> do
    se' <- tcSigExp se1
    return [$sgQ| include $se' |]
  [$sgQ| exception $uid:u of $opt:mt |] -> do
    mt' <- tcException u mt
    return [$sgQ| exception $uid:u of $opt:mt' |]
  [$sgQ| $anti:a |] -> $antifail

-- | Run a computation in the context of a let declaration
tcLet :: (?loc :: Loc, Monad m) =>
         Patt R -> Maybe (Syntax.Type R) -> Expr R ->
         TC m (Patt R, Maybe (Syntax.Type R), Expr R)
tcLet x mt e = do
  tassert (S.null (dtv x)) $
    "Cannot unpack existential in top-level binding"
  (te, e') <- tcExpr e
  t' <- case mt of
    Just t  -> do
      t' <- tcType t
      tassert (qualConst t' == Qu) $
        "Declared type of top-level binding " ++ show x ++ " is not unlimited"
      tassert (te <: t') $
        "Declared type for top-level binding " ++ show x ++ " : " ++ show t' ++
        " is not subsumed by actual type " ++ show te
      return t'
    Nothing -> do
      tassert (qualConst te == Qu) $
        "Type of top-level binding `" ++ show x ++ "' is not unlimited"
      return te
  x' <- tcPatt t' x
  return (x', Just (typeToStx t'), e')

-- | Run a computation in the context of a module open declaration
tcOpen :: (?loc :: Loc, Monad m) =>
          ModExp R -> TC m (ModExp R)
tcOpen b = tcModExp b

-- | Run a computation in the context of a local block (that is, after
--   the block)
tcLocal :: (?loc :: Loc, Monad m) =>
           [Decl R] -> [Decl R] ->
           TC m ([Decl R], [Decl R])
tcLocal ds1 ds2 = do
  (ds1', md1) <- steal $ tcDecls ds1
  ds2' <- inModule md1 $ tcDecls ds2
  return (ds1', ds2')

-- | Run a computation in the context of a new exception variant
tcException :: (?loc :: Loc, Monad m) =>
               Uid R -> Maybe (Syntax.Type R) ->
               TC m (Maybe (Syntax.Type R))
tcException n mt = do
  mt' <- gmapM tcType mt
  bindCon n (maybe tyExn (`tyArr` tyExn) mt')
  return (fmap typeToStx mt')

-- | Type check and bind a module
tcMod :: (?loc :: Loc, Monad m) =>
         Uid R -> ModExp R -> TC m (ModExp R)
tcMod u me0 = do
  (me', md) <- steal $ enterModule u $ tcModExp me0
  bindModule u md
  return me'

-- | Type check and bind a signature
tcSig :: (?loc :: Loc, Monad m) =>
         Uid R -> SigExp R -> TC m (SigExp R)
tcSig u se0 = do
  (se', md) <- steal $ tcSigExp se0
  bindSig u md
  return se'

{-
-- | Determine types that are no longer reachable by name
--   in a given scope, and give them an ugly printing name
hideInvisible :: Monad m =>
                 Scope -> TC m Scope
hideInvisible (PEnv modenv level) = do
  level' <- withAny level $ everywhereM (mkM repair) level
  withAny level' $ do
    ((), modenv') <- mapAccumM
                   (\scope acc -> do
                      scope' <- hideInvisible scope
                      return (acc, scope'))
                   () modenv
    return (PEnv modenv' level')
  where
    repair :: Monad m => Type -> TC m Type
    repair t@(TyApp tc ts cache) = do
      mtc <- tryGetAny (tcName tc)
      return $ if mtc == Just tc
        then t
        else TyApp (hide tc) ts cache
    repair t = return t
    --
    hide :: TyCon -> TyCon
    hide tc@TyCon { tcName = J (Uid _ "?" : _) _ } = tc
    hide tc@TyCon { tcName = J qs (Lid _ k), tcId = i } =
      tc { tcName = J (Uid "?":qs) (Lid _ (k ++ ':' : show i)) }

-- | Replace the printing name of each type with the shortest
--   path to access that type.  (So unnecessary!)
requalifyTypes :: [Uid R] -> E -> E
requalifyTypes _uids env = map (fmap repairLevel) env where
  repairLevel :: Level -> Level
  repairLevel level = everywhere (mkT repair) level
  --
  repair :: TypeT -> TypeT
  repair t@(TyCon { }) = case tyConsInThisEnv -.- ttId (tyinfo t) of
    Nothing   -> t
    Just name -> t `setTycon` name
  repair t = t
  --
  tyConsInThisEnv :: Env Integer (QLid R)
  tyConsInThisEnv  = uids <...> foldr addToScopeMap empty env
  --
  addToScopeMap :: Scope -> Env Integer (QLid R) -> Env Integer (QLid R)
  addToScopeMap (PEnv ms level) acc = 
    foldr (Env.unionWith chooseQLid) acc
      (makeLevelMap level :
       [ uid <..> addToScopeMap menv empty
       | (uid, menv) <- toList ms ])
  --
  makeLevelMap (Level _ ts) =
    fromList [ (ttId tag, J [] lid)
             | (lid, info) <- toList ts,
               tag <- tagOfTyInfo info ]
  --
  tagOfTyInfo (TiAbs tag)     = [tag]
  tagOfTyInfo (TiSyn _ _)     = []
  tagOfTyInfo (TiDat tag _ _) = [tag]
  tagOfTyInfo TiExn           = [tdExn]
  --
  chooseQLid :: QLid R -> QLid R -> QLid R
  chooseQLid q1@(J p1 _) q2@(J p2 _)
    | length p1 < length p2 = q1
    | otherwise             = q2
  --
  (<..>) :: Functor f => p -> f (Path p k) -> f (Path p k)
  (<..>)  = fmap . (<.>)
  --
  (<...>) :: Functor f => [p] -> f (Path p k) -> f (Path p k)
  (<...>) = flip $ foldr (<..>)
-}

-- | Type check a module body
tcModExp :: (?loc :: Loc, Monad m) =>
            ModExp R -> TC m (ModExp R)
tcModExp [$me| struct $list:ds end |] = do
  ds' <- tcDecls ds
  return [$me| struct $list:ds' end |]
tcModExp [$me| $quid:n $list:qls |] = do
  (md, _) <- find n
  tell md
  return [$me| $quid:n $list:qls |]
tcModExp [$me| $me1 : $se2 |] = do
  (me1', md1) <- steal $ tcModExp me1
  (se2', md2) <- steal $ tcSigExp se2
  ascribeSignature md1 md2
  return [$me| $me1' : $se2' |]
tcModExp [$me| $anti:a |] = $antifail

-- | Run a computation in the context of an abstype block
tcAbsTy :: (?loc :: Loc, Monad m) =>
            [AbsTy R] -> [Decl R] ->
            TC m ([AbsTy R], [Decl R])
tcAbsTy atds ds = do
  (_,   md1) <- steal $ tcTyDecs (map (atdecl . dataOf) atds)
  (ds', md2) <- steal $ inModule md1 $ tcDecls ds
  tcs <- forM atds $ \at0 -> case view at0 of
    AbsTy arity quals (N _ (TdDat name params _)) -> do
      let env = envify md1
          tc  = fromJust (env =..= name)
      qualSet <- indexQuals name params quals
      tassert (length params == length (tcArity tc)) $
        "abstract-with-end: " ++ show (length params) ++
        " given for type " ++ show name ++
        " which has " ++ show (length (tcArity tc))
      tassert (all2 (<:) (tcArity tc) arity) $
        "abstract-with-end: declared arity for type " ++ show name ++
        ", " ++ show arity ++
        ", is more general than actual arity " ++ show (tcArity tc)
      tassert (tcQual tc <: qualSet) $ 
        "abstract-with-end: declared qualifier for type " ++ show name ++
        ", " ++ show qualSet ++
        ", is more general than actual qualifier " ++ show (tcQual tc)
      return $ abstractTyCon tc {
        tcQual  = qualSet,
        tcArity = arity,
        tcCons  = ([], empty)
      }
    _ -> terr "(BUG) Can't abstract non-datatypes"
  tell (replaceTyCons tcs (md1 `mappend` md2))
  return (atds, ds')

-- | Type check a declaration
tcDecl :: Monad m => Decl R -> TC m (Decl R)
tcDecl decl =
  let ?loc = getLoc decl in
    case decl of
      [$dc| let $x : $opt:t = $e |] -> do
        (x', t', e') <- tcLet x t e
        return [$dc| let $x' : $opt:t' = $e' |] 
      [$dc| type $list:tds |] -> do
        tds' <- tcTyDecs tds
        return [$dc| type $list:tds' |]
      [$dc| abstype $list:at with $list:ds end |] -> do
        (at', ds') <- tcAbsTy at ds
        return [$dc| abstype $list:at' with $list:ds' end |]
      [$dc| module $uid:x = $b |] -> do
        b' <- tcMod x b
        return [$dc| module $uid:x = $b' |]
      [$dc| module type $uid:x = $b |] -> do
        b' <- tcSig x b
        return [$dc| module type $uid:x = $b' |]
      [$dc| open $b |] -> do
        b' <- tcOpen b
        return [$dc| open $b' |]
      [$dc| local $list:ds0 with $list:ds1 end |] -> do
        (ds0', ds1') <- tcLocal ds0 ds1
        return [$dc| local $list:ds0' with $list:ds1' end |]
      [$dc| exception $uid:n of $opt:mt |] -> do
        mt' <- tcException n mt
        return [$dc| exception $uid:n of $opt:mt' |]
      [$dc| $anti:a |] -> $antifail

-- | Type check a sequence of declarations
tcDecls :: Monad m => [Decl R] -> TC m [Decl R]
tcDecls = tcMapM tcDecl

---
--- Module sealing
---

-- | For mapping renamed names (from structures) into unrenamed names
--   (in signatures)
data NameMap
  = NameMap {
      nmValues  :: Env (BIdent R) (BIdent R),
      nmTycons  :: Env (Lid R)    (Lid R),
      nmModules :: Env (Uid R)    (Uid R, NameMap),
      nmSigs    :: Env (Uid R)    (Uid R)
  }

instance Monoid NameMap where
  mempty = NameMap empty empty empty empty
  mappend (NameMap a1 a2 a3 a4) (NameMap b1 b2 b3 b4) =
    NameMap (a1 =+= b1) (a2 =+= b2) (a3 =+= b3) (a4 =+= b4) where

instance GenEmpty NameMap where
  genEmpty = mempty
instance GenExtend NameMap NameMap where
  (=+=) = mappend
instance GenLookup NameMap (BIdent R) (BIdent R) where
  e =..= k = nmValues e =..= k
instance GenLookup NameMap (Lid R) (Lid R) where
  e =..= k = nmTycons e =..= k
instance GenLookup NameMap (Uid R) (Uid R, NameMap) where
  e =..= k = nmModules e =..= k
instance GenLookup NameMap SIGVAR (Uid R) where
  e =..= k = nmSigs e =..= unSIGVAR k

-- | Given a module, construct a 'NameMap' mapping raw versions of its
--   names to the actual renamed version.
makeNameMap :: Module -> NameMap
makeNameMap md0 = case md0 of
  MdNil          -> mempty
  MdApp md1 md2  -> makeNameMap md1 =+= makeNameMap md2
  MdValue x _    -> mempty { nmValues  = unnameBIdent x =:= x }
  MdTycon x _    -> mempty { nmTycons  = unnameLid x =:= x }
  MdModule x md1 -> mempty { nmModules = unnameUid x =:= (x, makeNameMap md1) }
  MdSig x _      -> mempty { nmSigs    = unnameUid x =:= x }
  where
    unnameLid :: Lid R -> Lid R
    unnameLid  = lid . unLid
    unnameUid :: Uid R -> Uid R
    unnameUid  = uid . unUid
    unnameBIdent :: BIdent R -> BIdent R
    unnameBIdent (Var l) = Var (unnameLid l)
    unnameBIdent (Con u) = Con (unnameUid u)

-- | Given a module and a signature, ascribe the signature to the module
--   and write the result.
ascribeSignature :: (?loc :: Loc, Monad m) =>
                    Module -> Module -> TC m ()
ascribeSignature md1 md2 = do
  let md2'   = renameSig (makeNameMap md1) md2
  onlyInModule md1 $ do
    subst <- matchSigTycons md2'
    subsumeSig (applyTyConSubstInSig subst md2')
  let tcs    = getGenTycons md2' []
  tcs'      <- forM tcs $ \tc -> do
    ix <- newIndex
    return tc { tcId = ix }
  tell (substTyCons tcs tcs' md2')

-- | Make the names in a signature match the names from the module it's
--   being applied to.
renameSig :: NameMap -> Module -> Module
renameSig nm0 = loop where
  loop md0 = case md0 of
    MdNil          -> MdNil
    MdApp md1 md2  -> MdApp (loop md1) (loop md2)
    MdValue x t    -> MdValue (fromJust (nm0 =..= x)) t
    MdTycon x tc   -> MdTycon (fromJust (nm0 =..= x)) tc
    MdModule x md1 ->
      let Just (x', nm1) = nm0 =..= x
       in MdModule x' (renameSig nm1 md1)
    MdSig x md1    -> MdSig (fromJust (nm0 =..= SIGVAR x)) md1

-- | Given a signature, find the tycon substitutions necessary to
--   unify it with the module in the environment.
matchSigTycons :: Monad m => Module -> TC m TyConSubst
matchSigTycons = loop [] where
  loop path md0 = case md0 of
    MdNil          -> return mempty
    MdApp md1 md2  -> mappend <$> loop path md1 <*> loop path md2
    MdValue _ _    -> return mempty
    MdTycon x tc   -> do
      tc' <- find (J path x)
      return (makeTyConSubst [tc] [tc'])
    MdModule x md1 -> loop (path++[x]) md1
    MdSig _ _      -> return mempty

-- | Given a tycon substitution, apply it to all the values and
--   RIGHT-HAND-SIDES of type definitions in a signature.  In
--   particular, don't replace any tycon bindings directly, but do
--   replace any references to other types in their definitions.
applyTyConSubstInSig :: TyConSubst -> Module -> Module
applyTyConSubstInSig subst = loop where
  loop md0   = case md0 of
    MdNil          -> MdNil
    MdApp md1 md2  -> MdApp (loop md1) (loop md2)
    MdValue x t    -> MdValue x (applyTyConSubst subst t)
    MdTycon x tc   -> MdTycon x (applyTyConSubstInTyCon subst tc)
    MdModule x md1 -> MdModule x (loop md1)
    MdSig x md1    -> MdSig x (loop md1)

-- | Get a list of all the tycons that need a new index allocated
--   because they're generative.
getGenTycons :: Module -> [TyCon] -> [TyCon]
getGenTycons = loop where
  loop MdNil            = id
  loop (MdApp md1 md2)  = loop md1 . loop md2
  loop (MdValue _ _)    = id
  loop (MdTycon _ tc)   = if varietyOf tc == OperatorType
                            then id
                            else (tc:)
  loop (MdModule _ md1) = loop md1
  loop (MdSig _ _)      = id

-- | Check whether the given signature subsumes the signature
--   implicit in the environment; takes a 'NameMap' mapping un-renamed
--   signature names to renamed environment names.
subsumeSig :: (?loc :: Loc, Monad m) =>
              Module -> TC m ()
subsumeSig = loop where
  loop md0 = case md0 of
    MdNil         -> return ()
    MdApp md1 md2 -> do loop md1; loop md2
    MdValue x t    -> do
      t' <- find (J [] x :: Ident R)
      tassgot (t' <: t)
        ("in signature matching, variable `"++show x++"'") t' (show t)
    MdTycon x tc   -> do
      tc' <- find (J [] x :: QLid R)
      case varietyOf tc of
        AbstractType -> do
          tassert (length (tcArity tc') == length (tcArity tc)) $
            "in signature matching, cannot match type definition for " ++
            show (tcName tc) ++ " because the actual number of type " ++
            "parameters (" ++ show (length (tcArity tc')) ++
            " does not match the expected number (" ++
            show (length (tcArity tc)) ++ "("
          tassert (all2 (<:) (tcArity tc') (tcArity tc)) $
            "in signature matching, cannot match type definition for " ++
            show (tcName tc) ++ " because actual variance " ++
            show (tcArity tc') ++
            " is less general than expected variance " ++
            show (tcArity tc)
          tassert (all2 (<:) (tcBounds tc') (tcBounds tc)) $
            "in signature matching, cannot match type definition for " ++
            show (tcName tc) ++ " because actual parameter bounds " ++
            show (tcBounds tc') ++
            " is less general than expected parameter bounds " ++
            show (tcBounds tc)
          tassert (tcQual tc' <: tcQual tc) $ 
            "in signature matching, cannot match type definition for " ++
            show (tcName tc) ++ " because actual qualifier " ++
            show (tcQual tc') ++
            " is less general than expected qualifier " ++
            show (tcQual tc)
        OperatorType -> matchTycons tc' tc
        DataType     -> matchTycons tc' tc
    MdModule x md1 -> do
      (md2, _) <- find (J [] x :: QUid R)
      onlyInModule md2 $ subsumeSig md1
    MdSig x md1    -> do
      (md2, _)  <- find (J [] (SIGVAR x) :: Path (Uid R) SIGVAR)
      matchSigs md2 md1

-- | Check that two signatures match EXACTLY.
matchSigs :: (?loc :: Loc, Monad m) =>
             Module -> Module -> TC m ()
matchSigs md10 md20 = loop (linearize md10 []) (linearize md20 []) where
  loop [] []                = return ()
  loop (MdValue x1 t1 : sgs1) (MdValue x2 t2 : sgs2)
    | x1 == x2 && t1 == t2  = loop sgs1 sgs2
  loop (MdTycon x1 tc1 : sgs1) (MdTycon x2 tc2 : sgs2)
    | x1 == x2              = do
      matchTycons tc1 tc2
      loop (substTyCon tc1 tc2 sgs1) sgs2
  loop (MdModule x1 md1 : sgs1) (MdModule x2 md2 : sgs2)
    | x1 == x2              = do
      matchSigs md1 md2
      loop sgs1 sgs2
  loop (MdSig x1 md1 : sgs1) (MdSig x2 md2 : sgs2)
    | x1 == x2              = do
      matchSigs md1 md2
      loop sgs1 sgs2
  loop [] (sg : _)          = do
    terr $ "cannot match signature item: " ++ name sg
  loop (sg : _) []          = do
    terr $ "cannot match signature item: " ++ name sg
  loop (sg1 : _) (sg2 : _)  = do
    terr $ "cannot match signature items: " ++ name sg1 ++
           " and " ++ name sg2
  --
  name (MdValue x _)  = "value " ++ show x
  name (MdTycon x _)  = "type " ++ show x
  name (MdModule x _) = "module " ++ show x
  name (MdSig x _)    = "module type " ++ show x
  name _              = error "BUG! in Statics.matchSigs"

-- | Extensional equality for type constructors
tyconExtEq :: TyCon -> TyCon -> Bool
tyconExtEq tc1 tc2 | tcBounds tc1 == tcBounds tc2 =
  let tvs = zipWith (TyVar .) tvalphabet (tcBounds tc1)
   in tyApp tc1 tvs == tyApp tc2 tvs
tyconExtEq _   _   = False

-- | Check that two type constructors match exactly.
matchTycons :: (?loc :: Loc, Monad m) =>
               TyCon -> TyCon -> TC m ()
matchTycons tc1 tc2 = case (varietyOf tc1, varietyOf tc2) of
  (AbstractType, AbstractType) -> do
    tassert (tcArity tc1 == tcArity tc2) $
      estr "the arity" (show (tcArity tc1)) (show (tcArity tc2))
    tassert (tcBounds tc1 == tcBounds tc2) $
      estr "parameter bounds" (show (tcBounds tc1)) (show (tcBounds tc2))
    tassert (tcQual tc1 == tcQual tc2) $
      estr "qualifier" (show (tcQual tc1)) (show (tcQual tc2))
  (DataType, DataType) -> do
    let (tvs1, rhs1) = tcCons tc1
        (tvs2, rhs2) = tcCons tc2
    tassert (length tvs1 == length tvs2) $
      estr "number of parameters" (show (length tvs1)) (show (length tvs2))
    let mtv   = maxtv (tvs1, tvs2, Env.range rhs1, Env.range rhs2)
        tvs'  = fastFreshTyVars tvs1 mtv
        rhs1' = Env.mapVals (fmap (tysubsts tvs1 (map TyVar tvs'))) rhs1
        rhs2' = Env.mapVals (fmap (tysubsts tvs2 (map TyVar tvs'))) rhs2
    forM_ (Env.toList rhs1') $ \(k, t1) ->
      let Just t2 = rhs2' =..= k
       in tassert (t1 == t2) $ estr
            ("constructor `" ++ show k ++ "'")
            (maybe "nothing" show t1)
            (maybe "nothing" show t2)
  (OperatorType, _)            | tyconExtEq tc1 tc2 -> return ()
  (_,            OperatorType) | tyconExtEq tc1 tc2 -> return ()
  (OperatorType, OperatorType) -> do
    let next1 = fromJust (tcNext tc1)
        next2 = fromJust (tcNext tc2)
    tassert (length next1 == length next2) $
      estr "number of clauses" (show (length next1)) (show (length next2))
    forM_ (zip3 next1 next2 [1 :: Int .. ]) $
      \((tp1, t1), (tp2, t2), ix) -> do
        tassert (length tp1 == length tp2) $
          estr ("number of parameters in clause " ++ show ix)
               (show (length tp1)) (show (length tp2))
        (tvs1, tvs2) <- mconcat `liftM` zipWithM matchTypats tp1 tp2
        let mtv   = maxtv (tvs1, tvs2, t1, t2)
            tvs'  = fastFreshTyVars tvs1 mtv
            t1'   = tysubsts tvs1 (map TyVar tvs') t1
            t2'   = tysubsts tvs2 (map TyVar tvs') t2
        tassert (t1' == t2') $
          estr ("type operator right-hand sides in clause " ++ show ix)
               (show t1') (show t2')
  (v1, v2) -> terr $ estr "kind of definition" (show v1) (show v2)
  where
    estr what which1 which2 =
      "in signature matching, cannot match type definition for " ++
      show (tcName tc1) ++ " because the " ++ what ++
      " does not match (`" ++ which1 ++ "' vs. `" ++ which2 ++ "')"

-- | Check that two type patterns match, and return the pairs of
--   type variables that line up and thus need renaming.
matchTypats :: (?loc :: Loc, Monad m) =>
               TyPat -> TyPat -> TC m ([TyVar R], [TyVar R])
matchTypats (TpVar tv1) (TpVar tv2)
  = return ([tv1], [tv2])
matchTypats (TpApp tc1 tvs1) (TpApp tc2 tvs2)
  | tc1 == tc2
  = mconcat `liftM` zipWithM matchTypats tvs1 tvs2
matchTypats tp1 tp2
  = terr $ "in signature matching, cannot match type patterns `" ++
           show tp1 ++ "' and `" ++ show tp2 ++ "'"

-- | To flatten all the 'MdNil' and 'MdApp' constructors in a module
--   into an ordinary list.
linearize :: Module -> [Module] -> [Module]
linearize MdNil           = id
linearize (MdApp md1 md2) = linearize md1 . linearize md2
linearize md1             = (md1 :)

---
--- END Module Sealing
---

-- | Add the type of a value binding
addVal :: Monad m => Lid R -> Syntax.Type R -> TC m ()
addVal x t = do
  let ?loc = mkBogus "<addVal>"
  t' <- tcType t
  bindVar x t'

-- | Add an arbitrary declaration
addDecl     :: Monad m => Decl R -> TC m ()
addDecl d    = () <$ tcDecl d

-- | Add a type constructor binding
addType     :: Monad m => Lid R -> TyCon -> TC m ()
addType n tc = () <$ bindTycon n tc

-- | Add a nested submodule
addMod :: Monad m => Uid R -> TC m a -> TC m ()
addMod u action = do
  (_, md) <- steal $ enterModule u $ action
  bindModule u md

-- | Type check a program
tcProg :: Monad m => Prog R -> TC m (Type, Prog R)
tcProg [$prQ| $list:ds in $opt:e0 |] = do
  (ds', md) <- steal $ tcDecls ds
  (t, e0')  <- case e0 of
    Just e  -> liftM (second Just) $ inModule md $ tcExpr e
    Nothing -> return (tyUnit, Nothing)
  return (t, [$prQ|+ $list:ds' in $opt:e0' |])

-- | The initial type-checking state
env0 :: S
env0  = S e0 0 where
  e0 :: E
  e0  = genEmpty =+= (Con (uid "()") -:- tyUnit :: VE)

-- | Find out the parameter type of an exception
getExnParam :: Type -> Maybe (Maybe Type)
getExnParam (TyApp tc _ _)
  | tc == tcExn             = Just Nothing
getExnParam (TyFun _ t1 (TyApp tc _ _))
  | tc == tcExn             = Just (Just t1)
getExnParam _               = Nothing

-- | Reconstruct the declaration from a tycon binding, for printing
tyConToDec :: TyCon -> TyDec R
tyConToDec tc = case tc of
  _ | tc == tcExn
    -> tdAbs (lid "exn") [] [] maxBound
  TyCon { tcName = n, tcNext = Just clauses }
    -> tdSyn (jname n) [ (map tyPatToStx ps, typeToStx rhs)
                       | (ps, rhs) <- clauses ]
  TyCon { tcName = n, tcCons = (ps, alts) }
    | not (isEmpty alts)
    -> tdDat (jname n) ps [ (u, fmap typeToStx mt)
                          | (u, mt) <- toList alts ]
  TyCon { tcName = n }
    ->
    let tyvars = zipWith ($) tvalphabet (tcBounds tc)
     in tdAbs (jname n)
              (zipWith const tyvars (tcArity tc))
              (tcArity tc)
              (qRepresent
                (denumberQDen
                  (map (qInterpret . qeVar) tyvars)
                  (tcQual tc)))

getVarInfo :: QLid R -> S -> Maybe Type
getVarInfo ql (S e _) = e =..= fmap Var ql

getTypeInfo :: QLid R -> S -> Maybe TyCon
getTypeInfo ql (S e _) = e =..= ql

-- Find out about a type constructor.  If it's an exception constructor,
-- return 'Left' with its paramter, otherwise return the type construtor
-- of the result type
getConInfo :: QUid R -> S -> Maybe (Either (Maybe Type) TyCon)
getConInfo qu (S e _) = do
  t <- e =..= fmap Con qu
  case getExnParam t of
    Just mt -> Just (Left mt)
    Nothing ->
      let loop (TyFun _ _ t2) = loop t2
          loop (TyQu _ _ t1)  = loop t1
          loop (TyApp tc _ _) = Just (Right tc)
          loop _              = Nothing
       in loop t