module Agda.TypeChecking.Reduce where
import Prelude hiding (mapM)
import Control.Monad.State hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Monad.Error hiding (mapM)
import Control.Applicative
import Data.List as List hiding (sort)
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set
import Data.Traversable
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Scope.Base (Scope)
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Patterns.Match
import Agda.TypeChecking.CompiledClause.Match
import Agda.Utils.Monad
#include "../undefined.h"
import Agda.Utils.Impossible
traceFun :: MonadTCM tcm => String -> tcm a -> tcm a
traceFun s m = do
reportSLn "tc.inst" 100 $ "[ " ++ s
x <- m
reportSLn "tc.inst" 100 $ "]"
return x
traceFun' :: (Show a, MonadTCM tcm) => String -> tcm a -> tcm a
traceFun' s m = do
reportSLn "tc.inst" 100 $ "[ " ++ s
x <- m
reportSLn "tc.inst" 100 $ " result = " ++ show x ++ "\n]"
return x
class Instantiate t where
instantiate :: MonadTCM tcm => t -> tcm t
instance Instantiate Term where
instantiate t@(MetaV x args) = do
mi <- mvInstantiation <$> lookupMeta x
case mi of
InstV a -> instantiate $ a `apply` args
Open -> return t
BlockedConst _ -> return t
PostponedTypeCheckingProblem _ -> return t
InstS _ -> __IMPOSSIBLE__
instantiate (Sort s) = Sort <$> instantiate s
instantiate t = return t
instance Instantiate a => Instantiate (Blocked a) where
instantiate v@NotBlocked{} = return v
instantiate v@(Blocked x u) = do
mi <- mvInstantiation <$> lookupMeta x
case mi of
InstV _ -> notBlocked <$> instantiate u
Open -> return v
BlockedConst _ -> return v
PostponedTypeCheckingProblem _ -> return v
InstS _ -> __IMPOSSIBLE__
instance Instantiate Type where
instantiate (El s t) = El <$> instantiate s <*> instantiate t
instance Instantiate Sort where
instantiate s = case s of
MetaS x as -> do
mi <- mvInstantiation <$> lookupMeta x
case mi of
InstS s' -> do
v <- instantiate (s' `apply` as)
case v of
Sort s -> return s
_ -> __IMPOSSIBLE__
Open -> return s
InstV{} -> __IMPOSSIBLE__
BlockedConst{} -> __IMPOSSIBLE__
PostponedTypeCheckingProblem{} -> __IMPOSSIBLE__
_ -> return s
instance Instantiate t => Instantiate (Abs t) where
instantiate = traverse instantiate
instance Instantiate t => Instantiate (Arg t) where
instantiate = traverse instantiate
instance Instantiate t => Instantiate [t] where
instantiate = traverse instantiate
instance (Instantiate a, Instantiate b) => Instantiate (a,b) where
instantiate (x,y) = (,) <$> instantiate x <*> instantiate y
instance (Instantiate a, Instantiate b,Instantiate c) => Instantiate (a,b,c) where
instantiate (x,y,z) = (,,) <$> instantiate x <*> instantiate y <*> instantiate z
instance Instantiate a => Instantiate (Closure a) where
instantiate cl = do
x <- enterClosure cl instantiate
return $ cl { clValue = x }
instance Instantiate Telescope where
instantiate tel = return tel
instance Instantiate Constraint where
instantiate (ValueCmp cmp t u v) = do
(t,u,v) <- instantiate (t,u,v)
return $ ValueCmp cmp t u v
instantiate (ArgsCmp cmp t as bs) = do
(t, as, bs) <- instantiate (t, as, bs)
return $ ArgsCmp cmp t as bs
instantiate (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> instantiate (u,v)
instantiate (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> instantiate (a,b)
instantiate (TelCmp cmp a b) = uncurry (TelCmp cmp) <$> instantiate (a,b)
instantiate (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> instantiate (a,b)
instantiate (Guarded c cs) = uncurry Guarded <$> instantiate (c,cs)
instantiate (UnBlock m) = return $ UnBlock m
instantiate (IsEmpty t) = IsEmpty <$> instantiate t
instance (Ord k, Instantiate e) => Instantiate (Map k e) where
instantiate = traverse instantiate
class Reduce t where
reduce :: MonadTCM tcm => t -> tcm t
reduceB :: MonadTCM tcm => t -> tcm (Blocked t)
reduce t = ignoreBlocking <$> reduceB t
reduceB t = notBlocked <$> reduce t
instance Reduce Type where
reduce (El s t) = El <$> reduce s <*> reduce t
reduceB (El s t) = do
s <- reduce s
t <- reduceB t
return (El s <$> t)
instance Reduce Sort where
reduce s =
ifM (not <$> hasUniversePolymorphism) (red sSuc sLub s)
$ liftTCM $ do
suc <- do sc <- primLevelSuc
return $ \x -> case x of
Type n -> Type (sc `apply` [Arg NotHidden Relevant n])
_ -> sSuc x
`catchError` \_ -> return sSuc
lub <- do mx <- primLevelMax
return $ \x y -> case (x, y) of
(Type n, Type m) -> Type (mx `apply` List.map (Arg NotHidden Relevant) [n, m])
_ -> sLub x y
`catchError` \_ -> return sLub
red suc lub =<< instantiateFull s
where
red suc lub s = do
s <- instantiate s
case s of
Suc s' -> suc <$> reduce s'
Lub s1 s2 -> lub <$> reduce s1 <*> reduce s2
DLub s1 s2 -> do
s <- dLub <$> reduce s1 <*> reduce s2
case s of
DLub{} -> return s
_ -> reduce s
Prop -> return s
Type s' -> Type <$> reduce s'
MetaS m as -> MetaS m <$> reduce as
Inf -> return Inf
instance Reduce t => Reduce (Abs t) where
reduce b = Abs (absName b) <$> underAbstraction_ b reduce
instance Reduce t => Reduce [t] where
reduce = traverse reduce
instance Reduce t => Reduce (Arg t) where
reduce = traverse reduce
reduceB t = traverse id <$> traverse reduceB t
instance (Reduce a, Reduce b) => Reduce (a,b) where
reduce (x,y) = (,) <$> reduce x <*> reduce y
instance (Reduce a, Reduce b,Reduce c) => Reduce (a,b,c) where
reduce (x,y,z) = (,,) <$> reduce x <*> reduce y <*> reduce z
instance Reduce Term where
reduceB v =
do v <- instantiate v
case v of
MetaV x args -> notBlocked . MetaV x <$> reduce args
Def f args -> unfoldDefinition False reduceB (Def f []) f args
Con c args -> do
v <- unfoldDefinition False reduceB (Con c []) c args
traverse reduceNat v
Sort s -> fmap Sort <$> reduceB s
Pi _ _ -> return $ notBlocked v
Fun _ _ -> return $ notBlocked v
Lit _ -> return $ notBlocked v
Var _ _ -> return $ notBlocked v
Lam _ _ -> return $ notBlocked v
DontCare -> return $ notBlocked v
where
reduceNat v@(Con c []) = do
mz <- getBuiltin' builtinZero
mlz <- getBuiltin' builtinLevelZero
case v of
_ | Just v == mz -> return $ Lit $ LitInt (getRange c) 0
| Just v == mlz -> return $ Lit $ LitLevel (getRange c) 0
_ -> return v
reduceNat v@(Con c [Arg NotHidden Relevant w]) = do
ms <- getBuiltin' builtinSuc
mls <- getBuiltin' builtinLevelSuc
case v of
_ | Just (Con c []) == ms ||
Just (Con c []) == mls -> inc <$> reduce w
_ -> return v
where
inc w = case w of
Lit (LitInt r n) -> Lit (LitInt (fuseRange c r) $ n + 1)
Lit (LitLevel r n) -> Lit (LitLevel (fuseRange c r) $ n + 1)
_ -> Con c [Arg NotHidden Relevant w]
reduceNat v = return v
unfoldDefinition :: MonadTCM tcm =>
Bool -> (Term -> tcm (Blocked Term)) ->
Term -> QName -> Args -> tcm (Blocked Term)
unfoldDefinition unfoldDelayed keepGoing v0 f args =
do
info <- getConstInfo f
case theDef info of
Constructor{conSrcCon = c} ->
return $ notBlocked $ Con (c `withRangeOf` f) args
Primitive{primAbstr = ConcreteDef, primName = x, primClauses = cls} -> do
pf <- getPrimitive x
reducePrimitive x v0 f args pf (defDelayed info)
(maybe [] (List.map translatedClause) cls)
(defCompiled info)
_ -> reduceNormal v0 f (map notReduced args) (defDelayed info)
(List.map translatedClause $ defClauses info)
(defCompiled info)
where
reducePrimitive x v0 f args pf delayed cls mcc
| n < ar = return $ notBlocked $ v0 `apply` args
| otherwise = do
let (args1,args2) = genericSplitAt ar args
r <- def args1
case r of
NoReduction args1' ->
reduceNormal v0 f (args1' ++
map notReduced args2)
delayed cls mcc
YesReduction v ->
keepGoing $ v `apply` args2
where
n = genericLength args
ar = primFunArity pf
def = primFunImplementation pf
reduceNormal v0 f args delayed def mcc = do
case def of
_ | Delayed <- delayed,
not unfoldDelayed -> defaultResult
[] -> defaultResult
cls@(Clause{ clausePats = ps } : _)
| length ps <= length args -> do
let (args1,args2') = splitAt (length ps) args
args2 = map ignoreReduced args2'
ev <- maybe (appDef' v0 cls args1)
(\cc -> appDef v0 cc args1) mcc
case ev of
NoReduction v -> return $ v `apply` args2
YesReduction v -> keepGoing $ v `apply` args2
| otherwise -> defaultResult
where defaultResult = return $ notBlocked $ v0 `apply` (map ignoreReduced args)
appDef :: MonadTCM tcm => Term -> CompiledClauses -> MaybeReducedArgs -> tcm (Reduced (Blocked Term) Term)
appDef v cc args = liftTCM $ do
r <- matchCompiled cc args
case r of
YesReduction t -> return $ YesReduction t
NoReduction args' -> return $ NoReduction $ fmap (apply v) args'
appDef' :: MonadTCM tcm => Term -> [Clause] -> MaybeReducedArgs -> tcm (Reduced (Blocked Term) Term)
appDef' v cls args = do
goCls cls (map ignoreReduced args) where
goCls :: MonadTCM tcm => [Clause] -> Args -> tcm (Reduced (Blocked Term) Term)
goCls [] args = typeError $ IncompletePatternMatching v args
goCls (cl@(Clause { clausePats = pats
, clauseBody = body }) : cls) args = do
(m, args) <- matchPatterns pats args
case m of
No -> goCls cls args
DontKnow Nothing -> return $ NoReduction $ notBlocked $ v `apply` args
DontKnow (Just m) -> return $ NoReduction $ blocked m $ v `apply` args
Yes args'
| hasBody body -> return $ YesReduction (
app args' body)
| otherwise -> return $ NoReduction $ notBlocked $ v `apply` args
hasBody (Body _) = True
hasBody NoBody = False
hasBody (Bind (Abs _ b)) = hasBody b
hasBody (NoBind b) = hasBody b
app [] (Body v') = v'
app (arg : args) (Bind (Abs _ body)) = app args $ subst arg body
app (_ : args) (NoBind body) = app args body
app _ NoBody = __IMPOSSIBLE__
app (_ : _) (Body _) = __IMPOSSIBLE__
app [] (Bind _) = __IMPOSSIBLE__
app [] (NoBind _) = __IMPOSSIBLE__
instance Reduce a => Reduce (Closure a) where
reduce cl = do
x <- enterClosure cl reduce
return $ cl { clValue = x }
instance Reduce Telescope where
reduce tel = return tel
instance Reduce Constraint where
reduce (ValueCmp cmp t u v) = do
(t,u,v) <- reduce (t,u,v)
return $ ValueCmp cmp t u v
reduce (ArgsCmp cmp t us vs) = do
(t,us,vs) <- reduce (t,us,vs)
return $ ArgsCmp cmp t us vs
reduce (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> reduce (u,v)
reduce (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> reduce (a,b)
reduce (TelCmp cmp a b) = uncurry (TelCmp cmp) <$> reduce (a,b)
reduce (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> reduce (a,b)
reduce (Guarded c cs) = uncurry Guarded <$> reduce (c,cs)
reduce (UnBlock m) = return $ UnBlock m
reduce (IsEmpty t) = IsEmpty <$> reduce t
instance (Ord k, Reduce e) => Reduce (Map k e) where
reduce = traverse reduce
class Normalise t where
normalise :: MonadTCM tcm => t -> tcm t
instance Normalise Sort where
normalise s = do
s <- reduce s
case s of
Suc s' -> sSuc <$> normalise s'
Lub s1 s2 -> sLub <$> normalise s1 <*> normalise s2
DLub s1 s2 -> dLub <$> normalise s1 <*> normalise s2
Prop -> return s
Type s' -> Type <$> normalise s'
MetaS m as -> MetaS m <$> normalise as
Inf -> return Inf
instance Normalise Type where
normalise (El s t) = El <$> normalise s <*> normalise t
instance Normalise Term where
normalise v =
do v <- reduce v
case v of
Var n vs -> Var n <$> normalise vs
Con c vs -> Con c <$> normalise vs
Def f vs -> Def f <$> normalise vs
MetaV x vs -> MetaV x <$> normalise vs
Lit _ -> return v
Lam h b -> Lam h <$> normalise b
Sort s -> Sort <$> normalise s
Pi a b -> uncurry Pi <$> normalise (a,b)
Fun a b -> uncurry Fun <$> normalise (a,b)
DontCare -> return v
instance Normalise ClauseBody where
normalise (Body t) = Body <$> normalise t
normalise (Bind b) = Bind <$> normalise b
normalise (NoBind b) = NoBind <$> normalise b
normalise NoBody = return NoBody
instance Normalise t => Normalise (Abs t) where
normalise a = Abs (absName a) <$> underAbstraction_ a normalise
instance Normalise t => Normalise (Arg t) where
normalise = traverse normalise
instance Normalise t => Normalise [t] where
normalise = traverse normalise
instance (Normalise a, Normalise b) => Normalise (a,b) where
normalise (x,y) = (,) <$> normalise x <*> normalise y
instance (Normalise a, Normalise b, Normalise c) => Normalise (a,b,c) where
normalise (x,y,z) =
do (x,(y,z)) <- normalise (x,(y,z))
return (x,y,z)
instance Normalise a => Normalise (Closure a) where
normalise cl = do
x <- enterClosure cl normalise
return $ cl { clValue = x }
instance Normalise a => Normalise (Tele a) where
normalise EmptyTel = return EmptyTel
normalise (ExtendTel a b) = uncurry ExtendTel <$> normalise (a, b)
instance Normalise Constraint where
normalise (ValueCmp cmp t u v) = do
(t,u,v) <- normalise (t,u,v)
return $ ValueCmp cmp t u v
normalise (ArgsCmp cmp t u v) = do
(t,u,v) <- normalise (t,u,v)
return $ ArgsCmp cmp t u v
normalise (LevelCmp cmp u v) = uncurry (LevelCmp cmp) <$> normalise (u,v)
normalise (TypeCmp cmp a b) = uncurry (TypeCmp cmp) <$> normalise (a,b)
normalise (TelCmp cmp a b) = uncurry (TelCmp cmp) <$> normalise (a,b)
normalise (SortCmp cmp a b) = uncurry (SortCmp cmp) <$> normalise (a,b)
normalise (Guarded c cs) = uncurry Guarded <$> normalise (c,cs)
normalise (UnBlock m) = return $ UnBlock m
normalise (IsEmpty t) = IsEmpty <$> normalise t
instance Normalise Pattern where
normalise p = case p of
VarP _ -> return p
LitP _ -> return p
ConP c mt ps -> ConP c <$> normalise mt <*> normalise ps
DotP v -> DotP <$> normalise v
instance Normalise DisplayForm where
normalise (Display n ps v) = Display n <$> normalise ps <*> return v
instance (Ord k, Normalise e) => Normalise (Map k e) where
normalise = traverse normalise
instance Normalise a => Normalise (Maybe a) where
normalise = traverse normalise
class InstantiateFull t where
instantiateFull :: MonadTCM tcm => t -> tcm t
instance InstantiateFull Name where
instantiateFull = return
instance InstantiateFull Sort where
instantiateFull s = do
s <- instantiate s
case s of
MetaS x as -> MetaS x <$> instantiateFull as
Type n -> Type <$> instantiateFull n
Prop -> return s
Suc s -> sSuc <$> instantiateFull s
Lub s1 s2 -> sLub <$> instantiateFull s1 <*> instantiateFull s2
DLub s1 s2 -> dLub <$> instantiateFull s1 <*> instantiateFull s2
Inf -> return s
instance InstantiateFull Type where
instantiateFull (El s t) =
El <$> instantiateFull s <*> instantiateFull t
instance InstantiateFull Term where
instantiateFull v = etaOnce =<< do
v <- instantiate v
case v of
Var n vs -> Var n <$> instantiateFull vs
Con c vs -> Con c <$> instantiateFull vs
Def f vs -> Def f <$> instantiateFull vs
MetaV x vs -> MetaV x <$> instantiateFull vs
Lit _ -> return v
Lam h b -> Lam h <$> instantiateFull b
Sort s -> Sort <$> instantiateFull s
Pi a b -> uncurry Pi <$> instantiateFull (a,b)
Fun a b -> uncurry Fun <$> instantiateFull (a,b)
DontCare -> return v
instance InstantiateFull Pattern where
instantiateFull v@VarP{} = return v
instantiateFull (DotP t) = DotP <$> instantiateFull t
instantiateFull (ConP n mt ps) = ConP n <$> instantiateFull mt <*> instantiateFull ps
instantiateFull l@LitP{} = return l
instance InstantiateFull ClauseBody where
instantiateFull (Body t) = Body <$> instantiateFull t
instantiateFull (Bind b) = Bind <$> instantiateFull b
instantiateFull (NoBind b) = NoBind <$> instantiateFull b
instantiateFull NoBody = return NoBody
instance InstantiateFull t => InstantiateFull (Abs t) where
instantiateFull a = Abs (absName a) <$> underAbstraction_ a instantiateFull
instance InstantiateFull t => InstantiateFull (Arg t) where
instantiateFull = traverse instantiateFull
instance InstantiateFull t => InstantiateFull [t] where
instantiateFull = traverse instantiateFull
instance (InstantiateFull a, InstantiateFull b) => InstantiateFull (a,b) where
instantiateFull (x,y) = (,) <$> instantiateFull x <*> instantiateFull y
instance (InstantiateFull a, InstantiateFull b, InstantiateFull c) => InstantiateFull (a,b,c) where
instantiateFull (x,y,z) =
do (x,(y,z)) <- instantiateFull (x,(y,z))
return (x,y,z)
instance InstantiateFull a => InstantiateFull (Closure a) where
instantiateFull cl = do
x <- enterClosure cl instantiateFull
return $ cl { clValue = x }
instance InstantiateFull Constraint where
instantiateFull c = case c of
ValueCmp cmp t u v -> do
(t,u,v) <- instantiateFull (t,u,v)
return $ ValueCmp cmp t u v
ArgsCmp cmp t u v -> do
(t,u,v) <- instantiateFull (t,u,v)
return $ ArgsCmp cmp t u v
LevelCmp cmp u v -> uncurry (LevelCmp cmp) <$> instantiateFull (u,v)
TypeCmp cmp a b -> uncurry (TypeCmp cmp) <$> instantiateFull (a,b)
TelCmp cmp a b -> uncurry (TelCmp cmp) <$> instantiateFull (a,b)
SortCmp cmp a b -> uncurry (SortCmp cmp) <$> instantiateFull (a,b)
Guarded c cs -> uncurry Guarded <$> instantiateFull (c,cs)
UnBlock m -> return $ UnBlock m
IsEmpty t -> IsEmpty <$> instantiateFull t
instance (Ord k, InstantiateFull e) => InstantiateFull (Map k e) where
instantiateFull = traverse instantiateFull
instance InstantiateFull ModuleName where
instantiateFull = return
instance InstantiateFull Scope where
instantiateFull = return
instance InstantiateFull Signature where
instantiateFull (Sig a b) = uncurry Sig <$> instantiateFull (a, b)
instance InstantiateFull Section where
instantiateFull (Section tel n) = flip Section n <$> instantiateFull tel
instance InstantiateFull a => InstantiateFull (Tele a) where
instantiateFull EmptyTel = return EmptyTel
instantiateFull (ExtendTel a b) = uncurry ExtendTel <$> instantiateFull (a, b)
instance InstantiateFull Char where
instantiateFull = return
instance InstantiateFull Definition where
instantiateFull (Defn rel x t df i d) = do
(t, (df, d)) <- instantiateFull (t, (df, d))
return $ Defn rel x t df i d
instance InstantiateFull a => InstantiateFull (Open a) where
instantiateFull (OpenThing n a) = OpenThing n <$> instantiateFull a
instance InstantiateFull DisplayForm where
instantiateFull (Display n ps v) = uncurry (Display n) <$> instantiateFull (ps, v)
instance InstantiateFull DisplayTerm where
instantiateFull (DTerm v) = DTerm <$> instantiateFull v
instantiateFull (DWithApp vs ws) = uncurry DWithApp <$> instantiateFull (vs, ws)
instance InstantiateFull Defn where
instantiateFull d = case d of
Axiom{} -> return d
Function{ funClauses = cs, funCompiled = cc, funInv = inv } -> do
(cs, cc, inv) <- instantiateFull (cs, cc, inv)
return $ d { funClauses = cs, funCompiled = cc, funInv = inv }
Datatype{ dataSort = s, dataClause = cl } -> do
s <- instantiateFull s
cl <- instantiateFull cl
return $ d { dataSort = s, dataClause = cl }
Record{ recConType = t, recClause = cl, recTel = tel } -> do
t <- instantiateFull t
cl <- instantiateFull cl
tel <- instantiateFull tel
return $ d { recConType = t, recClause = cl, recTel = tel }
Constructor{} -> return d
Primitive{ primClauses = cs } -> do
cs <- instantiateFull cs
return $ d { primClauses = cs }
instance InstantiateFull FunctionInverse where
instantiateFull NotInjective = return NotInjective
instantiateFull (Inverse inv) = Inverse <$> instantiateFull inv
instance InstantiateFull a => InstantiateFull (Case a) where
instantiateFull (Branches cs ls m) =
Branches <$> instantiateFull cs
<*> instantiateFull ls
<*> instantiateFull m
instance InstantiateFull CompiledClauses where
instantiateFull Fail = return Fail
instantiateFull (Done m t) = Done m <$> instantiateFull t
instantiateFull (Case n bs) = Case n <$> instantiateFull bs
instance InstantiateFull Clauses where
instantiateFull (Clauses c tc) =
Clauses <$> instantiateFull c <*> instantiateFull tc
instance InstantiateFull Clause where
instantiateFull (Clause r tel perm ps b) =
Clause r <$> instantiateFull tel
<*> return perm
<*> instantiateFull ps
<*> instantiateFull b
instance InstantiateFull Interface where
instantiateFull (Interface ms mod scope inside
sig b hsImports highlighting pragmas) =
Interface ms mod scope inside
<$> instantiateFull sig
<*> instantiateFull b
<*> return hsImports
<*> return highlighting
<*> return pragmas
instance InstantiateFull a => InstantiateFull (Builtin a) where
instantiateFull (Builtin t) = Builtin <$> instantiateFull t
instantiateFull (Prim x) = Prim <$> instantiateFull x
instance InstantiateFull a => InstantiateFull (Maybe a) where
instantiateFull = mapM instantiateFull
telViewM :: MonadTCM tcm => Type -> tcm TelView
telViewM t = do
t <- reduce t
case unEl t of
Pi a (Abs x b) -> absV a x <$> telViewM b
Fun a b -> absV a "_" <$> telViewM (raise 1 b)
_ -> return $ TelV EmptyTel t
where
absV a x (TelV tel t) = TelV (ExtendTel a (Abs x tel)) t