content: {-|
  Module      : Idris.Core.Typecheck
  Description : Idris' type checker.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  
  {-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances,
               MultiParamTypeClasses, PatternGuards #-}
  
  module Idris.Core.Typecheck where
  
  import Idris.Core.Evaluate
  import Idris.Core.TT
  
  import Control.Monad
  import Control.Monad.State
  
  -- To check conversion, normalise each term wrt the current environment.
  -- Since we haven't converted everything to de Bruijn indices yet, we'll have to
  -- deal with alpha conversion - we do this by making each inner term de Bruijn
  -- indexed with 'finalise'
  
  convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()
  convertsC ctxt env x y =
      do let hs = map fstEnv (filter isHole env)
         c1 <- convEq ctxt hs x y
         if c1 then return ()
           else
              do c2 <- convEq ctxt hs (finalise (normalise ctxt env x))
                           (finalise (normalise ctxt env y))
                 if c2 then return ()
                   else lift $ tfail (CantConvert
                               (finalise (normalise ctxt env x))
                               (finalise (normalise ctxt env y)) (errEnv env))
  
  converts :: Context -> Env -> Term -> Term -> TC ()
  converts ctxt env x y
       = let hs = map fstEnv (filter isHole env) in
         case convEq' ctxt hs x y of
            OK True -> return ()
            _ -> case convEq' ctxt hs (finalise (normalise ctxt env x))
                                      (finalise (normalise ctxt env y)) of
                  OK True -> return ()
                  _ -> tfail (CantConvert
                             (finalise (normalise ctxt env x))
                             (finalise (normalise ctxt env y)) (errEnv env))
  
  isHole (n, _, Hole _) = True
  isHole _ = False
  
  errEnv = map (\(x, _, b) -> (x, binderTy b))
  
  isType :: Context -> Env -> Term -> TC ()
  isType ctxt env tm = isType' (normalise ctxt env tm)
      where isType' tm | isUniverse tm = return ()
                       | otherwise = fail (showEnv env tm ++ " is not a Type")
  
  convType :: String -> Context -> Env -> Term -> StateT UCs TC ()
  convType tcns ctxt env tm =
      do (v, cs) <- get
         put (v + 1, cs)
         case normalise ctxt env tm of
              UType _ -> return ()
              _ -> convertsC ctxt env tm (TType (UVar tcns v))
  
  recheck :: String -> Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
  recheck = recheck_borrowing False []
  
  recheck_borrowing :: Bool -> [Name] -> String -> Context -> Env -> Raw -> Term ->
                       TC (Term, Type, UCs)
  recheck_borrowing uniq_check bs tcns ctxt env tm orig
     = let v = next_tvar ctxt in
         case runStateT (check' False tcns ctxt env tm) (v, []) of -- holes banned
            Error (IncompleteTerm _) -> Error $ IncompleteTerm orig
            Error e -> Error e
            OK ((tm, ty), constraints) ->
                do when uniq_check $ checkUnique bs ctxt env tm
                   return (tm, ty, constraints)
  
  check :: Context -> Env -> Raw -> TC (Term, Type)
  check ctxt env tm
       -- Holes allowed, so constraint namespace doesn't matter
       = evalStateT (check' True [] ctxt env tm) (0, [])
  
  check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
  check' holes tcns ctxt env top
     = do (tm, ty, _) <- chk Rig1 (TType (UVar tcns (-5))) Nothing env top
          return (tm, ty)
   where
  
    smaller (UType NullType) _ = UType NullType
    smaller _ (UType NullType) = UType NullType
    smaller (UType u)        _ = UType u
    smaller _        (UType u) = UType u
    smaller x        _         = x
  
    astate | holes = MaybeHoles
           | otherwise = Complete
  
    chk :: RigCount -> -- 'sigma' in Bob Atkey's QTT paper, except that
                 -- for implementation purposes it could be 0, 1 or omega when
                 -- checking variable usage.
           Type -> -- uniqueness level
           Maybe UExp -> -- universe for kind
           Env -> Raw -> StateT UCs TC (Term, Type, [Name])
    chk rigc u lvl env (Var n)
        | Just (i, erig, ty) <- lookupTyEnv n env
               = case rigSafe holes erig rigc n of
                      Nothing -> return (P Bound n ty, ty, used rigc n)
                      Just msg -> lift $ tfail $ Msg msg
        -- If we're elaborating, we don't want the private names; if we're
        -- checking an already elaborated term, we do
        | [P nt n' ty] <- lookupP_all (not holes) True n ctxt
               = return (P nt n' ty, ty, [])
  --       -- If the names are ambiguous, require it to be fully qualified
  --       | [P nt n' ty] <- lookupP_all (not holes) True n ctxt
  --              = return (P nt n' ty, ty, [])
        | otherwise = do lift $ tfail $ NoSuchVariable n
      where rigSafe True _    _    n = Nothing
            rigSafe _    Rig1 RigW n = Just ("Trying to use linear name " ++ show n ++ " in non-linear context")
            rigSafe _    Rig0 RigW n = Just ("Trying to use irrelevant name " ++ show n ++ " in relevant context")
            rigSafe _    Rig0 Rig1 n = Just ("Trying to use irrelevant name " ++ show n ++ " in relevant context")
            rigSafe _    _    _    n = Nothing
  
            used Rig0 n = []
            used _ n = [n]
  
    chk rigc u lvl env ap@(RApp f RType) | not holes
      -- special case to reduce constraintss
        = do (fv, fty, fns) <- chk rigc u Nothing env f
             let fty' = case uniqueBinders (map fstEnv env) (finalise fty) of
                          ty@(Bind x (Pi _ i s k) t) -> ty
                          _ -> uniqueBinders (map fstEnv env)
                                   $ case normalise ctxt env fty of
                                       ty@(Bind x (Pi _ i s k) t) -> ty
                                       _ -> normalise ctxt env fty
             case fty' of
               Bind x (Pi rig i (TType v') k) t ->
                 do (v, cs) <- get
                    put (v+1, ULT (UVar tcns v) v' : cs)
                    let apty = simplify initContext env
                                   (Bind x (Let rig (TType v') (TType (UVar tcns v))) t)
                    return (App Complete fv (TType (UVar tcns v)), apty, fns)
               Bind x (Pi rig i s k) t ->
                   do (av, aty, _) <- chk rigc u Nothing env RType
                      convertsC ctxt env aty s
                      let apty = simplify initContext env
                                          (Bind x (Let rig aty av) t)
                      return (App astate fv av, apty, fns)
               t -> lift $ tfail $ NonFunctionType fv fty
    chk rigc u lvl env ap@(RApp f a)
        = do (fv, fty, fns) <- chk rigc u Nothing env f
             let (rigf, fty') =
                     case uniqueBinders (map fstEnv env) (finalise fty) of
                          ty@(Bind x (Pi rig i s k) t) -> (rig, ty)
                          _ -> case normalise ctxt env fty of
                                    ty@(Bind x (Pi rig i s k) t) ->
                                       (rig, uniqueBinders (map fstEnv env) ty)
                                    _ -> (RigW, uniqueBinders (map fstEnv env)
                                                      (normalise ctxt env fty)) -- This is an error, caught below...
             (av, aty, ans_in) <- chk (rigMult rigf rigc) u Nothing env a
             -- usage in 'a' doesn't count if the binder has multiplicity 0
             let ans = case rigf of
                            Rig0 -> []
                            _ -> ans_in
             case fty' of
               Bind x (Pi rig i s k) t ->
                   do convertsC ctxt env aty s
                      let apty = simplify initContext env
                                          (Bind x (Let rig aty av) t)
                      return (App astate fv av, apty, fns ++ ans)
               t -> lift $ tfail $ NonFunctionType fv fty
    chk rigc u lvl env RType
      | holes = return (TType (UVal 0), TType (UVal 0), [])
      | otherwise = do (v, cs) <- get
                       let c = ULT (UVar tcns v) (UVar tcns (v+1))
                       put (v+2, (c:cs))
                       return (TType (UVar tcns v), TType (UVar tcns (v+1)), [])
    chk rigc u lvl env (RUType un)
      | holes = return (UType un, TType (UVal 0), [])
      | otherwise = do -- TODO! Issue #1715 on the issue tracker.
                       -- https://github.com/idris-lang/Idris-dev/issues/1715
                       -- (v, cs) <- get
                       -- let c = ULT (UVar v) (UVar (v+1))
                       -- put (v+2, (c:cs))
                       -- return (TType (UVar v), TType (UVar (v+1)))
                       return (UType un, TType (UVal 0), [])
    chk rigc u lvl env (RConstant Forgot) = return (Erased, Erased, [])
    chk rigc u lvl env (RConstant c) = return (Constant c, constType c, [])
      where constType (I _)   = Constant (AType (ATInt ITNative))
            constType (BI _)  = Constant (AType (ATInt ITBig))
            constType (Fl _)  = Constant (AType ATFloat)
            constType (Ch _)  = Constant (AType (ATInt ITChar))
            constType (Str _) = Constant StrType
            constType (B8 _)  = Constant (AType (ATInt (ITFixed IT8)))
            constType (B16 _) = Constant (AType (ATInt (ITFixed IT16)))
            constType (B32 _) = Constant (AType (ATInt (ITFixed IT32)))
            constType (B64 _) = Constant (AType (ATInt (ITFixed IT64)))
            constType TheWorld = Constant WorldType
            constType Forgot  = Erased
            constType _       = TType (UVal 0)
    chk rigc u lvl env (RBind n (Pi rig i s k) t)
        = do (sv, st, sns) <- chk Rig0 u Nothing (envZero env) s
             (v, cs) <- get
             (kv, kt, _) <- chk Rig0 u Nothing (envZero env) k -- no need to validate these constraints, they are independent
             put (v+1, cs)
             let maxu = case lvl of
                             Nothing -> UVar tcns v
                             Just v' -> v'
             (tv, tt, tns) <- chk Rig0 st (Just maxu) ((n, Rig0, Pi Rig0 i sv kv) : envZero env) t
  
             case (normalise ctxt env st, normalise ctxt env tt) of
                  (TType su, TType tu) -> do
                      when (not holes) $ do (v, cs) <- get
                                            put (v, ULE su maxu :
                                                    ULE tu maxu : cs)
                      let k' = TType (UVar tcns v) `smaller` st `smaller` kv `smaller` u
                      return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')
                                (pToV n tv), k', sns ++ tns)
                  (un, un') ->
                     let k' = st `smaller` kv `smaller` un `smaller` un' `smaller` u in
                      return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')
                                  (pToV n tv), k', sns ++ tns)
  
    chk rigc_in u lvl env (RBind n b sc)
        = do (b', bt', bns) <- checkBinder b
             (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc
             checkUsageOK (getCount b) scns
             discharge n b' bt' (pToV n scv) (pToV n sct) (bns ++ scns)
      where -- should only check at 0 or 1 (as in Bob's paper) but rigc_in
            -- might be RigW, since that's how we check in the Var rule that
            -- a linearly bound name is only used in a linear context.
            -- So, here, check the scope at multiplicity 1
            rigc = case rigc_in of
                        Rig0 -> Rig0
                        _ -> Rig1
            getCount (Pi rig _ _ _) = rigMult rigc rig
            getCount (PVar rig _) = rigMult rigc rig
            getCount (Lam rig _) = rigMult rigc rig
            getCount (Let rig _ _) = rigMult rigc rig
            getCount _ = rigMult rigc RigW
  
            checkUsageOK Rig0 _ = return ()
            checkUsageOK RigW _ = return ()
            checkUsageOK Rig1 ns
                = let used = length (filter (==n) ns) in
                      if used == 1 then return ()
                         else lift $ tfail $ Msg $ "There are " ++ (show used) ++
                                " uses of linear name " ++ show n
  
            checkBinder (Lam rig t)
              = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                   convType tcns ctxt env tt
                   return (Lam rig tv, tt, [])
            checkBinder (Let rig t v)
              = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                   (vv, vt, vns) <- chk (rigMult rig rigc) u Nothing env v
                   convertsC ctxt env vt tv
                   convType tcns ctxt env tt
                   return (Let rig tv vv, tt, vns)
            checkBinder (NLet t v)
              = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                   (vv, vt, vns) <- chk rigc u Nothing env v
                   convertsC ctxt env vt tv
                   convType tcns ctxt env tt
                   return (NLet tv vv, tt, vns)
            checkBinder (Hole t)
              | not holes = lift $ tfail (IncompleteTerm undefined)
              | otherwise
                     = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                          convType tcns ctxt env tt
                          return (Hole tv, tt, [])
            checkBinder (GHole i ns t)
              = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                   convType tcns ctxt env tt
                   return (GHole i ns tv, tt, [])
            checkBinder (Guess t v)
              | not holes = lift $ tfail (IncompleteTerm undefined)
              | otherwise
                     = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                          (vv, vt, vns) <- chk rigc u Nothing env v
                          convertsC ctxt env vt tv
                          convType tcns ctxt env tt
                          return (Guess tv vv, tt, vns)
            checkBinder (PVar rig t)
              = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                   convType tcns ctxt env tt
                   return (PVar rig tv, tt, [])
            checkBinder (PVTy t)
              = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                   convType tcns ctxt env tt
                   return (PVTy tv, tt, [])
  
            discharge n (Lam r t) bt scv sct ns
              = return (Bind n (Lam r t) scv, Bind n (Pi r Nothing t bt) sct, ns)
            discharge n (Pi r i t k) bt scv sct ns
              = return (Bind n (Pi r i t k) scv, sct, ns)
            discharge n (Let r t v) bt scv sct ns
              = return (Bind n (Let r t v) scv, Bind n (Let r t v) sct, ns)
            discharge n (NLet t v) bt scv sct ns
              = return (Bind n (NLet t v) scv, Bind n (Let RigW t v) sct, ns)
            discharge n (Hole t) bt scv sct ns
              = return (Bind n (Hole t) scv, sct, ns)
            discharge n (GHole i ns t) bt scv sct uns
              = return (Bind n (GHole i ns t) scv, sct, uns)
            discharge n (Guess t v) bt scv sct ns
              = return (Bind n (Guess t v) scv, sct, ns)
            discharge n (PVar r t) bt scv sct ns
              = return (Bind n (PVar r t) scv, Bind n (PVTy t) sct, ns)
            discharge n (PVTy t) bt scv sct ns
              = return (Bind n (PVTy t) scv, sct, ns)
  
  -- Number of times a name can be used
  data UniqueUse = Never -- no more times
                 | Once -- at most once more
                 | LendOnly -- only under 'lend'
                 | Many -- unlimited
    deriving Eq
  
  -- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears
  -- in the scope more than once, this is an error.
  checkUnique :: [Name] -> Context -> Env -> Term -> TC ()
  checkUnique borrowed ctxt env tm
           = evalStateT (chkBinders env (explicitNames tm)) []
    where
      isVar (P _ _ _) = True
      isVar (V _) = True
      isVar _ = False
  
      chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
      chkBinders env (V i) | length env > i = chkName (fstEnv (env!!i))
      chkBinders env (P _ n _) = chkName n
      -- 'lending' a unique or nulltype variable doesn't count as a use,
      -- but we still can't lend something that's already been used.
      chkBinders env (App _ (App _ (P _ (NS (UN lend) [owner]) _) t) a)
         | isVar a && owner == txt "Ownership" &&
           (lend == txt "lend" || lend == txt "Read")
              = do chkBinders env t -- Check the type normally
                   st <- get
                   -- Remove the 'LendOnly' names from the unusable set
                   put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)
                   chkBinders env a
                   put st -- Reset the old state after checking the argument
      chkBinders env (App _ f a) = do chkBinders env f; chkBinders env a
      chkBinders env (Bind n b t)
         = do chkBinderName env n b
              st <- get
              case b of
                   Let _ t v -> chkBinders env v
                   _ -> return ()
              chkBinders ((n, Rig0, b) : env) t
      chkBinders env t = return ()
  
      chkBinderName :: Env -> Name -> Binder Term ->
                       StateT [(Name, (UniqueUse, Universe))] TC ()
      chkBinderName env n b
         = do let rawty = forgetEnv (map fstEnv env) (binderTy b)
              (_, kind) <- lift $ check ctxt env rawty
              case kind of
                   UType UniqueType -> do ns <- get
                                          if n `elem` borrowed
                                             then put ((n, (LendOnly, NullType)) : ns)
                                             else put ((n, (Once, UniqueType)) : ns)
                   UType NullType -> do ns <- get
                                        put ((n, (Many, NullType)) : ns)
                   UType AllTypes -> do ns <- get
                                        put ((n, (Once, AllTypes)) : ns)
                   _ -> return ()
  
      chkName n
         = do ns <- get
              case lookup n ns of
                   Nothing -> return ()
                   Just (Many, k) -> return ()
                   Just (Never, k) -> lift $ tfail (UniqueError k n)
                   Just (LendOnly, k) -> lift $ tfail (UniqueError k n)
                   Just (Once, k) -> put ((n, (Never, k)) :
                                                filter (\x -> fst x /= n) ns)
  