module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where

-- The code here is based on the paper:
-- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich.
-- Practical type inference for arbitrary-rank types.
-- 14 September 2011

import GF.Grammar hiding (Env, VGen, VApp, VRecType)
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.Lockfield
import GF.Compile.Compute.ConcreteNew
import GF.Compile.Compute.Predef(predef,predefName)
import GF.Infra.CheckM
import GF.Data.Operations
import Control.Applicative(Applicative(..))
import Control.Monad(ap,liftM,mplus)
import GF.Text.Pretty
import Data.List (nub, (\\), tails)
import qualified Data.IntMap as IntMap
import Data.Maybe(fromMaybe,isNothing)

checkLType :: GlobalEnv -> Term -> Type -> Check (Term, Type)
checkLType ge t ty = runTcM $ do
  vty <- liftErr (eval ge [] ty)
  (t,_) <- tcRho ge [] t (Just vty)
  t <- zonkTerm t
  return (t,ty)

inferLType :: GlobalEnv -> Term -> Check (Term, Type)
inferLType ge t = runTcM $ do
  (t,ty) <- inferSigma ge [] t
  t  <- zonkTerm t
  ty <- zonkTerm =<< tc_value2term (geLoc ge) [] ty
  return (t,ty)

inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma)
inferSigma ge scope t = do                                      -- GEN1
  (t,ty) <- tcRho ge scope t Nothing
  env_tvs <- getMetaVars (geLoc ge) (scopeTypes scope)
  res_tvs <- getMetaVars (geLoc ge) [(scope,ty)]
  let forall_tvs = res_tvs \\ env_tvs
  quantify ge scope t forall_tvs ty

Just vtypeInt   = fmap (flip VApp []) (predef cInt)
Just vtypeFloat = fmap (flip VApp []) (predef cFloat)
Just vtypeInts  = fmap (\p i -> VApp p [VInt i]) (predef cInts)
vtypeStr   = VSort cStr
vtypeStrs  = VSort cStrs
vtypeType  = VSort cType
vtypePType = VSort cPType

tcRho :: GlobalEnv -> Scope -> Term -> Maybe Rho -> TcM (Term, Rho)
tcRho ge scope t@(EInt i)   mb_ty = instSigma ge scope t (vtypeInts i) mb_ty -- INT
tcRho ge scope t@(EFloat _) mb_ty = instSigma ge scope t vtypeFloat mb_ty    -- FLOAT
tcRho ge scope t@(K _)      mb_ty = instSigma ge scope t vtypeStr   mb_ty    -- STR
tcRho ge scope t@(Empty)    mb_ty = instSigma ge scope t vtypeStr   mb_ty
tcRho ge scope t@(Vr v)     mb_ty = do                          -- VAR
  case lookup v scope of
    Just v_sigma -> instSigma ge scope t v_sigma mb_ty
    Nothing      -> tcError ("Unknown variable" <+> v)
tcRho ge scope t@(Q id)     mb_ty =
  runTcA (tcOverloadFailed t) $
    tcApp ge scope t `bindTcA` \(t,ty) ->
      instSigma ge scope t ty mb_ty
tcRho ge scope t@(QC id)    mb_ty =
  runTcA (tcOverloadFailed t) $
    tcApp ge scope t `bindTcA` \(t,ty) ->
      instSigma ge scope t ty mb_ty
tcRho ge scope t@(App fun arg) mb_ty = do
  runTcA (tcOverloadFailed t) $
    tcApp ge scope t `bindTcA` \(t,ty) ->
      instSigma ge scope t ty mb_ty
tcRho ge scope (Abs bt var body) Nothing = do                   -- ABS1
  i <- newMeta scope vtypeType
  let arg_ty = VMeta i (scopeEnv scope) []
  (body,body_ty) <- tcRho ge ((var,arg_ty):scope) body Nothing
  return (Abs bt var body, (VProd bt arg_ty identW (Bind (const body_ty))))
tcRho ge scope t@(Abs Implicit var body) (Just ty) = do         -- ABS2
  (bt, var_ty, body_ty) <- unifyFun ge scope ty
  if bt == Implicit
    then return ()
    else tcError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected")
  (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) [])))
  return (Abs Implicit var body,ty)
tcRho ge scope (Abs Explicit var body) (Just ty) = do           -- ABS3
  (scope,f,ty') <- skolemise ge scope ty
  (_,var_ty,body_ty) <- unifyFun ge scope ty'
  (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) [])))
  return (f (Abs Explicit var body),ty)
tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do    -- LET
  (rhs,var_ty) <- case mb_ann_ty of
                    Nothing     -> inferSigma ge scope rhs
                    Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
                                      v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
                                      (rhs,_) <- tcRho ge scope rhs (Just v_ann_ty)
                                      return (rhs, v_ann_ty)
  (body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty
  var_ty <- tc_value2term (geLoc ge) (scopeVars scope) var_ty
  return (Let (var, (Just var_ty, rhs)) body, body_ty)
tcRho ge scope (Typed body ann_ty) mb_ty = do                   -- ANNOT
  (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
  v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
  (body,_) <- tcRho ge scope body (Just v_ann_ty)
  instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty
tcRho ge scope (FV ts) mb_ty = do
  case ts of
    []     -> do i <- newMeta scope vtypeType
                 instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty
    (t:ts) -> do (t,ty) <- tcRho ge scope t mb_ty

                 let go []     ty = return ([],ty)
                     go (t:ts) ty = do (t, ty) <- tcRho ge scope t (Just ty)
                                       (ts,ty) <- go ts ty
                                       return (t:ts,ty)

                 (ts,ty) <- go ts ty
                 return (FV (t:ts), ty)
tcRho ge scope t@(Sort s) mb_ty = do
  instSigma ge scope t vtypeType mb_ty
tcRho ge scope t@(RecType rs) Nothing   = do
  (rs,mb_ty) <- tcRecTypeFields ge scope rs Nothing
  return (RecType rs,fromMaybe vtypePType mb_ty)
tcRho ge scope t@(RecType rs) (Just ty) = do
  (scope,f,ty') <- skolemise ge scope ty
  case ty' of
    VSort s
      | s == cType  -> return ()
      | s == cPType -> return ()
    VMeta i env vs  -> case rs of
                         [] -> unifyVar ge scope i env vs vtypePType
                         _  -> return ()
    ty              -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
                          tcError ("The record type" <+> ppTerm Unqualified 0 t $$ 
                                   "cannot be of type" <+> ppTerm Unqualified 0 ty)
  (rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
  return (f (RecType rs),ty)
tcRho ge scope t@(Table p res) mb_ty = do
  (p,  p_ty)   <- tcRho ge scope p   (Just vtypePType)
  (res,res_ty) <- tcRho ge scope res (Just vtypeType)
  instSigma ge scope (Table p res) vtypeType mb_ty
tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do
  (ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType)
  vty1 <- liftErr (eval ge (scopeEnv scope) ty1)
  (ty2,ty2_ty) <- tcRho ge ((x,vty1):scope) ty2 (Just vtypeType)
  instSigma ge scope (Prod bt x ty1 ty2) vtypeType mb_ty
tcRho ge scope (S t p) mb_ty = do
  p_ty   <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType
  res_ty <- case mb_ty of
              Nothing -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType
              Just ty -> return ty
  let t_ty = VTblType p_ty res_ty
  (t,t_ty) <- tcRho ge scope t (Just t_ty)
  (p,_) <- tcRho ge scope p (Just p_ty)
  return (S t p, res_ty)
tcRho ge scope (T tt ps) Nothing = do                           -- ABS1/AABS1 for tables
  p_ty   <- case tt of
              TRaw      -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType
              TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
                              liftErr (eval ge (scopeEnv scope) ty)
  (ps,mb_res_ty) <- tcCases ge scope ps p_ty Nothing
  res_ty <- case mb_res_ty of
              Just res_ty -> return res_ty
              Nothing     -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType
  p_ty_t <- tc_value2term (geLoc ge) [] p_ty
  return (T (TTyped p_ty_t) ps, VTblType p_ty res_ty)
tcRho ge scope (T tt ps) (Just ty) = do                         -- ABS2/AABS2 for tables
  (scope,f,ty') <- skolemise ge scope ty
  (p_ty, res_ty) <- unifyTbl ge scope ty'
  case tt of
    TRaw      -> return ()
    TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
                    return ()--subsCheckRho ge scope -> Term ty res_ty
  (ps,Just res_ty) <- tcCases ge scope ps p_ty (Just res_ty)
  p_ty_t <- tc_value2term (geLoc ge) [] p_ty
  return (f (T (TTyped p_ty_t) ps), VTblType p_ty res_ty)
tcRho ge scope (R rs) Nothing = do
  lttys <- inferRecFields ge scope rs
  rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
  return (R        rs,
          VRecType [(l, ty) | (l,t,ty) <- lttys]
         )
tcRho ge scope (R rs) (Just ty) = do
  (scope,f,ty') <- skolemise ge scope ty
  case ty' of
    (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
                          rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
                          return ((f . R)  rs, 
                                  VRecType [(l, ty) | (l,t,ty) <- lttys]
                                 )
    ty              -> do lttys <- inferRecFields ge scope rs
                          t <- liftM (f . R) (mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
                          let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys]
                          t <- subsCheckRho ge scope t ty' ty
                          return (t, ty')
tcRho ge scope (P t l) mb_ty = do
  l_ty   <- case mb_ty of
              Just ty -> return ty
              Nothing -> do i <- newMeta scope vtypeType
                            return (VMeta i (scopeEnv scope) [])
  (t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,l_ty)]))
  return (P t l,l_ty)
tcRho ge scope (C t1 t2) mb_ty = do
  (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr)
  (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr)
  instSigma ge scope (C t1 t2) vtypeStr mb_ty
tcRho ge scope (Glue t1 t2) mb_ty = do
  (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr)
  (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr)
  instSigma ge scope (Glue t1 t2) vtypeStr mb_ty
tcRho ge scope t@(ExtR t1 t2) mb_ty = do
  (t1,t1_ty) <- tcRho ge scope t1 Nothing
  (t2,t2_ty) <- tcRho ge scope t2 Nothing
  case (t1_ty,t2_ty) of
    (VSort s1,VSort s2)
       | (s1 == cType || s1 == cPType) &&
         (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType
                                                   | otherwise                    = cType
                                          in instSigma ge scope (ExtR t1 t2) (VSort sort) mb_ty
    (VRecType rs1, VRecType rs2)       -> instSigma ge scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty
    _                                  -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t)
tcRho ge scope (ELin cat t) mb_ty = do  -- this could be done earlier, i.e. in the parser
  tcRho ge scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
tcRho ge scope (ELincat cat t) mb_ty = do  -- this could be done earlier, i.e. in the parser
  tcRho ge scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty
tcRho ge scope (Alts t ss) mb_ty = do
  (t,_) <- tcRho ge scope t (Just vtypeStr)
  ss    <- flip mapM ss $ \(t1,t2) -> do
              (t1,_) <- tcRho ge scope t1 (Just vtypeStr)
              (t2,_) <- tcRho ge scope t2 (Just vtypeStrs)
              return (t1,t2)
  instSigma ge scope (Alts t ss) vtypeStr mb_ty
tcRho ge scope (Strs ss) mb_ty = do
  ss <- flip mapM ss $ \t -> do
           (t,_) <- tcRho ge scope t (Just vtypeStr)
           return t
  instSigma ge scope (Strs ss) vtypeStrs mb_ty
tcRho ge scope (EPattType ty) mb_ty = do
  (ty, _) <- tcRho ge scope ty (Just vtypeType)
  instSigma ge scope (EPattType ty) vtypeType mb_ty
tcRho ge scope t@(EPatt p) mb_ty = do
  (scope,f,ty) <- case mb_ty of
                    Nothing -> do i <- newMeta scope vtypeType
                                  return (scope,id,VMeta i (scopeEnv scope) [])
                    Just ty -> do (scope,f,ty) <- skolemise ge scope ty
                                  case ty of
                                    VPattType ty -> return (scope,f,ty)
                                    _            -> tcError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
  tcPatt ge scope p ty
  return (f (EPatt p), ty)
tcRho gr scope t _ = unimplemented ("tcRho "++show t)

tcCases ge scope []         p_ty mb_res_ty = return ([],mb_res_ty)
tcCases ge scope ((p,t):cs) p_ty mb_res_ty = do
  scope' <- tcPatt ge scope p p_ty
  (t,res_ty)     <- tcRho ge scope' t mb_res_ty
  (cs,mb_res_ty) <- tcCases ge scope cs p_ty (Just res_ty)
  return ((p,t):cs,mb_res_ty)


tcApp ge scope t@(App fun (ImplArg arg)) = do                   -- APP1
  tcApp ge scope fun `bindTcA` \(fun,fun_ty) ->
     do (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty
        if (bt == Implicit)
          then return ()
          else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected")
        (arg,_) <- tcRho ge scope arg (Just arg_ty)
        varg <- liftErr (eval ge (scopeEnv scope) arg)
        return (App fun (ImplArg arg), res_ty varg)
tcApp ge scope (App fun arg) =                                  -- APP2
  tcApp ge scope fun `bindTcA` \(fun,fun_ty) ->
     do (fun,fun_ty) <- instantiate scope fun fun_ty
        (_, arg_ty, res_ty) <- unifyFun ge scope fun_ty
        (arg,_) <- tcRho ge scope arg (Just arg_ty)
        varg <- liftErr (eval ge (scopeEnv scope) arg)
        return (App fun arg, res_ty varg)
tcApp ge scope (Q id) =                                          -- VAR (global)
  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> 
     do ty <- liftErr (eval ge [] ty)
        return (t,ty)
tcApp ge scope (QC id) =                                         -- VAR (global)
  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> 
     do ty <- liftErr (eval ge [] ty)
        return (t,ty)
tcApp ge scope t =
  singleTcA (tcRho ge scope t Nothing)


tcOverloadFailed t ttys =
  tcError ("Overload resolution failed" $$
           "of term   " <+> pp t $$
           "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys])


tcPatt ge scope PW        ty0 =
  return scope
tcPatt ge scope (PV x)    ty0 =
  return ((x,ty0):scope)
tcPatt ge scope (PP c ps) ty0 =
  case lookupResType (geGrammar ge) c of
    Ok ty  -> do let go scope ty []     = return (scope,ty)
                     go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun ge scope ty
                                             scope <- tcPatt ge scope p arg_ty
                                             go scope (res_ty (VGen (length scope) [])) ps
                 vty <- liftErr (eval ge [] ty)
                 (scope,ty) <- go scope vty ps
                 unify ge scope ty0 ty
                 return scope
    Bad err -> tcError (pp err)
tcPatt ge scope (PInt i) ty0 = do
  subsCheckRho ge scope (EInt i) (vtypeInts i) ty0
  return scope
tcPatt ge scope (PString s) ty0 = do
  unify ge scope ty0 vtypeStr
  return scope
tcPatt ge scope PChar ty0 = do
  unify ge scope ty0 vtypeStr
  return scope
tcPatt ge scope (PSeq p1 p2) ty0 = do
  unify ge scope ty0 vtypeStr
  scope <- tcPatt ge scope p1 vtypeStr
  scope <- tcPatt ge scope p2 vtypeStr
  return scope
tcPatt ge scope (PAs x p) ty0 = do
  tcPatt ge ((x,ty0):scope) p ty0
tcPatt ge scope (PR rs) ty0 = do
  let mk_ltys  []            = return []
      mk_ltys  ((l,p):rs)    = do i <- newMeta scope vtypePType
                                  ltys <- mk_ltys rs
                                  return ((l,p,VMeta i (scopeEnv scope) []) : ltys)
      go scope []            = return scope
      go scope ((l,p,ty):rs) = do scope <- tcPatt ge scope p ty
                                  go scope rs
  ltys <- mk_ltys rs
  subsCheckRho ge scope (EPatt (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0
  go scope ltys
tcPatt ge scope (PAlt p1 p2) ty0 = do
  tcPatt ge scope p1 ty0
  tcPatt ge scope p2 ty0
  return scope
tcPatt ge scope (PM q) ty0 = do
  case lookupResType (geGrammar ge) q of
    Ok (EPattType ty)
            -> do vty <- liftErr (eval ge [] ty)
                  unify ge scope ty0 vty
                  return scope
    Ok ty   -> tcError ("Pattern type expected but " <+> pp ty <+> " found.")
    Bad err -> tcError (pp err)
tcPatt ge scope p ty = unimplemented ("tcPatt "++show p)

inferRecFields ge scope rs = 
  mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs

checkRecFields ge scope []          ltys
  | null ltys                            = return []
  | otherwise                            = tcError ("Missing fields:" <+> hsep (map fst ltys))
checkRecFields ge scope ((l,t):lts) ltys =
  case takeIt l ltys of
    (Just ty,ltys) -> do ltty  <- tcRecField ge scope l t (Just ty)
                         lttys <- checkRecFields ge scope lts ltys
                         return (ltty : lttys)
    (Nothing,ltys) -> do tcWarn ("Discarded field:" <+> l)
                         ltty  <- tcRecField ge scope l t Nothing
                         lttys <- checkRecFields ge scope lts ltys
                         return lttys     -- ignore the field
  where
    takeIt l1 []  = (Nothing, [])
    takeIt l1 (lty@(l2,ty):ltys)
      | l1 == l2  = (Just ty,ltys) 
      | otherwise = let (mb_ty,ltys') = takeIt l1 ltys
                    in (mb_ty,lty:ltys')

tcRecField ge scope l (mb_ann_ty,t) mb_ty = do
  (t,ty) <- case mb_ann_ty of
              Just ann_ty -> do (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
                                v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
                                (t,_) <- tcRho ge scope t (Just v_ann_ty)
                                instSigma ge scope t v_ann_ty mb_ty
              Nothing     -> tcRho ge scope t mb_ty
  return (l,t,ty)

tcRecTypeFields ge scope []          mb_ty = return ([],mb_ty)
tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
  (ty,sort) <- tcRho ge scope ty mb_ty
  mb_ty <- case sort of
             VSort s
               | s == cType  -> return (Just sort)
               | s == cPType -> return mb_ty
             VMeta _ _ _     -> return mb_ty
             _               -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort
                                   tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ 
                                            "cannot be of type" <+> ppTerm Unqualified 0 sort)
  (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
  return ((l,ty):rs,mb_ty)

-- | Invariant: if the third argument is (Just rho),
-- 	            then rho is in weak-prenex form
instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
instSigma ge scope t ty1 Nothing    = return (t,ty1)           -- INST1
instSigma ge scope t ty1 (Just ty2) = do                       -- INST2
  t <- subsCheckRho ge scope t ty1 ty2
  return (t,ty2)

-- | Invariant: the second argument is in weak-prenex form
subsCheckRho :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> TcM Term
subsCheckRho ge scope t ty1@(VMeta i env vs) ty2 = do
  mv <- getMeta i
  case mv of
    Unbound _ _ -> do unify ge scope ty1 ty2
                      return t
    Bound ty1   -> do vty1 <- liftErr (eval ge env ty1)
                      subsCheckRho ge scope t (vapply (geLoc ge) vty1 vs) ty2
subsCheckRho ge scope t ty1 ty2@(VMeta i env vs) = do
  mv <- getMeta i
  case mv of
    Unbound _ _ -> do unify ge scope ty1 ty2
                      return t
    Bound ty2   -> do vty2 <- liftErr (eval ge env ty2)
                      subsCheckRho ge scope t ty1 (vapply (geLoc ge) vty2 vs)
subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do     -- Rule SPEC
  i <- newMeta scope ty1
  subsCheckRho ge scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) rho2
subsCheckRho ge scope t rho1 (VProd Implicit ty1 x (Bind ty2)) = do     -- Rule SKOL
  let v = newVar scope
  t <- subsCheckRho ge ((v,ty1):scope) t rho1 (ty2 (VGen (length scope) []))
  return (Abs Implicit v t)
subsCheckRho ge scope t rho1 (VProd Explicit a2 _ (Bind r2)) = do       -- Rule FUN
  (_,a1,r1) <- unifyFun ge scope rho1
  subsCheckFun ge scope t a1 r1 a2 r2
subsCheckRho ge scope t (VProd Explicit a1 _ (Bind r1)) rho2 = do       -- Rule FUN
  (bt,a2,r2) <- unifyFun ge scope rho2
  subsCheckFun ge scope t a1 r1 a2 r2
subsCheckRho ge scope t rho1 (VTblType p2 r2) = do                      -- Rule TABLE
  (p1,r1) <- unifyTbl ge scope rho1
  subsCheckTbl ge scope t p1 r1 p2 r2
subsCheckRho ge scope t (VTblType p1 r1) rho2 = do                      -- Rule TABLE
  (p2,r2) <- unifyTbl ge scope rho2
  subsCheckTbl ge scope t p1 r1 p2 r2
subsCheckRho ge scope t (VSort s1) (VSort s2)                           -- Rule PTYPE
  | s1 == cPType && s2 == cType = return t
subsCheckRho ge scope t (VApp p1 _) (VApp p2 _)                         -- Rule INT1
  | predefName p1 == cInts && predefName p2 == cInt = return t
subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j])           -- Rule INT2
  | predefName p1 == cInts && predefName p2 == cInts =
      if i <= j 
        then return t
        else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do      -- Rule REC
  let mkAccess scope t = 
        case t of
          ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1
                           (scope,mkProj2,mkWrap2) <- mkAccess scope t2
                           return (scope
                                  ,\l -> mkProj2 l `mplus` mkProj1 l
                                  ,mkWrap1 . mkWrap2
                                  )
          R rs -> do sequence_ [tcWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup l rs2)]
                     return (scope
                            ,\l -> lookup l rs
                            ,id
                            )
          Vr x -> do return (scope
                            ,\l -> do VRecType rs <- lookup x scope
                                      ty <- lookup l rs
                                      return (Nothing,P t l)
                            ,id
                            )
          t    -> let x = newVar scope
                  in return (((x,ty1):scope)
                            ,\l  -> return (Nothing,P (Vr x) l)
                            ,Let (x, (Nothing, t))
                            )

      mkField scope l (mb_ty,t) ty1 ty2 = do
        t <- subsCheckRho ge scope t ty1 ty2
        return (l, (mb_ty,t))

  (scope,mkProj,mkWrap) <- mkAccess scope t

  let fields = [(l,ty2,lookup l rs1) | (l,ty2) <- rs2]
  case [l | (l,_,Nothing) <- fields] of
    []      -> return ()
    missing -> tcError ("In the term" <+> pp t $$
                        "there are no values for fields:" <+> hsep missing)
  rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]]
  return (mkWrap (R rs))
subsCheckRho ge scope t tau1 tau2 = do                                  -- Rule EQ
  unify ge scope tau1 tau2                                 -- Revert to ordinary unification
  return t

subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> TcM Term
subsCheckFun ge scope t a1 r1 a2 r2 = do
  let v   = newVar scope
  vt <- subsCheckRho ge ((v,a2):scope) (Vr v) a2 a1
  val1 <- liftErr (eval ge (scopeEnv ((v,vtypeType):scope)) vt)
  val2 <- return  (VGen (length scope) [])
  t  <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) (r1 val1) (r2 val2)
  return (Abs Explicit v t)

subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
subsCheckTbl ge scope t p1 r1 p2 r2 = do
  let x = newVar scope
  xt <- subsCheckRho ge scope (Vr x) p2 p1
  t  <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ;
  p2 <- tc_value2term (geLoc ge) (scopeVars scope) p2
  return (T (TTyped p2) [(PV x,t)])

-----------------------------------------------------------------------
-- Unification
-----------------------------------------------------------------------

unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (BindType, Sigma, Value -> Rho)
unifyFun ge scope (VProd bt arg x (Bind res)) =
  return (bt,arg,res)
unifyFun ge scope tau = do
  let mk_val ty = VMeta ty [] []
  arg <- fmap mk_val $ newMeta scope vtypeType
  res <- fmap mk_val $ newMeta scope vtypeType
  let bt = Explicit
  unify ge scope tau (VProd bt arg identW (Bind (const res)))
  return (bt,arg,const res)

unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho)
unifyTbl ge scope (VTblType arg res) =
  return (arg,res)
unifyTbl ge scope tau = do
  let mk_val ty = VMeta ty (scopeEnv scope) []
  arg <- fmap mk_val $ newMeta scope vtypePType
  res <- fmap mk_val $ newMeta scope vtypeType
  unify ge scope tau (VTblType arg res)
  return (arg,res)

unify ge scope (VApp f1 vs1)      (VApp f2 vs2)
  | f1 == f2                   = sequence_ (zipWith (unify ge scope) vs1 vs2)
unify ge scope (VCApp f1 vs1)     (VCApp f2 vs2)
  | f1 == f2                   = sequence_ (zipWith (unify ge scope) vs1 vs2)
unify ge scope (VSort s1)         (VSort s2)
  | s1 == s2                   = return ()
unify ge scope (VGen i vs1)       (VGen j vs2)
  | i == j                     = sequence_ (zipWith (unify ge scope) vs1 vs2)
unify ge scope (VTblType p1 res1) (VTblType p2 res2) = do
  unify ge scope p1   p2
  unify ge scope res1 res2
unify ge scope (VMeta i env1 vs1) (VMeta j env2 vs2)
  | i  == j                    = sequence_ (zipWith (unify ge scope) vs1 vs2)
  | otherwise                  = do mv <- getMeta j
                                    case mv of
                                      Bound t2    -> do v2 <- liftErr (eval ge env2 t2)
                                                        unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2)
                                      Unbound _ _ -> setMeta i (Bound (Meta j))
unify ge scope (VInt i)       (VInt j)
  | i == j                     = return ()
unify ge scope (VMeta i env vs) v = unifyVar ge scope i env vs v
unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
unify ge scope v1 v2 = do
  t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
  t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
  tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ 
                                      ppTerm Unqualified 0 t2))

-- | Invariant: tv1 is a flexible type variable
unifyVar :: GlobalEnv -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
unifyVar ge scope i env vs ty2 = do            -- Check whether i is bound
  mv <- getMeta i
  case mv of
    Bound ty1       -> do v <- liftErr (eval ge env ty1)
                          unify ge scope (vapply (geLoc ge) v vs) ty2
    Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of
                          Left i     -> let (v,_) = reverse scope !! i
                                        in tcError ("Variable" <+> pp v <+> "has escaped")
                          Right ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
                                           if i `elem` ms2
                                             then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
                                                           nest 2 (ppTerm Unqualified 0 ty2'))
                                             else setMeta i (Bound ty2')

-----------------------------------------------------------------------
-- Instantiation and quantification
-----------------------------------------------------------------------

-- | Instantiate the topmost implicit arguments with metavariables
instantiate :: Scope -> Term -> Sigma -> TcM (Term,Rho)
instantiate scope t (VProd Implicit ty1 x (Bind ty2)) = do
  i <- newMeta scope ty1
  instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] []))
instantiate scope t ty = do
  return (t,ty)

-- | Build fresh lambda abstractions for the topmost implicit arguments
skolemise :: GlobalEnv -> Scope -> Sigma -> TcM (Scope, Term->Term, Rho)
skolemise ge scope ty@(VMeta i env vs) = do
  mv <- getMeta i
  case mv of
    Unbound _ _ -> return (scope,id,ty)                   -- guarded constant?
    Bound ty    -> do vty <- liftErr (eval ge env ty)
                      skolemise ge scope (vapply (geLoc ge) vty vs)
skolemise ge scope (VProd Implicit ty1 x (Bind ty2)) = do
  let v = newVar scope
  (scope,f,ty2) <- skolemise ge ((v,ty1):scope) (ty2 (VGen (length scope) []))
  return (scope,Abs Implicit v . f,ty2)
skolemise ge scope ty = do
  return (scope,id,ty)

-- | Quantify over the specified type variables (all flexible)
quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
quantify ge scope t tvs ty0 = do
  ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
  let used_bndrs = nub (bndrs ty)  -- Avoid quantified type variables in use
      new_bndrs  = take (length tvs) (allBinders \\ used_bndrs)
  mapM_ bind (tvs `zip` new_bndrs)   -- 'bind' is just a cunning way 
  ty <- zonkTerm ty                  -- of doing the substitution
  vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
  return (foldr (Abs Implicit) t new_bndrs,vty)
  where
    bind (i, name) = setMeta i (Bound (Vr name))

    bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1  ++ bndrs t2
    bndrs _                = []

allBinders :: [Ident]    -- a,b,..z, a1, b1,... z1, a2, b2,... 
allBinders = [ identS [x]          | x <- ['a'..'z'] ] ++
             [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']]


-----------------------------------------------------------------------
-- The Monad
-----------------------------------------------------------------------

type Scope = [(Ident,Value)]

type Sigma = Value
type Rho   = Value	-- No top-level ForAll
type Tau   = Value	-- No ForAlls anywhere

data MetaValue
  = Unbound Scope Sigma
  | Bound   Term
type MetaStore = IntMap.IntMap MetaValue
data TcResult a
  = TcOk   a MetaStore [Message]
  | TcFail             [Message] -- First msg is error, the rest are warnings?
newtype TcM a = TcM {unTcM :: MetaStore -> [Message] -> TcResult a}

instance Monad TcM where
  return x = TcM (\ms msgs -> TcOk x ms msgs)
  f >>= g  = TcM (\ms msgs -> case unTcM f ms msgs of
                                TcOk x ms msgs -> unTcM (g x) ms msgs
                                TcFail    msgs -> TcFail msgs)
  fail     = tcError . pp

instance Applicative TcM where
  pure = return
  (<*>) = ap

instance Functor TcM where
  fmap f g = TcM (\ms msgs -> case unTcM g ms msgs of
                           TcOk x ms msgs -> TcOk (f x) ms msgs
                           TcFail msgs    -> TcFail msgs)

instance ErrorMonad TcM where
  raise  = tcError . pp
  handle f g = TcM (\ms msgs -> case unTcM f ms msgs of
                                  TcFail (msg:msgs) -> unTcM (g (render msg)) ms msgs
                                  r                 -> r)

tcError :: Message -> TcM a
tcError msg = TcM (\ms msgs -> TcFail (msg : msgs))

tcWarn :: Message -> TcM ()
tcWarn msg = TcM (\ms msgs -> TcOk () ms (msg : msgs))

unimplemented str = fail ("Unimplemented: "++str)


runTcM :: TcM a -> Check a
runTcM f = case unTcM f IntMap.empty [] of
             TcOk x _ msgs -> do checkWarnings msgs; return x
             TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg

newMeta :: Scope -> Sigma -> TcM MetaId
newMeta scope ty = TcM (\ms msgs -> 
  let i = IntMap.size ms
  in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)

getMeta :: MetaId -> TcM MetaValue
getMeta i = TcM (\ms msgs -> 
  case IntMap.lookup i ms of
    Just mv -> TcOk mv ms msgs
    Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs))

setMeta :: MetaId -> MetaValue -> TcM ()
setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs)

newVar :: Scope -> Ident
newVar scope = head [x | i <- [1..], 
                         let x = identS ('v':show i),
                         isFree scope x]
  where
    isFree []            x = True
    isFree ((y,_):scope) x = x /= y && isFree scope x

scopeEnv   scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..]
scopeVars  scope = map fst scope
scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope)

-- | This function takes account of zonking, and returns a set
-- (no duplicates) of unbound meta-type variables
getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId]
getMetaVars loc sc_tys = do
  tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
  return (foldr go [] tys)
  where
    -- Get the MetaIds from a term; no duplicates in result
    go (Vr tv)    acc = acc 
    go (App x y)  acc = go x (go y acc)
    go (Meta i)   acc
	  | i `elem` acc  = acc
	  | otherwise	  = i : acc
    go (Q _)      acc = acc
    go (QC _)     acc = acc
    go (Sort _)   acc = acc
    go (Prod _ _ arg res) acc = go arg (go res acc)
    go (Table p t) acc = go p (go t acc)
    go (RecType rs) acc = foldl (\acc (l,ty) -> go ty acc) acc rs
    go t acc = unimplemented ("go "++show t)

-- | This function takes account of zonking, and returns a set
-- (no duplicates) of free type variables
getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident]
getFreeVars loc sc_tys = do
  tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
  return (foldr (go []) [] tys)
  where
    go bound (Vr tv)            acc 
	  | tv `elem` bound             = acc
	  | tv `elem` acc               = acc
	  | otherwise                   = tv : acc
    go bound (App x y)          acc = go bound x (go bound y acc)
    go bound (Meta _)           acc = acc
    go bound (Q _)              acc = acc
    go bound (QC _)             acc = acc
    go bound (Prod _ x arg res) acc = go bound arg (go (x : bound) res acc)
    go bound (RecType rs) acc = foldl (\acc (l,ty) -> go bound ty acc) acc rs
    go bound (Table p t)        acc = go bound p (go bound t acc)

-- | Eliminate any substitutions in a term
zonkTerm :: Term -> TcM Term
zonkTerm (Meta i) = do
  mv <- getMeta i
  case mv of
    Unbound _ _ -> return (Meta i)
    Bound t     -> do t <- zonkTerm t
                      setMeta i (Bound t)       -- "Short out" multiple hops
                      return t
zonkTerm t = composOp zonkTerm t

tc_value2term loc xs v =
  case value2term loc xs v of
    Left i  -> tcError ("Variable #" <+> pp i <+> "has escaped")
    Right t -> return t



data TcA x a 
  = TcSingle   (MetaStore -> [Message] -> TcResult a)
  | TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])])

mkTcA :: Err [a] -> TcA a a
mkTcA f = case f of
            Bad msg -> TcSingle  (\ms msgs -> TcFail (pp msg : msgs))
            Ok  [x] -> TcSingle  (\ms msgs -> TcOk x ms msgs)
            Ok  xs  -> TcMany xs (\ms msgs -> [(x,ms,msgs) | x <- xs])

singleTcA :: TcM a -> TcA x a
singleTcA = TcSingle . unTcM

bindTcA :: TcA x a -> (a -> TcM b) -> TcA x b
bindTcA f g = case f of
                TcSingle  f -> TcSingle (unTcM (TcM f >>= g))
                TcMany xs f -> TcMany xs (\ms msgs -> foldr add [] (f ms msgs))
  where
    add (y,ms,msgs) rs =
      case unTcM (g y) ms msgs of
        TcFail _       -> rs
        TcOk y ms msgs -> (y,ms,msgs):rs

runTcA :: ([x] -> TcM a) -> TcA x a -> TcM a
runTcA g f = TcM (\ms msgs -> case f of
                                TcMany xs f -> case f ms msgs of
                                                 [(x,ms,msgs)] -> TcOk x ms msgs
                                                 rs            -> unTcM (g xs) ms msgs
                                TcSingle f                     -> f ms msgs)