summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Rules/LHS/Unify.hs')
-rw-r--r--src/full/Agda/TypeChecking/Rules/LHS/Unify.hs132
1 files changed, 86 insertions, 46 deletions
diff --git a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
index e2a9166..baa40e7 100644
--- a/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
+++ b/src/full/Agda/TypeChecking/Rules/LHS/Unify.hs
@@ -1,14 +1,13 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE DeriveFoldable #-}
-{-# LANGUAGE DeriveFunctor #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TupleSections #-}
module Agda.TypeChecking.Rules.LHS.Unify where
@@ -42,11 +41,11 @@ import Agda.TypeChecking.Monad.Exception
import Agda.TypeChecking.Monad.Builtin (constructorForm)
import Agda.TypeChecking.Conversion -- equalTerm
import Agda.TypeChecking.Constraints
+import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.DropArgs
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Reduce
-import Agda.TypeChecking.Pretty hiding (empty)
-import qualified Agda.TypeChecking.Pretty as P
+import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute hiding (Substitution)
import qualified Agda.TypeChecking.Substitute as S
import Agda.TypeChecking.Telescope
@@ -63,7 +62,7 @@ import Agda.Utils.Except
( Error(noMsg, strMsg)
, MonadError(catchError, throwError)
)
-
+import Agda.Utils.Either
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
@@ -72,8 +71,23 @@ import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
-newtype Unify a = U { unUnify :: ReaderT UnifyEnv (WriterT UnifyOutput (ExceptionT UnifyException (StateT UnifyState TCM))) a }
- deriving (Monad, MonadIO, Functor, Applicative, MonadException UnifyException, MonadWriter UnifyOutput)
+-- | Result of 'unifyIndices'.
+type UnificationResult = UnificationResult' Substitution
+
+data UnificationResult' a
+ = Unifies a -- ^ Unification succeeded.
+ | NoUnify TCErr -- ^ Terms are not unifiable.
+ | DontKnow TCErr -- ^ Some other error happened, unification got stuck.
+ deriving (Typeable, Show, Functor, Foldable, Traversable)
+
+-- | Monad for unification.
+newtype Unify a = U { unUnify ::
+ ReaderT UnifyEnv (
+ WriterT UnifyOutput (
+ ExceptionT UnifyException (
+ StateT UnifyState TCM))) a
+ } deriving ( Monad, MonadIO, Functor, Applicative
+ , MonadException UnifyException, MonadWriter UnifyOutput)
instance MonadTCM Unify where
liftTCM = U . lift . lift . lift . lift
@@ -163,8 +177,24 @@ constructorMismatch :: Type -> Term -> Term -> Unify a
constructorMismatch a u v = throwException $ ConstructorMismatch a u v
constructorMismatchHH :: TypeHH -> Term -> Term -> Unify a
-constructorMismatchHH aHH = constructorMismatch (leftHH aHH)
- -- do not report heterogenity
+constructorMismatchHH aHH u v = do
+ ifM (liftTCM fullyApplied `and2M` canCompare aHH)
+ {- then -} (constructorMismatch (leftHH aHH) u v) -- do not report heterogenity
+ {- else -} (throwException (UnclearOccurrence (leftHH aHH) u v))
+ where
+ -- Comparing constructors at different types is incompatible with univalence
+ canCompare (Het s t) = ifM (liftTCM $ optWithoutK <$> pragmaOptions)
+ (liftTCM $ tryConversion $ equalType s t) -- no constraints left
+ (return True)
+ canCompare Hom{} = return True
+ -- Issue 1497: only fully applied constructors can mismatch
+ fullyApplied = case (ignoreSharing u, ignoreSharing v) of
+ (Con c us, Con d vs) -> do
+ when (c == d) __IMPOSSIBLE__
+ car <- fromLeft length <$> getConstructorArity (conName c)
+ dar <- fromLeft length <$> getConstructorArity (conName d)
+ return $ length us == car && length vs == dar
+ _ -> return True -- could be literals
instance Subst Equality where
applySubst rho (Equal a s t) =
@@ -221,6 +251,13 @@ forceHom (Het a1 a2) = a1 <$ do noConstraints $ equalType a1 a2
makeHom :: TypeHH -> TCM (Maybe Type)
makeHom aHH = (Just <$> forceHom aHH) `catchError` \ err -> return Nothing
+-- | Try to make a possibly heterogeneous term situation homogeneous.
+tryHom :: TypeHH -> Term -> Term -> TCM TermHH
+tryHom aHH u v = do
+ a <- forceHom aHH
+ Hom u <$ checkEquality a u v
+ `catchError` \ err -> return $ Het u v
+
addEquality :: Type -> Term -> Term -> Unify ()
addEquality a = addEqualityHH (Hom a)
@@ -348,12 +385,7 @@ flattenSubstitution s = foldr instantiate s is
-- @inst i u v@ replaces index @i@ in @v@ by @u@, without removing the index.
inst :: Nat -> Term -> Term -> Term
inst i u v = applySubst us v
- where us = [var j | j <- [0..i - 1] ] ++# u :# raiseS (i + 1)
-
-data UnificationResult
- = Unifies Substitution
- | NoUnify Type Term Term
- | DontKnow TCErr
+ where us = [ var j | j <- [0..i - 1] ] ++# consS u (raiseS $ i + 1)
-- | Are we in a homogeneous (one type) or heterogeneous (two types) situation?
data HomHet a
@@ -472,7 +504,7 @@ unifyIndices_ flex a us vs = liftTCM $ do
case r of
Unifies sub -> return sub
DontKnow err -> throwError err
- NoUnify a u v -> typeError $ UnequalTerms CmpEq u v a
+ NoUnify err -> throwError err
unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult
unifyIndices flex a us vs = liftTCM $ do
@@ -493,9 +525,9 @@ unifyIndices flex a us vs = liftTCM $ do
recheckEqualities
case r of
- Left (ConstructorMismatch a u v) -> return $ NoUnify a u v
+ Left (ConstructorMismatch a u v) -> noUnify a u v
-- Andreas 2011-04-14:
- Left (StronglyRigidOccurrence a u v) -> return $ NoUnify a u v
+ Left (StronglyRigidOccurrence a u v) -> noUnify a u v
Left (UnclearOccurrence a u v) -> typeError $ UnequalTerms CmpEq u v a
Left (WithoutKException a u v) -> typeError $ WithoutKError a u v
Left (GenericUnifyException err) -> typeError $ GenericError err
@@ -507,6 +539,8 @@ unifyIndices flex a us vs = liftTCM $ do
TypeError _ (Closure {clValue = WithoutKError{}}) -> throwError err
_ -> return $ DontKnow err
where
+ noUnify a u v = NoUnify <$> do typeError_ $ UnequalTerms CmpEq u v a
+
flex' = map flexVar flex
flexible i = i `elem` flex'
findFlexible i = find ((i ==) . flexVar) flex
@@ -561,7 +595,7 @@ unifyIndices flex a us vs = liftTCM $ do
-- , nest 2 $ parens (prettyTCM tel0)
, nest 2 $ prettyList $ map prettyTCM us0
, nest 2 $ prettyList $ map prettyTCM vs0
- , nest 2 $ text "at telescope" <+> prettyTCM bHH <+> text "..."
+ , nest 2 $ text "at telescope" <+> prettyTCM bHH <+> text ("(" ++ show (getRelevance a) ++ ") ...")
]
liftTCM $ reportSDoc "tc.lhs.unify" 25 $
(text $ "tel0 = " ++ show tel0)
@@ -571,7 +605,11 @@ unifyIndices flex a us vs = liftTCM $ do
-- in case of dependent function type, we cannot postpone
-- unification of u and v, otherwise us or vs might be ill-typed
-- skip irrelevant parts
- uHH <- if isIrrelevant a then return $ Hom u else
+ uHH <- if getRelevance a == Irrelevant then return $ Hom u else
+ -- Andreas, 2015-01-19 Forced constructor arguments are not unified.
+ -- Andreas, 2015-02-26 Restricting this to big forced arguments;
+ -- this still addresses issue 1406.
+ if getRelevance a == Forced Big then liftTCM $ tryHom bHH u v else
ifClean (unifyHH bHH u v) (return $ Hom u) (return $ Het u v)
liftTCM $ reportSDoc "tc.lhs.unify" 25 $
@@ -755,9 +793,9 @@ unifyIndices flex a us vs = liftTCM $ do
liftTCM $ reportSDoc "tc.lhs.unify" 15 $
sep [ text "unifyAtom"
- , nest 2 $ prettyTCM u <> if flexibleTerm u then text " (flexible)" else P.empty
+ , nest 2 $ prettyTCM u <> if flexibleTerm u then text " (flexible)" else empty
, nest 2 $ text "=?="
- , nest 2 $ prettyTCM v <> if flexibleTerm v then text " (flexible)" else P.empty
+ , nest 2 $ prettyTCM v <> if flexibleTerm v then text " (flexible)" else empty
, nest 2 $ text ":" <+> prettyTCM aHH
]
liftTCM $ reportSDoc "tc.lhs.unify" 60 $
@@ -793,18 +831,18 @@ unifyIndices flex a us vs = liftTCM $ do
| c == c' -> do
r <- liftTCM (dataOrRecordTypeHH' c aHH)
case r of
- Just (d, bHH) -> do
- bHH <- ureduce bHH
+ Just (d, b, parsIxsHH) -> do
+ (b, parsIxsHH) <- ureduce (b, parsIxsHH)
-- Jesper, 2014-05-03: When --without-K is enabled, we reconstruct
-- datatype indices and unify them as well
withoutKEnabled <- liftTCM $ optWithoutK <$> pragmaOptions
- when withoutKEnabled (do
+ when withoutKEnabled $ do
def <- liftTCM $ getConstInfo d
- let parsHH = fmap (\(b, pars, ixs) -> pars) bHH
- ixsHH = fmap (\(b, pars, ixs) -> ixs) bHH
- dtypeHH = (defType def) `applyHH` parsHH
- unifyConstructorArgs dtypeHH (leftHH ixsHH) (rightHH ixsHH))
- let a'HH = fmap (\(b, pars, _) -> b `apply` pars) bHH
+ let parsHH = fst <$> parsIxsHH
+ ixsHH = snd <$> parsIxsHH
+ dtypeHH = defType def `applyHH` parsHH
+ unifyConstructorArgs dtypeHH (leftHH ixsHH) (rightHH ixsHH)
+ let a'HH = (b `apply`) . fst <$> parsIxsHH
unifyConstructorArgs a'HH us vs
Nothing -> checkEqualityHH aHH u v
| otherwise -> constructorMismatchHH aHH u v
@@ -989,22 +1027,24 @@ dataOrRecordTypeHH c (Het a1 a2) = do
dataOrRecordTypeHH' ::
ConHead
-> TypeHH
- -> TCM (Maybe (QName, HomHet (Type, Args, Args)))
+ -> TCM (Maybe (QName, Type, HomHet (Args, Args)))
dataOrRecordTypeHH' c (Hom a) = do
r <- dataOrRecordType' c a
case r of
- Just (d, a', pars, ixs) -> return $ Just (d, Hom (a', pars, ixs))
+ Just (d, a', pars, ixs) -> return $ Just (d, a', Hom (pars, ixs))
Nothing -> return $ Nothing
dataOrRecordTypeHH' c (Het a1 a2) = do
r1 <- dataOrRecordType' c a1
r2 <- dataOrRecordType' c a2
- return $ case (r1, r2) of
- -- TODO: We should always have b1 == b2, check/force this in some way?
- (Just (d1, b1, pars1, ixs1), Just (d2, b2, pars2, ixs2)) | d1 == d2 -> Just $
+ case (r1, r2) of
+ (Just (d1, b1, pars1, ixs1), Just (d2, b2, pars2, ixs2)) | d1 == d2 -> do
+ -- Same constructors have same types, of course.
+ unless (b1 == b2) __IMPOSSIBLE__
+ return $ Just $
if null pars1 && null pars2 && null ixs1 && null ixs2
- then (d1, Hom (b1, [], []))
- else (d1, Het (b1, pars1, ixs1) (b2, pars2, ixs2))
- _ -> Nothing
+ then (d1, b1, Hom ([], []))
+ else (d1, b1, Het (pars1, ixs1) (pars2, ixs2))
+ _ -> return Nothing
-- | Return record type identifier if argument is a record type.