{-# LANGUAGE DeriveFunctor, FlexibleContexts, FlexibleInstances,
MultiParamTypeClasses, PatternGuards #-}
module Idris.Core.Typecheck where
import Idris.Core.Evaluate
import Idris.Core.TT
import Control.Monad.State
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
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
= 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 ->
Type ->
Maybe UExp ->
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
| [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, [])
| 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
= 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))
(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
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
(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
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
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)
data UniqueUse = Never
| Once
| LendOnly
| Many
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
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
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
[(Name, (UniqueUse, Universe))]
st <- 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, (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
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)