{-|
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.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 ctxt :: Context
ctxt env :: Env
env x :: Term
x y :: 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 (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 (m :: * -> *) a. Monad m => a -> m a
return ()
                 else TC () -> StateT UCs TC ()
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 ctxt :: Context
ctxt env :: Env
env x :: Term
x y :: 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 True -> () -> TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          _ -> 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 True -> () -> TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                _ -> 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 (n :: a
n, _, Hole _) = Bool
True
isHole _ = 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 (\(x :: 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 ctxt :: Context
ctxt env :: Env
env tm :: 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' tm :: Term
tm | Term -> Bool
isUniverse Term
tm = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                     | Bool
otherwise = String -> m ()
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]
++ " is not a Type")

convType :: String -> Context -> Env -> Term -> StateT UCs TC ()
convType :: String -> Context -> Env -> Term -> StateT UCs TC ()
convType tcns :: String
tcns ctxt :: Context
ctxt env :: Env
env tm :: Term
tm =
    do (v :: Int
v, cs :: [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
+ 1, [UConstraint]
cs)
       case Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
tm of
            UType _ -> () -> StateT UCs TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            _ -> 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 uniq_check :: Bool
uniq_check bs :: [Name]
bs tcns :: String
tcns ctxt :: Context
ctxt env :: Env
env tm :: Raw
tm orig :: 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 _) -> 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 e :: Err
e -> Err -> TC (Term, Term, UCs)
forall a. Err -> TC a
Error Err
e
          OK ((tm :: Term
tm, ty :: Term
ty), constraints :: 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 (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 ctxt :: Context
ctxt env :: Env
env tm :: 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) (0, [])

check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)
check' :: Bool
-> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Term)
check' holes :: Bool
holes tcns :: String
tcns ctxt :: Context
ctxt env :: Env
env top :: Raw
top
   = do (tm :: Term
tm, ty :: Term
ty, _) <- 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 (-5))) Maybe UExp
forall a. Maybe a
Nothing Env
env Raw
top
        (Term, Term) -> StateT UCs TC (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, Term
ty)
 where

  smaller :: TT n -> TT n -> TT n
smaller (UType NullType) _ = Universe -> TT n
forall n. Universe -> TT n
UType Universe
NullType
  smaller _ (UType NullType) = Universe -> TT n
forall n. Universe -> TT n
UType Universe
NullType
  smaller (UType u :: Universe
u)        _ = Universe -> TT n
forall n. Universe -> TT n
UType Universe
u
  smaller _        (UType u :: Universe
u) = Universe -> TT n
forall n. Universe -> TT n
UType Universe
u
  smaller x :: TT n
x        _         = 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 rigc :: RigCount
rigc u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env (Var n :: Name
n)
      | Just (i :: Int
i, erig :: RigCount
erig, ty :: 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
                    Nothing -> (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
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 msg :: String
msg -> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
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 nt :: NameType
nt n' :: Name
n' ty :: 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 (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 (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 True _    _    n :: a
n = Maybe String
forall a. Maybe a
Nothing
          rigSafe _    Rig1 RigW n :: a
n = String -> Maybe String
forall a. a -> Maybe a
Just ("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]
++ " in non-linear context")
          rigSafe _    Rig0 RigW n :: a
n = String -> Maybe String
forall a. a -> Maybe a
Just ("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]
++ " in relevant context")
          rigSafe _    Rig0 Rig1 n :: a
n = String -> Maybe String
forall a. a -> Maybe a
Just ("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]
++ " in relevant context")
          rigSafe _    _    _    n :: a
n = Maybe String
forall a. Maybe a
Nothing

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

  chk rigc :: RigCount
rigc u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env ap :: Raw
ap@(RApp f :: Raw
f RType) | Bool -> Bool
not Bool
holes
    -- special case to reduce constraintss
      = do (fv :: Term
fv, fty :: Term
fty, fns :: [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 x :: Name
x (Pi _ i :: Maybe ImplicitInfo
i s :: Term
s k :: Term
k) t :: Term
t) -> Term
ty
                        _ -> [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 x :: Name
x (Pi _ i :: Maybe ImplicitInfo
i s :: Term
s k :: Term
k) t :: Term
t) -> Term
ty
                                     _ -> Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
fty
           case Term
fty' of
             Bind x :: Name
x (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i (TType v' :: UExp
v') k :: Term
k) t :: Term
t ->
               do (v :: Int
v, cs :: [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
+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 (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 x :: Name
x (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i s :: Term
s k :: Term
k) t :: Term
t ->
                 do (av :: Term
av, aty :: Term
aty, _) <- 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 (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)
             t :: Term
t -> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
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 rigc :: RigCount
rigc u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env ap :: Raw
ap@(RApp f :: Raw
f a :: Raw
a)
      = do (fv :: Term
fv, fty :: Term
fty, fns :: [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 (rigf :: RigCount
rigf, 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 x :: Name
x (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i s :: Term
s k :: Term
k) t :: Term
t) -> (RigCount
rig, Term
ty)
                        _ -> case Context -> Env -> Term -> Term
normalise Context
ctxt Env
env Term
fty of
                                  ty :: Term
ty@(Bind x :: Name
x (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i s :: Term
s k :: Term
k) t :: 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)
                                  _ -> (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...
           (av :: Term
av, aty :: Term
aty, ans_in :: [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
                          Rig0 -> []
                          _ -> [Name]
ans_in
           case Term
fty' of
             Bind x :: Name
x (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i s :: Term
s k :: Term
k) t :: 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 (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)
             t :: Term
t -> TC (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
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 rigc :: RigCount
rigc u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env RType
    | Bool
holes = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> Term
forall n. UExp -> TT n
TType (Int -> UExp
UVal 0), UExp -> Term
forall n. UExp -> TT n
TType (Int -> UExp
UVal 0), [])
    | Bool
otherwise = do (v :: Int
v, cs :: [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
+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
+2, (UConstraint
cUConstraint -> [UConstraint] -> [UConstraint]
forall a. a -> [a] -> [a]
:[UConstraint]
cs))
                     (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
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
+1)), [])
  chk rigc :: RigCount
rigc u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env (RUType un :: Universe
un)
    | Bool
holes = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
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 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 (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 0), [])
  chk rigc :: RigCount
rigc u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env (RConstant Forgot) = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
forall n. TT n
Erased, Term
forall n. TT n
Erased, [])
  chk rigc :: RigCount
rigc u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env (RConstant c :: Const
c) = (Term, Term, [Name]) -> StateT UCs TC (Term, Term, [Name])
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 _)   = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative))
          constType (BI _)  = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig))
          constType (Fl _)  = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType ArithTy
ATFloat)
          constType (Ch _)  = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITChar))
          constType (Str _) = Const -> TT n
forall n. Const -> TT n
Constant Const
StrType
          constType (B8 _)  = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT8)))
          constType (B16 _) = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT16)))
          constType (B32 _) = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT32)))
          constType (B64 _) = Const -> TT n
forall n. Const -> TT n
Constant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)))
          constType TheWorld = Const -> TT n
forall n. Const -> TT n
Constant Const
WorldType
          constType Forgot  = TT n
forall n. TT n
Erased
          constType _       = UExp -> TT n
forall n. UExp -> TT n
TType (Int -> UExp
UVal 0)
  chk rigc :: RigCount
rigc u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env (RBind n :: Name
n (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i s :: Raw
s k :: Raw
k) t :: Raw
t)
      = do (sv :: Term
sv, st :: Term
st, sns :: [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
           (v :: Int
v, cs :: [UConstraint]
cs) <- StateT UCs TC UCs
forall s (m :: * -> *). MonadState s m => m s
get
           (kv :: Term
kv, kt :: Term
kt, _) <- 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
+1, [UConstraint]
cs)
           let maxu :: UExp
maxu = case Maybe UExp
lvl of
                           Nothing -> String -> Int -> UExp
UVar String
tcns Int
v
                           Just v' :: UExp
v' -> UExp
v'
           (tv :: Term
tv, tt :: Term
tt, tns :: [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 su :: UExp
su, TType tu :: 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 (v :: Int
v, cs :: [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 (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)
                (un :: Term
un, 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 (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 rigc_in :: RigCount
rigc_in u :: Term
u lvl :: Maybe UExp
lvl env :: Env
env (RBind n :: Name
n b :: Binder Raw
b sc :: Raw
sc)
      = do (b' :: Binder Term
b', bt' :: Term
bt', bns :: [Name]
bns) <- Binder Raw -> StateT UCs TC (Binder Term, Term, [Name])
checkBinder Binder Raw
b
           (scv :: Term
scv, sct :: Term
sct, scns :: [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
                      Rig0 -> RigCount
Rig0
                      _ -> RigCount
Rig1
          getCount :: Binder b -> RigCount
getCount (Pi rig :: RigCount
rig _ _ _) = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
rig
          getCount (PVar rig :: RigCount
rig _) = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
rig
          getCount (Lam rig :: RigCount
rig _) = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
rig
          getCount (Let rig :: RigCount
rig _ _) = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
rig
          getCount _ = RigCount -> RigCount -> RigCount
rigMult RigCount
rigc RigCount
RigW

          checkUsageOK :: RigCount -> [Name] -> t TC ()
checkUsageOK Rig0 _ = () -> t TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          checkUsageOK RigW _ = () -> t TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          checkUsageOK Rig1 ns :: [Name]
ns
              = let used :: Int
used = [Name] -> 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
== 1 then () -> t TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                       else TC () -> t TC ()
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
$ "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]
++
                              " 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 rig :: RigCount
rig t :: Raw
t)
            = do (tv :: Term
tv, tt :: Term
tt, _) <- 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 (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 rig :: RigCount
rig t :: Raw
t v :: Raw
v)
            = do (tv :: Term
tv, tt :: Term
tt, _) <- 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
                 (vv :: Term
vv, vt :: Term
vt, vns :: [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 (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 t :: Raw
t v :: Raw
v)
            = do (tv :: Term
tv, tt :: Term
tt, _) <- 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
                 (vv :: Term
vv, vt :: Term
vt, vns :: [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 (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 t :: Raw
t)
            | Bool -> Bool
not Bool
holes = TC (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
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 (tv :: Term
tv, tt :: Term
tt, _) <- 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 (m :: * -> *) a. Monad m => a -> m a
return (Term -> Binder Term
forall b. b -> Binder b
Hole Term
tv, Term
tt, [])
          checkBinder (GHole i :: Int
i ns :: [Name]
ns t :: Raw
t)
            = do (tv :: Term
tv, tt :: Term
tt, _) <- 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 (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 t :: Raw
t v :: Raw
v)
            | Bool -> Bool
not Bool
holes = TC (Binder Term, Term, [Name])
-> StateT UCs TC (Binder Term, Term, [Name])
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 (tv :: Term
tv, tt :: Term
tt, _) <- 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
                        (vv :: Term
vv, vt :: Term
vt, vns :: [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 (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 rig :: RigCount
rig t :: Raw
t)
            = do (tv :: Term
tv, tt :: Term
tt, _) <- 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 (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 t :: Raw
t)
            = do (tv :: Term
tv, tt :: Term
tt, _) <- 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 (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
n (Lam r :: RigCount
r t :: TT n
t) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct ns :: c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
n (Pi r :: RigCount
r i :: Maybe ImplicitInfo
i t :: TT n
t k :: TT n
k) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct ns :: c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
n (Let r :: RigCount
r t :: TT n
t v :: TT n
v) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct ns :: c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
n (NLet t :: TT n
t v :: TT n
v) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct ns :: c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
n (Hole t :: TT n
t) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct ns :: c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
n (GHole i :: Int
i ns :: [Name]
ns t :: TT n
t) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct uns :: c
uns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
n (Guess t :: TT n
t v :: TT n
v) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct ns :: c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
n (PVar r :: RigCount
r t :: TT n
t) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct ns :: c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
n (PVTy t :: TT n
t) bt :: TT n
bt scv :: TT n
scv sct :: TT n
sct ns :: c
ns
            = (TT n, TT n, c) -> m (TT n, TT n, c)
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
/= :: UniqueUse -> UniqueUse -> Bool
$c/= :: UniqueUse -> UniqueUse -> Bool
== :: UniqueUse -> UniqueUse -> Bool
$c== :: 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 borrowed :: [Name]
borrowed ctxt :: Context
ctxt env :: Env
env tm :: 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 _ _ _) = Bool
True
    isVar (V _) = Bool
True
    isVar _ = Bool
False

    chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
    chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders env :: Env
env (V i :: Int
i) | Env -> 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. [a] -> Int -> a
!!Int
i))
    chkBinders env :: Env
env (P _ n :: Name
n _) = 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
env (App _ (App _ (P _ (NS (UN lend :: Text
lend) [owner :: Text
owner]) _) t :: Term
t) a :: 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 "Ownership" Bool -> Bool -> Bool
&&
         (Text
lend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "lend" Bool -> Bool -> Bool
|| Text
lend Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "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 (\(n :: Name
n, (ok :: UniqueUse
ok, _)) -> 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
env (App _ f :: Term
f a :: 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
env (Bind n :: Name
n b :: Binder Term
b t :: 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 _ t :: Term
t v :: Term
v -> Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders Env
env Term
v
                 _ -> () -> StateT [(Name, (UniqueUse, Universe))] TC ()
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
env t :: Term
t = () -> StateT [(Name, (UniqueUse, Universe))] TC ()
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
env n :: Name
n b :: 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)
            (_, kind :: Term
kind) <- TC (Term, Term)
-> StateT [(Name, (UniqueUse, Universe))] TC (Term, Term)
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 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 (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 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 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)
                 _ -> () -> StateT [(Name, (UniqueUse, Universe))] TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    chkName :: Name -> t TC ()
chkName n :: 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
                 Nothing -> () -> t TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 Just (Many, k :: Universe
k) -> () -> t TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 Just (Never, k :: Universe
k) -> TC () -> t TC ()
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 (LendOnly, k :: Universe
k) -> TC () -> t TC ()
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 (Once, k :: 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 (\x :: (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)