{-|
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 :: Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC Context
ctxt Env
env Term
x Term
y =
    do let hs :: [Name]
hs = ((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv (((Name, RigCount, Binder Term) -> Bool) -> Env -> Env
forall a. (a -> Bool) -> [a] -> [a]
filter (Name, RigCount, Binder Term) -> Bool
forall {a} {b} {b}. (a, b, Binder b) -> Bool
isHole Env
env)
       Bool
c1 <- Context -> [Name] -> Term -> Term -> StateT UCs TC Bool
convEq Context
ctxt [Name]
hs Term
x Term
y
       if Bool
c1 then () -> StateT UCs TC ()
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         else
            do Bool
c2 <- Context -> [Name] -> Term -> Term -> StateT UCs TC Bool
convEq Context
ctxt [Name]
hs (Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
x))
                         (Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
y))
               if Bool
c2 then () -> StateT UCs TC ()
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 else TC () -> StateT UCs TC ()
forall (m :: * -> *) a. Monad m => m a -> StateT UCs m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> StateT UCs TC ()) -> TC () -> StateT UCs TC ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Term -> Term -> [(Name, Term)] -> Err
forall t. t -> t -> [(Name, t)] -> Err' t
CantConvert
                             (Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
x))
                             (Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
y)) (Env -> [(Name, Term)]
forall {a} {b} {b}. [(a, b, Binder b)] -> [(a, b)]
errEnv Env
env))

converts :: Context -> Env -> Term -> Term -> TC ()
converts :: Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt Env
env Term
x Term
y
     = let hs :: [Name]
hs = ((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv (((Name, RigCount, Binder Term) -> Bool) -> Env -> Env
forall a. (a -> Bool) -> [a] -> [a]
filter (Name, RigCount, Binder Term) -> Bool
forall {a} {b} {b}. (a, b, Binder b) -> Bool
isHole Env
env) in
       case Context -> [Name] -> Term -> Term -> TC Bool
convEq' Context
ctxt [Name]
hs Term
x Term
y of
          OK Bool
True -> () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          TC Bool
_ -> case Context -> [Name] -> Term -> Term -> TC Bool
convEq' Context
ctxt [Name]
hs (Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
x))
                                    (Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
y)) of
                OK Bool
True -> () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                TC Bool
_ -> Err -> TC ()
forall a. Err -> TC a
tfail (Term -> Term -> [(Name, Term)] -> Err
forall t. t -> t -> [(Name, t)] -> Err' t
CantConvert
                           (Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
x))
                           (Term -> Term
forall n. Eq n => TT n -> TT n
finalise (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
y)) (Env -> [(Name, Term)]
forall {a} {b} {b}. [(a, b, Binder b)] -> [(a, b)]
errEnv Env
env))

isHole :: (a, b, Binder b) -> Bool
isHole (a
n, b
_, Hole b
_) = Bool
True
isHole (a, b, Binder b)
_ = Bool
False

errEnv :: [(a, b, Binder b)] -> [(a, b)]
errEnv = ((a, b, Binder b) -> (a, b)) -> [(a, b, Binder b)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(a
x, b
_, Binder b
b) -> (a
x, Binder b -> b
forall b. Binder b -> b
binderTy Binder b
b))

isType :: Context -> Env -> Term -> TC ()
isType :: Context -> Env -> Term -> TC ()
isType Context
ctxt Env
env Term
tm = Term -> TC ()
forall {m :: * -> *}. MonadFail m => Term -> m ()
isType' (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
tm)
    where isType' :: Term -> m ()
isType' Term
tm | Term -> Bool
isUniverse Term
tm = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                     | Bool
otherwise = String -> m ()
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (Env -> Term -> String
forall n. (Eq n, Show n) => EnvTT n -> TT n -> String
showEnv Env
env Term
tm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not a Type")

convType :: String -> Context -> Env -> Term -> StateT UCs TC ()
convType :: String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tm =
    do (Int
v, [UConstraint]
cs) <- StateT UCs TC UCs
forall s (m :: * -> *). MonadState s m => m s
get
       UCs -> StateT UCs TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, [UConstraint]
cs)
       case Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
tm of
            UType Universe
_ -> () -> StateT UCs TC ()
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Term
_ -> Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC Context
ctxt Env
env Term
tm (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar String
tcns Int
v))

recheck :: String -> Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
recheck :: String -> Context -> Env -> Raw -> Term -> TC (Term, Term, UCs)
recheck = Bool
-> [Name]
-> String
-> Context
-> Env
-> Raw
-> Term
-> TC (Term, Term, UCs)
recheck_borrowing Bool
False []

recheck_borrowing :: Bool -> [Name] -> String -> Context -> Env -> Raw -> Term ->
                     TC (Term, Type, UCs)
recheck_borrowing :: Bool
-> [Name]
-> String
-> Context
-> Env
-> Raw
-> Term
-> TC (Term, Term, UCs)
recheck_borrowing Bool
uniq_check [Name]
bs String
tcns Context
ctxt Env
env Raw
tm Term
orig
   = let v :: Int
v = Context -> Int
next_tvar Context
ctxt in
       case StateT UCs TC (Term, Term) -> UCs -> TC ((Term, Term), UCs)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Bool
-> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Term)
check' Bool
False String
tcns Context
ctxt Env
env Raw
tm) (Int
v, []) of -- holes banned
          Error (IncompleteTerm Term
_) -> Err -> TC (Term, Term, UCs)
forall a. Err -> TC a
Error (Err -> TC (Term, Term, UCs)) -> Err -> TC (Term, Term, UCs)
forall a b. (a -> b) -> a -> b
$ Term -> Err
forall t. t -> Err' t
IncompleteTerm Term
orig
          Error Err
e -> Err -> TC (Term, Term, UCs)
forall a. Err -> TC a
Error Err
e
          OK ((Term
tm, Term
ty), UCs
constraints) ->
              do Bool -> TC () -> TC ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
uniq_check (TC () -> TC ()) -> TC () -> TC ()
forall a b. (a -> b) -> a -> b
$ [Name] -> Context -> Env -> Term -> TC ()
checkUnique [Name]
bs Context
ctxt Env
env Term
tm
                 (Term, Term, UCs) -> TC (Term, Term, UCs)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, Term
ty, UCs
constraints)

check :: Context -> Env -> Raw -> TC (Term, Type)
check :: Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
tm
     -- Holes allowed, so constraint namespace doesn't matter
     = StateT UCs TC (Term, Term) -> UCs -> TC (Term, Term)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Bool
-> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Term)
check' Bool
True [] Context
ctxt Env
env Raw
tm) (Int
0, [])

check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
check' :: Bool
-> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Term)
check' Bool
holes String
tcns Context
ctxt Env
env Raw
top
   = do (Term
tm, Term
ty, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig1 (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar String
tcns (-Int
5))) Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
top
        (Term, Term) -> StateT UCs TC (Term, Term)
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, Term
ty)
 where

  smaller :: TT n -> TT n -> TT n
smaller (UType Universe
NullType) TT n
_ = Universe -> TT n
forall n. Universe -> TT n
UType Universe
NullType
  smaller TT n
_ (UType Universe
NullType) = Universe -> TT n
forall n. Universe -> TT n
UType Universe
NullType
  smaller (UType Universe
u)        TT n
_ = Universe -> TT n
forall n. Universe -> TT n
UType Universe
u
  smaller TT n
_        (UType Universe
u) = Universe -> TT n
forall n. Universe -> TT n
UType Universe
u
  smaller TT n
x        TT n
_         = TT n
x

  astate :: AppStatus n
astate | Bool
holes = AppStatus n
forall n. AppStatus n
MaybeHoles
         | Bool
otherwise = AppStatus n
forall n. AppStatus n
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 :: RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
rigc Term
u Maybe UExp
lvl Env
env (Var Name
n)
      | Just (Int
i, RigCount
erig, Term
ty) <- Name -> Env -> Maybe (Int, RigCount, Term)
lookupTyEnv Name
n Env
env
             = case Bool -> RigCount -> RigCount -> Name -> Maybe String
forall {a}.
Show a =>
Bool -> RigCount -> RigCount -> a -> Maybe String
rigSafe Bool
holes RigCount
erig RigCount
rigc Name
n of
                    Maybe String
Nothing -> (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Term
ty, Term
ty, RigCount -> Name -> [Name]
forall {a}. RigCount -> a -> [a]
used RigCount
rigc Name
n)
                    Just String
msg -> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall (m :: * -> *) a. Monad m => m a -> StateT UCs m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name]))
-> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Err -> TC (Term, Term, [Name])
forall a. Err -> TC a
tfail (Err -> TC (Term, Term, [Name])) -> Err -> TC (Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg String
msg
      -- If we're elaborating, we don't want the private names; if we're
      -- checking an already elaborated term, we do
      | [P NameType
nt Name
n' Term
ty] <- Bool -> Bool -> Name -> Context -> [Term]
lookupP_all (Bool -> Bool
not Bool
holes) Bool
True Name
n Context
ctxt
             = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n' Term
ty, Term
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, [])
      | Bool
otherwise = do TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall (m :: * -> *) a. Monad m => m a -> StateT UCs m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name]))
-> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Err -> TC (Term, Term, [Name])
forall a. Err -> TC a
tfail (Err -> TC (Term, Term, [Name])) -> Err -> TC (Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Name -> Err
forall t. Name -> Err' t
NoSuchVariable Name
n
    where rigSafe :: Bool -> RigCount -> RigCount -> a -> Maybe String
rigSafe Bool
True RigCount
_    RigCount
_    a
n = Maybe String
forall a. Maybe a
Nothing
          rigSafe Bool
_    RigCount
Rig1 RigCount
RigW a
n = String -> Maybe String
forall a. a -> Maybe a
Just (String
"Trying to use linear name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in non-linear context")
          rigSafe Bool
_    RigCount
Rig0 RigCount
RigW a
n = String -> Maybe String
forall a. a -> Maybe a
Just (String
"Trying to use irrelevant name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in relevant context")
          rigSafe Bool
_    RigCount
Rig0 RigCount
Rig1 a
n = String -> Maybe String
forall a. a -> Maybe a
Just (String
"Trying to use irrelevant name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in relevant context")
          rigSafe Bool
_    RigCount
_    RigCount
_    a
n = Maybe String
forall a. Maybe a
Nothing

          used :: RigCount -> a -> [a]
used RigCount
Rig0 a
n = []
          used RigCount
_ a
n = [a
n]

  chk RigCount
rigc Term
u Maybe UExp
lvl Env
env ap :: Raw
ap@(RApp Raw
f Raw
RType) | Bool -> Bool
not Bool
holes
    -- special case to reduce constraintss
      = do (Term
fv, Term
fty, [Name]
fns) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
rigc Term
u Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
f
           let fty' :: Term
fty' = case [Name] -> Term -> Term
uniqueBinders (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) (Term -> Term
forall n. Eq n => TT n -> TT n
finalise Term
fty) of
                        ty :: Term
ty@(Bind Name
x (Pi RigCount
_ Maybe ImplicitInfo
i Term
s Term
k) Term
t) -> Term
ty
                        Term
_ -> [Name] -> Term -> Term
uniqueBinders (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env)
                                 (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ case Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
fty of
                                     ty :: Term
ty@(Bind Name
x (Pi RigCount
_ Maybe ImplicitInfo
i Term
s Term
k) Term
t) -> Term
ty
                                     Term
_ -> Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
fty
           case Term
fty' of
             Bind Name
x (Pi RigCount
rig Maybe ImplicitInfo
i (TType UExp
v') Term
k) Term
t ->
               do (Int
v, [UConstraint]
cs) <- StateT UCs TC UCs
forall s (m :: * -> *). MonadState s m => m s
get
                  UCs -> StateT UCs TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, UExp -> UExp -> UConstraint
ULT (String -> Int -> UExp
UVar String
tcns Int
v) UExp
v' UConstraint -> [UConstraint] -> [UConstraint]
forall a. a -> [a] -> [a]
: [UConstraint]
cs)
                  let apty :: Term
apty = Context -> Env -> Term -> Term
simplify Context
initContext Env
env
                                 (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig (UExp -> Term
forall n. UExp -> TT n
TType UExp
v') (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar String
tcns Int
v))) Term
t)
                  (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete Term
fv (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar String
tcns Int
v)), Term
apty, [Name]
fns)
             Bind Name
x (Pi RigCount
rig Maybe ImplicitInfo
i Term
s Term
k) Term
t ->
                 do (Term
av, Term
aty, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
rigc Term
u Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
RType
                    Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC Context
ctxt Env
env Term
aty Term
s
                    let apty :: Term
apty = Context -> Env -> Term -> Term
simplify Context
initContext Env
env
                                        (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Term
aty Term
av) Term
t)
                    (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
astate Term
fv Term
av, Term
apty, [Name]
fns)
             Term
t -> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall (m :: * -> *) a. Monad m => m a -> StateT UCs m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name]))
-> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Err -> TC (Term, Term, [Name])
forall a. Err -> TC a
tfail (Err -> TC (Term, Term, [Name])) -> Err -> TC (Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Err
forall t. t -> t -> Err' t
NonFunctionType Term
fv Term
fty
  chk RigCount
rigc Term
u Maybe UExp
lvl Env
env ap :: Raw
ap@(RApp Raw
f Raw
a)
      = do (Term
fv, Term
fty, [Name]
fns) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
rigc Term
u Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
f
           let (RigCount
rigf, Term
fty') =
                   case [Name] -> Term -> Term
uniqueBinders (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) (Term -> Term
forall n. Eq n => TT n -> TT n
finalise Term
fty) of
                        ty :: Term
ty@(Bind Name
x (Pi RigCount
rig Maybe ImplicitInfo
i Term
s Term
k) Term
t) -> (RigCount
rig, Term
ty)
                        Term
_ -> case Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
fty of
                                  ty :: Term
ty@(Bind Name
x (Pi RigCount
rig Maybe ImplicitInfo
i Term
s Term
k) Term
t) ->
                                     (RigCount
rig, [Name] -> Term -> Term
uniqueBinders (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) Term
ty)
                                  Term
_ -> (RigCount
RigW, [Name] -> Term -> Term
uniqueBinders (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env)
                                                    (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
fty)) -- This is an error, caught below...
           (Term
av, Term
aty, [Name]
ans_in) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk (RigCount -> RigCount -> RigCount
rigMult RigCount
rigf RigCount
rigc) Term
u Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
a
           -- usage in 'a' doesn't count if the binder has multiplicity 0
           let ans :: [Name]
ans = case RigCount
rigf of
                          RigCount
Rig0 -> []
                          RigCount
_ -> [Name]
ans_in
           case Term
fty' of
             Bind Name
x (Pi RigCount
rig Maybe ImplicitInfo
i Term
s Term
k) Term
t ->
                 do Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC Context
ctxt Env
env Term
aty Term
s
                    let apty :: Term
apty = Context -> Env -> Term -> Term
simplify Context
initContext Env
env
                                        (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Term
aty Term
av) Term
t)
                    (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
astate Term
fv Term
av, Term
apty, [Name]
fns [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
ans)
             Term
t -> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall (m :: * -> *) a. Monad m => m a -> StateT UCs m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name]))
-> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Err -> TC (Term, Term, [Name])
forall a. Err -> TC a
tfail (Err -> TC (Term, Term, [Name])) -> Err -> TC (Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Err
forall t. t -> t -> Err' t
NonFunctionType Term
fv Term
fty
  chk RigCount
rigc Term
u Maybe UExp
lvl Env
env Raw
RType
    | Bool
holes = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> Term
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0), UExp -> Term
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0), [])
    | Bool
otherwise = do (Int
v, [UConstraint]
cs) <- StateT UCs TC UCs
forall s (m :: * -> *). MonadState s m => m s
get
                     let c :: UConstraint
c = UExp -> UExp -> UConstraint
ULT (String -> Int -> UExp
UVar String
tcns Int
v) (String -> Int -> UExp
UVar String
tcns (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1))
                     UCs -> StateT UCs TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2, (UConstraint
cUConstraint -> [UConstraint] -> [UConstraint]
forall a. a -> [a] -> [a]
:[UConstraint]
cs))
                     (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar String
tcns Int
v), UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar String
tcns (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)), [])
  chk RigCount
rigc Term
u Maybe UExp
lvl Env
env (RUType Universe
un)
    | Bool
holes = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> Term
forall n. Universe -> TT n
UType Universe
un, UExp -> Term
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0), [])
    | Bool
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)))
                     (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> Term
forall n. Universe -> TT n
UType Universe
un, UExp -> Term
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0), [])
  chk RigCount
rigc Term
u Maybe UExp
lvl Env
env (RConstant Const
Forgot) = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
forall n. TT n
Erased, Term
forall n. TT n
Erased, [])
  chk RigCount
rigc Term
u Maybe UExp
lvl Env
env (RConstant Const
c) = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> Term
forall n. Const -> TT n
Constant Const
c, Const -> Term
forall n. Const -> TT n
constType Const
c, [])
    where constType :: Const -> TT n
constType (I Int
_)   = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative))
          constType (BI Integer
_)  = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig))
          constType (Fl Double
_)  = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType ArithTy
ATFloat)
          constType (Ch Char
_)  = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITChar))
          constType (Str String
_) = Const -> TT n
forall n. Const -> TT n
Constant Const
StrType
          constType (B8 Word8
_)  = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT8)))
          constType (B16 Word16
_) = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT16)))
          constType (B32 Word32
_) = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT32)))
          constType (B64 Word64
_) = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)))
          constType Const
TheWorld = Const -> TT n
forall n. Const -> TT n
Constant Const
WorldType
          constType Const
Forgot  = TT n
forall n. TT n
Erased
          constType Const
_       = UExp -> TT n
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0)
  chk RigCount
rigc Term
u Maybe UExp
lvl Env
env (RBind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Raw
s Raw
k) Raw
t)
      = do (Term
sv, Term
st, [Name]
sns) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
s
           (Int
v, [UConstraint]
cs) <- StateT UCs TC UCs
forall s (m :: * -> *). MonadState s m => m s
get
           (Term
kv, Term
kt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
k -- no need to validate these constraints, they are independent
           UCs -> StateT UCs TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
vInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, [UConstraint]
cs)
           let maxu :: UExp
maxu = case Maybe UExp
lvl of
                           Maybe UExp
Nothing -> String -> Int -> UExp
UVar String
tcns Int
v
                           Just UExp
v' -> UExp
v'
           (Term
tv, Term
tt, [Name]
tns) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
st (UExp -> Maybe UExp
forall a. a -> Maybe a
Just UExp
maxu) ((Name
n, RigCount
Rig0, RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
Rig0 Maybe ImplicitInfo
i Term
sv Term
kv) (Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
: Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t

           case (Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
st, Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
tt) of
                (TType UExp
su, TType UExp
tu) -> do
                    Bool -> StateT UCs TC () -> StateT UCs TC ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
holes) (StateT UCs TC () -> StateT UCs TC ())
-> StateT UCs TC () -> StateT UCs TC ()
forall a b. (a -> b) -> a -> b
$ do (Int
v, [UConstraint]
cs) <- StateT UCs TC UCs
forall s (m :: * -> *). MonadState s m => m s
get
                                          UCs -> StateT UCs TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int
v, UExp -> UExp -> UConstraint
ULE UExp
su UExp
maxu UConstraint -> [UConstraint] -> [UConstraint]
forall a. a -> [a] -> [a]
:
                                                  UExp -> UExp -> UConstraint
ULE UExp
tu UExp
maxu UConstraint -> [UConstraint] -> [UConstraint]
forall a. a -> [a] -> [a]
: [UConstraint]
cs)
                    let k' :: TT n
k' = UExp -> TT n
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar String
tcns Int
v) TT n -> Term -> TT n
forall {n} {n}. TT n -> TT n -> TT n
`smaller` Term
st TT n -> Term -> TT n
forall {n} {n}. TT n -> TT n -> TT n
`smaller` Term
kv TT n -> Term -> TT n
forall {n} {n}. TT n -> TT n -> TT n
`smaller` Term
u
                    (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i ([Name] -> Term -> Term
uniqueBinders (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) Term
sv) Term
forall n. TT n
k')
                              (Name -> Term -> Term
forall n. Eq n => n -> TT n -> TT n
pToV Name
n Term
tv), Term
forall n. TT n
k', [Name]
sns [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
tns)
                (Term
un, Term
un') ->
                   let k' :: Term
k' = Term
st Term -> Term -> Term
forall {n} {n}. TT n -> TT n -> TT n
`smaller` Term
kv Term -> Term -> Term
forall {n} {n}. TT n -> TT n -> TT n
`smaller` Term
un Term -> Term -> Term
forall {n} {n}. TT n -> TT n -> TT n
`smaller` Term
un' Term -> Term -> Term
forall {n} {n}. TT n -> TT n -> TT n
`smaller` Term
u in
                    (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i ([Name] -> Term -> Term
uniqueBinders (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) Term
sv) Term
k')
                                (Name -> Term -> Term
forall n. Eq n => n -> TT n -> TT n
pToV Name
n Term
tv), Term
k', [Name]
sns [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
tns)

  chk RigCount
rigc_in Term
u Maybe UExp
lvl Env
env (RBind Name
n Binder Raw
b Raw
sc)
      = do (Binder Term
b', Term
bt', [Name]
bns) <- Binder Raw -> StateT UCs TC (Binder Term, Term, [Name])
checkBinder Binder Raw
b
           (Term
scv, Term
sct, [Name]
scns) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
rigc (Term -> Term -> Term
forall {n} {n}. TT n -> TT n -> TT n
smaller Term
bt' Term
u) Maybe UExp
forall a. Maybe a
Nothing ((Name
n, Binder Raw -> RigCount
forall {b}. Binder b -> RigCount
getCount Binder Raw
b, Binder Term
b')(Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Raw
sc
           RigCount -> [Name] -> StateT UCs TC ()
forall {t :: (* -> *) -> * -> *}.
(Monad (t TC), MonadTrans t) =>
RigCount -> [Name] -> t TC ()
checkUsageOK (Binder Raw -> RigCount
forall {b}. Binder b -> RigCount
getCount Binder Raw
b) [Name]
scns
           Name
-> Binder Term
-> Term
-> Term
-> Term
-> [Name]
-> StateT UCs TC (Term, Term, [Name])
forall {m :: * -> *} {n} {c}.
Monad m =>
n
-> Binder (TT n) -> TT n -> TT n -> TT n -> c -> m (TT n, TT n, c)
discharge Name
n Binder Term
b' Term
bt' (Name -> Term -> Term
forall n. Eq n => n -> TT n -> TT n
pToV Name
n Term
scv) (Name -> Term -> Term
forall n. Eq n => n -> TT n -> TT n
pToV Name
n Term
sct) ([Name]
bns [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
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 :: RigCount
rigc = case RigCount
rigc_in of
                      RigCount
Rig0 -> RigCount
Rig0
                      RigCount
_ -> RigCount
Rig1
          getCount :: Binder b -> RigCount
getCount (Pi RigCount
rig Maybe ImplicitInfo
_ b
_ b
_) = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
rig
          getCount (PVar RigCount
rig b
_) = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
rig
          getCount (Lam RigCount
rig b
_) = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
rig
          getCount (Let RigCount
rig b
_ b
_) = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
rig
          getCount Binder b
_ = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
RigW

          checkUsageOK :: RigCount -> [Name] -> t TC ()
checkUsageOK RigCount
Rig0 [Name]
_ = () -> t TC ()
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          checkUsageOK RigCount
RigW [Name]
_ = () -> t TC ()
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          checkUsageOK RigCount
Rig1 [Name]
ns
              = let used :: Int
used = [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==Name
n) [Name]
ns) in
                    if Int
used Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then () -> t TC ()
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                       else TC () -> t TC ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> t TC ()) -> TC () -> t TC ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> Err -> TC ()
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> String -> Err
forall a b. (a -> b) -> a -> b
$ String
"There are " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int -> String
forall a. Show a => a -> String
show Int
used) String -> String -> String
forall a. [a] -> [a] -> [a]
++
                              String
" uses of linear name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n

          checkBinder :: Binder Raw -> StateT UCs TC (Binder Term, Term, [Name])
checkBinder (Lam RigCount
rig Raw
t)
            = do (Term
tv, Term
tt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t
                 String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tt
                 (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
Lam RigCount
rig Term
tv, Term
tt, [])
          checkBinder (Let RigCount
rig Raw
t Raw
v)
            = do (Term
tv, Term
tt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t
                 (Term
vv, Term
vt, [Name]
vns) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk (RigCount -> RigCount -> RigCount
rigMult RigCount
rig RigCount
rigc) Term
u Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
v
                 Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC Context
ctxt Env
env Term
vt Term
tv
                 String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tt
                 (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Term
tv Term
vv, Term
tt, [Name]
vns)
          checkBinder (NLet Raw
t Raw
v)
            = do (Term
tv, Term
tt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t
                 (Term
vv, Term
vt, [Name]
vns) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
rigc Term
u Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
v
                 Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC Context
ctxt Env
env Term
vt Term
tv
                 String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tt
                 (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
NLet Term
tv Term
vv, Term
tt, [Name]
vns)
          checkBinder (Hole Raw
t)
            | Bool -> Bool
not Bool
holes = TC (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall (m :: * -> *) a. Monad m => m a -> StateT UCs m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Binder Term, Term, [Name])
 -> StateT UCs TC (Binder Term, Term, [Name]))
-> TC (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Err -> TC (Binder Term, Term, [Name])
forall a. Err -> TC a
tfail (Term -> Err
forall t. t -> Err' t
IncompleteTerm Term
forall a. HasCallStack => a
undefined)
            | Bool
otherwise
                   = do (Term
tv, Term
tt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t
                        String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tt
                        (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Binder Term
forall b. b -> Binder b
Hole Term
tv, Term
tt, [])
          checkBinder (GHole Int
i [Name]
ns Raw
t)
            = do (Term
tv, Term
tt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t
                 String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tt
                 (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Name] -> Term -> Binder Term
forall b. Int -> [Name] -> b -> Binder b
GHole Int
i [Name]
ns Term
tv, Term
tt, [])
          checkBinder (Guess Raw
t Raw
v)
            | Bool -> Bool
not Bool
holes = TC (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall (m :: * -> *) a. Monad m => m a -> StateT UCs m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Binder Term, Term, [Name])
 -> StateT UCs TC (Binder Term, Term, [Name]))
-> TC (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a b. (a -> b) -> a -> b
$ Err -> TC (Binder Term, Term, [Name])
forall a. Err -> TC a
tfail (Term -> Err
forall t. t -> Err' t
IncompleteTerm Term
forall a. HasCallStack => a
undefined)
            | Bool
otherwise
                   = do (Term
tv, Term
tt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t
                        (Term
vv, Term
vt, [Name]
vns) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
rigc Term
u Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
v
                        Context -> Env -> Term -> Term -> StateT UCs TC ()
convertsC Context
ctxt Env
env Term
vt Term
tv
                        String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tt
                        (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess Term
tv Term
vv, Term
tt, [Name]
vns)
          checkBinder (PVar RigCount
rig Raw
t)
            = do (Term
tv, Term
tt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t
                 String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tt
                 (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
PVar RigCount
rig Term
tv, Term
tt, [])
          checkBinder (PVTy Raw
t)
            = do (Term
tv, Term
tt, [Name]
_) <- RigCount
-> Term
-> Maybe UExp
-> Env
-> Raw
-> StateT UCs TC (Term, Term, [Name])
chk RigCount
Rig0 Term
u Maybe UExp
forall a. Maybe a
Nothing (Env -> Env
forall {a} {b} {c}. [(a, b, c)] -> [(a, RigCount, c)]
envZero Env
env) Raw
t
                 String -> Context -> Env -> Term -> StateT UCs TC ()
convType String
tcns Context
ctxt Env
env Term
tt
                 (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
forall a. a -> StateT UCs TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Binder Term
forall b. b -> Binder b
PVTy Term
tv, Term
tt, [])

          discharge :: n
-> Binder (TT n) -> TT n -> TT n -> TT n -> c -> m (TT n, TT n, c)
discharge n
n (Lam RigCount
r TT n
t) TT n
bt TT n
scv TT n
sct c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> Binder (TT n)
forall b. RigCount -> b -> Binder b
Lam RigCount
r TT n
t) TT n
scv, n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> Maybe ImplicitInfo -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
r Maybe ImplicitInfo
forall a. Maybe a
Nothing TT n
t TT n
bt) TT n
sct, c
ns)
          discharge n
n (Pi RigCount
r Maybe ImplicitInfo
i TT n
t TT n
k) TT n
bt TT n
scv TT n
sct c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> Maybe ImplicitInfo -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
r Maybe ImplicitInfo
i TT n
t TT n
k) TT n
scv, TT n
sct, c
ns)
          discharge n
n (Let RigCount
r TT n
t TT n
v) TT n
bt TT n
scv TT n
sct c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
r TT n
t TT n
v) TT n
scv, n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
r TT n
t TT n
v) TT n
sct, c
ns)
          discharge n
n (NLet TT n
t TT n
v) TT n
bt TT n
scv TT n
sct c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (TT n -> TT n -> Binder (TT n)
forall b. b -> b -> Binder b
NLet TT n
t TT n
v) TT n
scv, n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
RigW TT n
t TT n
v) TT n
sct, c
ns)
          discharge n
n (Hole TT n
t) TT n
bt TT n
scv TT n
sct c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (TT n -> Binder (TT n)
forall b. b -> Binder b
Hole TT n
t) TT n
scv, TT n
sct, c
ns)
          discharge n
n (GHole Int
i [Name]
ns TT n
t) TT n
bt TT n
scv TT n
sct c
uns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (Int -> [Name] -> TT n -> Binder (TT n)
forall b. Int -> [Name] -> b -> Binder b
GHole Int
i [Name]
ns TT n
t) TT n
scv, TT n
sct, c
uns)
          discharge n
n (Guess TT n
t TT n
v) TT n
bt TT n
scv TT n
sct c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (TT n -> TT n -> Binder (TT n)
forall b. b -> b -> Binder b
Guess TT n
t TT n
v) TT n
scv, TT n
sct, c
ns)
          discharge n
n (PVar RigCount
r TT n
t) TT n
bt TT n
scv TT n
sct c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> Binder (TT n)
forall b. RigCount -> b -> Binder b
PVar RigCount
r TT n
t) TT n
scv, n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (TT n -> Binder (TT n)
forall b. b -> Binder b
PVTy TT n
t) TT n
sct, c
ns)
          discharge n
n (PVTy TT n
t) TT n
bt TT n
scv TT n
sct c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (TT n -> Binder (TT n)
forall b. b -> Binder b
PVTy TT n
t) TT n
scv, TT n
sct, c
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 UniqueUse -> UniqueUse -> Bool
(UniqueUse -> UniqueUse -> Bool)
-> (UniqueUse -> UniqueUse -> Bool) -> Eq UniqueUse
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UniqueUse -> UniqueUse -> Bool
== :: UniqueUse -> UniqueUse -> Bool
$c/= :: UniqueUse -> UniqueUse -> Bool
/= :: UniqueUse -> UniqueUse -> Bool
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 :: [Name] -> Context -> Env -> Term -> TC ()
checkUnique [Name]
borrowed Context
ctxt Env
env Term
tm
         = StateT [(Name, (UniqueUse, Universe))] TC ()
-> [(Name, (UniqueUse, Universe))] -> TC ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders Env
env (Term -> Term
forall n. TT n -> TT n
explicitNames Term
tm)) []
  where
    isVar :: TT n -> Bool
isVar (P NameType
_ n
_ TT n
_) = Bool
True
    isVar (V Int
_) = Bool
True
    isVar TT n
_ = Bool
False

    chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
    chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders Env
env (V Int
i) | Env -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
env Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i = Name -> StateT [(Name, (UniqueUse, Universe))] TC ()
forall {t :: (* -> *) -> * -> *}.
(MonadState [(Name, (UniqueUse, Universe))] (t TC),
 MonadTrans t) =>
Name -> t TC ()
chkName ((Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv (Env
envEnv -> Int -> (Name, RigCount, Binder Term)
forall a. HasCallStack => [a] -> Int -> a
!!Int
i))
    chkBinders Env
env (P NameType
_ Name
n Term
_) = Name -> StateT [(Name, (UniqueUse, Universe))] TC ()
forall {t :: (* -> *) -> * -> *}.
(MonadState [(Name, (UniqueUse, Universe))] (t TC),
 MonadTrans t) =>
Name -> t TC ()
chkName Name
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
env (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ (NS (UN Text
lend) [Text
owner]) Term
_) Term
t) Term
a)
       | Term -> Bool
forall {n}. TT n -> Bool
isVar Term
a Bool -> Bool -> Bool
&& Text
owner Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Ownership" Bool -> Bool -> Bool
&&
         (Text
lend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"lend" Bool -> Bool -> Bool
|| Text
lend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Read")
            = do Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders Env
env Term
t -- Check the type normally
                 [(Name, (UniqueUse, Universe))]
st <- StateT
  [(Name, (UniqueUse, Universe))] TC [(Name, (UniqueUse, Universe))]
forall s (m :: * -> *). MonadState s m => m s
get
                 -- Remove the 'LendOnly' names from the unusable set
                 [(Name, (UniqueUse, Universe))]
-> StateT [(Name, (UniqueUse, Universe))] TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (((Name, (UniqueUse, Universe)) -> Bool)
-> [(Name, (UniqueUse, Universe))]
-> [(Name, (UniqueUse, Universe))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, (UniqueUse
ok, Universe
_)) -> UniqueUse
ok UniqueUse -> UniqueUse -> Bool
forall a. Eq a => a -> a -> Bool
/= UniqueUse
LendOnly) [(Name, (UniqueUse, Universe))]
st)
                 Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders Env
env Term
a
                 [(Name, (UniqueUse, Universe))]
-> StateT [(Name, (UniqueUse, Universe))] TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [(Name, (UniqueUse, Universe))]
st -- Reset the old state after checking the argument
    chkBinders Env
env (App AppStatus Name
_ Term
f Term
a) = do Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders Env
env Term
f; Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders Env
env Term
a
    chkBinders Env
env (Bind Name
n Binder Term
b Term
t)
       = do Env
-> Name
-> Binder Term
-> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinderName Env
env Name
n Binder Term
b
            [(Name, (UniqueUse, Universe))]
st <- StateT
  [(Name, (UniqueUse, Universe))] TC [(Name, (UniqueUse, Universe))]
forall s (m :: * -> *). MonadState s m => m s
get
            case Binder Term
b of
                 Let RigCount
_ Term
t Term
v -> Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders Env
env Term
v
                 Binder Term
_ -> () -> StateT [(Name, (UniqueUse, Universe))] TC ()
forall a. a -> StateT [(Name, (UniqueUse, Universe))] TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders ((Name
n, RigCount
Rig0, Binder Term
b) (Name, RigCount, Binder Term) -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env) Term
t
    chkBinders Env
env Term
t = () -> StateT [(Name, (UniqueUse, Universe))] TC ()
forall a. a -> StateT [(Name, (UniqueUse, Universe))] TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    chkBinderName :: Env -> Name -> Binder Term ->
                     StateT [(Name, (UniqueUse, Universe))] TC ()
    chkBinderName :: Env
-> Name
-> Binder Term
-> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinderName Env
env Name
n Binder Term
b
       = do let rawty :: Raw
rawty = [Name] -> Term -> Raw
forgetEnv (((Name, RigCount, Binder Term) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Term) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) (Binder Term -> Term
forall b. Binder b -> b
binderTy Binder Term
b)
            (Term
_, Term
kind) <- TC (Term, Term)
-> StateT [(Name, (UniqueUse, Universe))] TC (Term, Term)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT [(Name, (UniqueUse, Universe))] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Term, Term)
 -> StateT [(Name, (UniqueUse, Universe))] TC (Term, Term))
-> TC (Term, Term)
-> StateT [(Name, (UniqueUse, Universe))] TC (Term, Term)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (Term, Term)
check Context
ctxt Env
env Raw
rawty
            case Term
kind of
                 UType Universe
UniqueType -> do [(Name, (UniqueUse, Universe))]
ns <- StateT
  [(Name, (UniqueUse, Universe))] TC [(Name, (UniqueUse, Universe))]
forall s (m :: * -> *). MonadState s m => m s
get
                                        if Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
borrowed
                                           then [(Name, (UniqueUse, Universe))]
-> StateT [(Name, (UniqueUse, Universe))] TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
n, (UniqueUse
LendOnly, Universe
NullType)) (Name, (UniqueUse, Universe))
-> [(Name, (UniqueUse, Universe))]
-> [(Name, (UniqueUse, Universe))]
forall a. a -> [a] -> [a]
: [(Name, (UniqueUse, Universe))]
ns)
                                           else [(Name, (UniqueUse, Universe))]
-> StateT [(Name, (UniqueUse, Universe))] TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
n, (UniqueUse
Once, Universe
UniqueType)) (Name, (UniqueUse, Universe))
-> [(Name, (UniqueUse, Universe))]
-> [(Name, (UniqueUse, Universe))]
forall a. a -> [a] -> [a]
: [(Name, (UniqueUse, Universe))]
ns)
                 UType Universe
NullType -> do [(Name, (UniqueUse, Universe))]
ns <- StateT
  [(Name, (UniqueUse, Universe))] TC [(Name, (UniqueUse, Universe))]
forall s (m :: * -> *). MonadState s m => m s
get
                                      [(Name, (UniqueUse, Universe))]
-> StateT [(Name, (UniqueUse, Universe))] TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
n, (UniqueUse
Many, Universe
NullType)) (Name, (UniqueUse, Universe))
-> [(Name, (UniqueUse, Universe))]
-> [(Name, (UniqueUse, Universe))]
forall a. a -> [a] -> [a]
: [(Name, (UniqueUse, Universe))]
ns)
                 UType Universe
AllTypes -> do [(Name, (UniqueUse, Universe))]
ns <- StateT
  [(Name, (UniqueUse, Universe))] TC [(Name, (UniqueUse, Universe))]
forall s (m :: * -> *). MonadState s m => m s
get
                                      [(Name, (UniqueUse, Universe))]
-> StateT [(Name, (UniqueUse, Universe))] TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
n, (UniqueUse
Once, Universe
AllTypes)) (Name, (UniqueUse, Universe))
-> [(Name, (UniqueUse, Universe))]
-> [(Name, (UniqueUse, Universe))]
forall a. a -> [a] -> [a]
: [(Name, (UniqueUse, Universe))]
ns)
                 Term
_ -> () -> StateT [(Name, (UniqueUse, Universe))] TC ()
forall a. a -> StateT [(Name, (UniqueUse, Universe))] TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    chkName :: Name -> t TC ()
chkName Name
n
       = do [(Name, (UniqueUse, Universe))]
ns <- t TC [(Name, (UniqueUse, Universe))]
forall s (m :: * -> *). MonadState s m => m s
get
            case Name
-> [(Name, (UniqueUse, Universe))] -> Maybe (UniqueUse, Universe)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, (UniqueUse, Universe))]
ns of
                 Maybe (UniqueUse, Universe)
Nothing -> () -> t TC ()
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 Just (UniqueUse
Many, Universe
k) -> () -> t TC ()
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 Just (UniqueUse
Never, Universe
k) -> TC () -> t TC ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> t TC ()) -> TC () -> t TC ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Universe -> Name -> Err
forall t. Universe -> Name -> Err' t
UniqueError Universe
k Name
n)
                 Just (UniqueUse
LendOnly, Universe
k) -> TC () -> t TC ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> t TC ()) -> TC () -> t TC ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Universe -> Name -> Err
forall t. Universe -> Name -> Err' t
UniqueError Universe
k Name
n)
                 Just (UniqueUse
Once, Universe
k) -> [(Name, (UniqueUse, Universe))] -> t TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
n, (UniqueUse
Never, Universe
k)) (Name, (UniqueUse, Universe))
-> [(Name, (UniqueUse, Universe))]
-> [(Name, (UniqueUse, Universe))]
forall a. a -> [a] -> [a]
:
                                              ((Name, (UniqueUse, Universe)) -> Bool)
-> [(Name, (UniqueUse, Universe))]
-> [(Name, (UniqueUse, Universe))]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name, (UniqueUse, Universe))
x -> (Name, (UniqueUse, Universe)) -> Name
forall a b. (a, b) -> a
fst (Name, (UniqueUse, Universe))
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
n) [(Name, (UniqueUse, Universe))]
ns)