summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/CheckInternal.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/CheckInternal.hs')
-rw-r--r--src/full/Agda/TypeChecking/CheckInternal.hs17
1 files changed, 8 insertions, 9 deletions
diff --git a/src/full/Agda/TypeChecking/CheckInternal.hs b/src/full/Agda/TypeChecking/CheckInternal.hs
index 9064cf7..ae93954 100644
--- a/src/full/Agda/TypeChecking/CheckInternal.hs
+++ b/src/full/Agda/TypeChecking/CheckInternal.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-- Initially authored by Andreas, 2013-10-22.
@@ -126,17 +125,17 @@ checkInternal' action v t = do
MetaV x es -> do -- we assume meta instantiations to be well-typed
a <- metaType x
checkSpine action a (MetaV x []) es t
- Con c vs -> do
+ Con c ci vs -> do
-- we need to fully apply the constructor to make getConType work
TelV tel t <- telView t
- addCtxTel tel $ do
+ addContext tel $ do
let failure = typeError $ DoesNotConstructAnElementOf (conName c) t
vs' = raise (size tel) vs ++ teleArgs tel
a <- maybe failure return =<< getConType c t
- Con c vs2 <- checkArgs action a (Con c []) vs' t
+ Con c ci vs2 <- checkArgs action a (Con c ci []) vs' t
-- Strip away the extra arguments
return $ applySubst (strengthenS __IMPOSSIBLE__ (size tel))
- $ Con c (take (length vs) vs2)
+ $ Con c ci (take (length vs) vs2)
Lit l -> Lit l <$ ((`subtype` t) =<< litType l)
Lam ai vb -> do
(a, b) <- shouldBePi t
@@ -227,7 +226,7 @@ inferDef' f a es = do
Just Projection{ projIndex = n } | n > 0 -> do
let self = unArg a
b <- infer self
- snd <$> inferSpine b self (Proj f : es)
+ snd <$> inferSpine b self (Proj ProjSystem f : es)
_ -> inferDef f (Apply a : es)
@@ -257,10 +256,10 @@ inferSpine' action t self self' (e : es) = do
v' <- checkInternal' action v $ unDom a
inferSpine' action (b `absApp` v) (self `applyE` [e]) (self' `applyE` [Apply (Arg ai v')]) es
-- case: projection or projection-like
- Proj f -> do
+ Proj o f -> do
(a, b) <- shouldBePi =<< shouldBeProjectible t f
- u <- f `applyDef` (argFromDom a $> self)
- u' <- f `applyDef` (argFromDom a $> self')
+ u <- applyDef o f (argFromDom a $> self)
+ u' <- applyDef o f (argFromDom a $> self')
inferSpine' action (b `absApp` self) u u' es
-- | Type should either be a record type of a type eligible for