summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/Term.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/Term.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/Term.hs230
1 files changed, 176 insertions, 54 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/Term.hs b/src/full/Agda/TypeChecking/Rules/Term.hs
index 451e3c4..fc6c343 100644
--- a/src/full/Agda/TypeChecking/Rules/Term.hs
+++ b/src/full/Agda/TypeChecking/Rules/Term.hs
@@ -1,10 +1,14 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections #-}
+
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
module Agda.TypeChecking.Rules.Term where
@@ -13,6 +17,7 @@ import Control.Monad.Trans
import Control.Monad.Reader
import Data.Maybe
+import Data.Monoid (mappend)
import Data.List hiding (sort)
import qualified Data.Map as Map
import Data.Traversable (sequenceA)
@@ -93,17 +98,24 @@ isType e s =
-- | Check that an expression is a type without knowing the sort.
isType_ :: A.Expr -> TCM Type
isType_ e =
- traceCall (IsType_ e) $ sharedType <$>
+ traceCall (IsType_ e) $ sharedType <$> do
+ let fallback = isType e =<< do workOnTypes $ newSortMeta
case unScope e of
A.Fun i (Arg info t) b -> do
a <- Dom info <$> isType_ t
b <- isType_ b
- return $ El (sLub (getSort $ unDom a) (getSort b)) (Pi (convColor a) (NoAbs underscore b))
+ s <- ptsRule a b
+ let t' = El s $ Pi (convColor a) $ NoAbs underscore b
+ noFunctionsIntoSize b t'
+ return t'
+ A.Pi _ tel e | null tel -> isType_ e
A.Pi _ tel e -> do
- checkTelescope_ tel $ \tel -> do
+ checkPiTelescope tel $ \tel -> do
t <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
- return $ telePi tel t
+ let t' = telePi tel t
+ noFunctionsIntoSize t t'
+ return t'
A.Set _ n -> do
n <- ifM typeInType (return 0) (return n)
return $ sort (mkType n)
@@ -119,9 +131,25 @@ isType_ e =
applyRelevanceToContext NonStrict $
checkExpr (namedThing l) lvl
return $ sort (Type n)
- _ -> do
- s <- workOnTypes $ newSortMeta
- isType e s
+ _ -> fallback
+
+ptsRule :: (LensSort a, LensSort b) => a -> b -> TCM Sort
+ptsRule a b = pts <$> reduce (getSort a) <*> reduce (getSort b)
+
+-- | Ensure that a (freshly created) function type does not inhabit 'SizeUniv'.
+noFunctionsIntoSize :: Type -> Type -> TCM ()
+noFunctionsIntoSize t tBlame = do
+ reportSDoc "tc.fun" 20 $ do
+ let El s (Pi dom b) = ignoreSharing <$> tBlame
+ sep [ text "created function type " <+> prettyTCM tBlame
+ , text "with pts rule" <+> prettyTCM (getSort dom, getSort b, s)
+ ]
+ s <- reduce $ getSort t
+ when (s == SizeUniv) $ do
+ -- Andreas, 2015-02-14
+ -- We have constructed a function type in SizeUniv
+ -- which is illegal to prevent issue 1428.
+ typeError $ FunctionTypeInSizeUniv $ unEl tBlame
-- | Check that an expression is a type which is equal to a given type.
isTypeEqualTo :: A.Expr -> Type -> TCM Type
@@ -139,11 +167,11 @@ leqType_ t t' = workOnTypes $ leqType t t'
-- | Force a type to be a Pi. Instantiates if necessary. The 'Hiding' is only
-- used when instantiating a meta variable.
-forcePi :: Hiding -> String -> Type -> TCM (Type, Constraints)
+forcePi :: Hiding -> String -> Type -> TCM Type
forcePi h name (El s t) =
do t' <- reduce t
case t' of
- Pi _ _ -> return (El s t', [])
+ Pi _ _ -> return $ El s t'
_ -> do
sa <- newSortMeta
sb <- newSortMeta
@@ -151,35 +179,50 @@ forcePi h name (El s t) =
a <- newTypeMeta sa
x <- freshName_ name
- let arg = Arg h Relevant a
+ let arg = setHiding h $ defaultDom a
b <- addCtx x arg $ newTypeMeta sb
let ty = El s' $ Pi arg (Abs (show x) b)
- cs <- equalType (El s t') ty
+ equalType (El s t') ty
ty' <- reduce ty
- return (ty', cs)
+ return ty'
-}
---------------------------------------------------------------------------
-- * Telescopes
---------------------------------------------------------------------------
+-- | Type check a (module) telescope.
+-- Binds the variables defined by the telescope.
+checkTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
+checkTelescope = checkTelescope' LamNotPi
+
+-- | Type check the telescope of a dependent function type.
+-- Binds the resurrected variables defined by the telescope.
+-- The returned telescope is unmodified (not resurrected).
+checkPiTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
+checkPiTelescope = checkTelescope' PiNotLam
+
+-- | Flag to control resurrection on domains.
+data LamOrPi
+ = LamNotPi -- ^ We are checking a module telescope.
+ -- We pass into the type world to check the domain type.
+ -- This resurrects the whole context.
+ | PiNotLam -- ^ We are checking a telescope in a Pi-type.
+ -- We stay in the term world, but add resurrected
+ -- domains to the context to check the remaining
+ -- domains and codomain of the Pi-type.
+ deriving (Eq, Show)
+
-- | Type check a telescope. Binds the variables defined by the telescope.
-checkTelescope_ :: A.Telescope -> (Telescope -> TCM a) -> TCM a
-checkTelescope_ [] ret = ret EmptyTel
-checkTelescope_ (b : tel) ret =
- checkTypedBindings_ b $ \tel1 ->
- checkTelescope_ tel $ \tel2 ->
+checkTelescope' :: LamOrPi -> A.Telescope -> (Telescope -> TCM a) -> TCM a
+checkTelescope' lamOrPi [] ret = ret EmptyTel
+checkTelescope' lamOrPi (b : tel) ret =
+ checkTypedBindings lamOrPi b $ \tel1 ->
+ checkTelescope' lamOrPi tel $ \tel2 ->
ret $ abstract tel1 tel2
-- | Check a typed binding and extends the context with the bound variables.
-- The telescope passed to the continuation is valid in the original context.
-checkTypedBindings_ :: A.TypedBindings -> (Telescope -> TCM a) -> TCM a
-checkTypedBindings_ = checkTypedBindings PiNotLam
-
-data LamOrPi = LamNotPi | PiNotLam deriving (Eq,Show)
-
--- | Check a typed binding and extends the context with the bound variables.
--- The telescope passed to the continuation is valid in the original context.
--
-- Parametrized by a flag wether we check a typed lambda or a Pi. This flag
-- is needed for irrelevance.
@@ -196,7 +239,8 @@ checkTypedBinding lamOrPi info (A.TBind i xs e) ret = do
allowed <- optExperimentalIrrelevance <$> pragmaOptions
t <- modEnv lamOrPi allowed $ isType_ e
let info' = mapRelevance (modRel lamOrPi allowed) info
- addCtxs xs (convColor $ Dom info' t) $ ret $ bindsToTel xs (convColor $ Dom info t)
+ addContext (xs, convColor (Dom info' t) :: I.Dom Type) $
+ ret $ bindsWithHidingToTel xs (convColor $ Dom info t)
where
-- if we are checking a typed lambda, we resurrect before we check the
-- types, but do not modify the new context entries
@@ -220,7 +264,7 @@ checkLambda (Arg _ (A.TLet _ lbs)) body target =
checkLambda (Arg info (A.TBind _ xs typ)) body target = do
let numbinds = length xs
TelV tel btyp <- telViewUpTo numbinds target
- if size tel < size xs || numbinds /= 1
+ if size tel < numbinds || numbinds /= 1
then dontUseTargetType
else useTargetType tel btyp
where
@@ -235,23 +279,29 @@ checkLambda (Arg info (A.TBind _ xs typ)) body target = do
-- body, we first unify (xs : argsT) → ?t₁ with the target type. If this
-- is inconclusive we need to block the resulting term so we create a
-- fresh problem for the check.
- t1 <- addCtxs xs argsT $ workOnTypes newTypeMeta_
- let tel = telFromList $ bindsToTel xs argsT
+ let tel = telFromList $ bindsWithHidingToTel xs argsT
+ -- DONT USE tel for addContext, as it loses NameIds.
+ -- WRONG: t1 <- addContext tel $ workOnTypes newTypeMeta_
+ t1 <- addContext (xs, argsT) $ workOnTypes newTypeMeta_
-- Do not coerce hidden lambdas
- if (getHiding info /= NotHidden) then do
+ if notVisible info || any notVisible xs then do
pid <- newProblem_ $ leqType (telePi tel t1) target
-- Now check body : ?t₁
- v <- addCtxs xs argsT $ checkExpr body t1
+ -- WRONG: v <- addContext tel $ checkExpr body t1
+ v <- addContext (xs, argsT) $ checkExpr body t1
-- Block on the type comparison
blockTermOnProblem target (teleLam tel v) pid
else do
-- Now check body : ?t₁
- v <- addCtxs xs argsT $ checkExpr body t1
+ -- WRONG: v <- addContext tel $ checkExpr body t1
+ v <- addContext (xs, argsT) $ checkExpr body t1
-- Block on the type comparison
coerce (teleLam tel v) (telePi tel t1) target
useTargetType tel@(ExtendTel arg (Abs y EmptyTel)) btyp = do
verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type"
+ -- merge in the hiding info of the TBind
+ info <- return $ mapHiding (mappend h) info
unless (getHiding arg == getHiding info) $ typeError $ WrongHidingInLambda target
-- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given
let r = getRelevance info
@@ -265,11 +315,76 @@ checkLambda (Arg info (A.TBind _ xs typ)) body target = do
v <- add y (Dom (setRelevance r' info) argT) $ checkExpr body btyp
blockTermOnProblem target (Lam info $ Abs (nameToArgName x) v) pid
where
- [x] = xs
+ [WithHiding h x] = xs
add y dom | isNoName x = addContext (y, dom)
| otherwise = addContext (x, dom)
useTargetType _ _ = __IMPOSSIBLE__
+-- | Checking a lambda whose domain type has already been checked.
+checkPostponedLambda :: I.Arg ([WithHiding Name], Maybe Type) -> A.Expr -> Type -> TCM Term
+checkPostponedLambda args@(Arg _ ([] , _ )) body target = do
+ checkExpr body target
+checkPostponedLambda args@(Arg info (WithHiding h x : xs, mt)) body target = do
+ let postpone _ t = postponeTypeCheckingProblem_ $ CheckLambda args body t
+ lamHiding = mappend h $ getHiding info
+ insertHiddenLambdas lamHiding target postpone $ \ t@(El _ (Pi dom b)) -> do
+ -- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given
+ let r = getRelevance info -- relevance of lambda
+ r' = getRelevance dom -- relevance of function type
+ info' = setHiding lamHiding $ setRelevance r' info
+ when (r == Irrelevant && r' /= r) $
+ typeError $ WrongIrrelevanceInLambda target
+ -- We only need to block the final term on the argument type
+ -- comparison. The body will be blocked if necessary. We still want to
+ -- compare the argument types first, so we spawn a new problem for that
+ -- check.
+ mpid <- caseMaybe mt (return Nothing) $ \ ascribedType -> Just <$> do
+ newProblem_ $ leqType (unDom dom) ascribedType
+ -- We type-check the body with the ascribedType given by the user
+ -- to get better error messages.
+ -- Using the type dom from the usage context would be more precise,
+ -- though.
+ let add dom | isNoName x = addContext (absName b, dom)
+ | otherwise = addContext (x, dom)
+ v <- add (maybe dom (dom $>) mt) $
+ checkPostponedLambda (Arg info (xs, mt)) body $ absBody b
+ let v' = Lam info' $ Abs (nameToArgName x) v
+ maybe (return v') (blockTermOnProblem t v') mpid
+
+
+-- | Insert hidden lambda until the hiding info of the domain type
+-- matches the expected hiding info.
+-- Throws 'WrongHidingInLambda'
+insertHiddenLambdas
+ :: Hiding -- ^ Expected hiding.
+ -> Type -- ^ Expected to be a function type.
+ -> (MetaId -> Type -> TCM Term) -- ^ Continuation on blocked type.
+ -> (Type -> TCM Term) -- ^ Continuation when expected hiding found.
+ -- The continuation may assume that the @Type@
+ -- is of the form @(El _ (Pi _ _))@.
+ -> TCM Term -- ^ Term with hidden lambda inserted.
+insertHiddenLambdas h target postpone ret = do
+ -- If the target type is blocked, we postpone,
+ -- because we do not know if a hidden lambda needs to be inserted.
+ ifBlockedType target postpone $ \ t0 -> do
+ let t = ignoreSharing <$> t0
+ case unEl t of
+
+ Pi dom b -> do
+ let h' = getHiding dom
+ -- Found expected hiding: return function type.
+ if h == h' then ret t else do
+ -- Found a visible argument but expected a hidden one:
+ -- That's an error, as we cannot insert a visible lambda.
+ if visible h' then typeError $ WrongHidingInLambda target else do
+ -- Otherwise, we found a hidden argument that we can insert.
+ let x = absName b
+ Lam (domInfo dom) . Abs x <$> do
+ addContext (x, dom) $ insertHiddenLambdas h (absBody b) postpone ret
+
+ _ -> typeError . GenericDocError =<< do
+ text "Expected " <+> prettyTCM target <+> text " to be a function type"
+
-- | @checkAbsurdLambda i h e t@ checks absurd lambda against type @t@.
-- Precondition: @e = AbsurdLam i h@
checkAbsurdLambda :: A.ExprInfo -> Hiding -> A.Expr -> Type -> TCM Term
@@ -573,13 +688,11 @@ checkExpr e t0 =
rx = caseMaybe (rStart re) noRange $ \ pos -> posToRange pos pos
hiddenLambdaOrHole h e = case e of
- A.AbsurdLam _ h' -> h == h'
- A.ExtendedLam _ _ _ cls -> any hiddenLHS cls
- A.Lam _ (A.DomainFree info' _) _ -> h == getHiding info'
- A.Lam _ (A.DomainFull (A.TypedBindings _ (Arg info' _))) _
- -> h == getHiding info'
- A.QuestionMark{} -> True
- _ -> False
+ A.AbsurdLam _ h' -> h == h'
+ A.ExtendedLam _ _ _ cls -> any hiddenLHS cls
+ A.Lam _ bind _ -> h == getHiding bind
+ A.QuestionMark{} -> True
+ _ -> False
hiddenLHS (A.Clause (A.LHS _ (A.LHSHead _ (a : _)) _) _ _) = notVisible a
hiddenLHS _ = False
@@ -651,23 +764,29 @@ checkExpr e t0 =
A.Lit lit -> checkLiteral lit t
A.Let i ds e -> checkLetBindings ds $ checkExpr e t
+ A.Pi _ tel e | null tel -> checkExpr e t
A.Pi _ tel e -> do
- t' <- checkTelescope_ tel $ \tel -> do
+ t' <- checkPiTelescope tel $ \tel -> do
t <- instantiateFull =<< isType_ e
tel <- instantiateFull tel
- return $ telePi tel t
+ let t' = telePi tel t
+ noFunctionsIntoSize t t'
+ return t'
let s = getSort t'
+ v = unEl t'
when (s == Inf) $ reportSDoc "tc.term.sort" 20 $
vcat [ text ("reduced to omega:")
, nest 2 $ text "t =" <+> prettyTCM t'
, nest 2 $ text "cxt =" <+> (prettyTCM =<< getContextTelescope)
]
- coerce (unEl t') (sort s) t
+ coerce v (sort s) t
A.Fun _ (Arg info a) b -> do
a' <- isType_ a
b' <- isType_ b
- s <- reduce $ getSort a' `sLub` getSort b'
- coerce (Pi (convColor $ Dom info a') (NoAbs underscore b')) (sort s) t
+ s <- ptsRule a' b'
+ let v = Pi (convColor $ Dom info a') (NoAbs underscore b')
+ noFunctionsIntoSize b' $ El s v
+ coerce v (sort s) t
A.Set _ n -> do
n <- ifM typeInType (return 0) (return n)
coerce (Sort $ mkType n) (sort $ mkType $ n + 1) t
@@ -812,7 +931,7 @@ checkApplication hd args e t = do
-- by inserting an underscore for the missing type.
domainFree :: A.ArgInfo -> A.Name -> A.LamBinding
domainFree info x =
- A.DomainFull $ A.TypedBindings r $ Arg info $ A.TBind r [x] $ A.Underscore underscoreInfo
+ A.DomainFull $ A.TypedBindings r $ Arg info $ A.TBind r [pure x] $ A.Underscore underscoreInfo
where
r = getRange x
underscoreInfo = A.MetaInfo
@@ -1246,7 +1365,7 @@ checkArguments exh expandIFS r args0@(arg@(Arg info e) : args) t0 t1 =
-- c) We inserted implicits, but did not find his one.
| otherwise = lift $ typeError $ WrongNamedArgument arg
- -- (t0', cs) <- forcePi h (name e) t0
+ -- t0' <- lift $ forcePi (getHiding info) (maybe "_" rangedThing $ nameOf e) t0'
case ignoreSharing $ unEl t0' of
Pi (Dom info' a) b
| getHiding info == getHiding info'
@@ -1352,7 +1471,10 @@ isModuleFreeVar i = do
-- @{tel} -> D vs@ for some datatype @D@ then insert the hidden
-- arguments. Otherwise, leave the type polymorphic.
inferExprForWith :: A.Expr -> TCM (Term, Type)
-inferExprForWith e = traceCall (InferExpr e) $ do
+inferExprForWith e = do
+ reportSDoc "tc.with.infer" 20 $ text "inferExprforWith " <+> prettyTCM e
+ reportSLn "tc.with.infer" 80 $ "inferExprforWith " ++ show e
+ traceCall (InferExpr e) $ do
-- With wants type and term fully instantiated!
(v, t) <- instantiateFull =<< inferExpr e
v0 <- reduce v
@@ -1402,7 +1524,7 @@ checkLetBinding b@(A.LetPatBind i p e) ret =
, text "t =" <+> prettyTCM t
]
]
- checkLeftHandSide (CheckPattern p EmptyTel t) Nothing [p0] t0 $ \ (LHSResult mgamma delta sub xs ps t' perm) -> do
+ checkLeftHandSide (CheckPattern p EmptyTel t) Nothing [p0] t0 $ \ (LHSResult delta ps _t _perm) -> do
-- A single pattern in internal syntax is returned.
let p = case ps of [p] -> namedArg p; _ -> __IMPOSSIBLE__
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat