[ rewriting ] Use typed conversion for non-linear rewrite rules

src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs

@@ -44,13 +44,14 @@ import Agda.Syntax.Common
 import qualified Agda.Syntax.Common as C
 import Agda.Syntax.Internal
 
+import Agda.TypeChecking.Conversion.Pure
 import Agda.TypeChecking.Datatypes
 import Agda.TypeChecking.EtaContract
 import Agda.TypeChecking.Free
 import Agda.TypeChecking.Free.Reduce
 import Agda.TypeChecking.Level
 import Agda.TypeChecking.Monad
-import Agda.TypeChecking.Monad.Builtin (getBuiltin', builtinLevel, primLevelSuc, primLevelMax)
+import Agda.TypeChecking.Monad.Builtin (HasBuiltins(..), getBuiltin', builtinLevel, primLevelSuc, primLevelMax)
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Records
 import Agda.TypeChecking.Reduce
@@ -234,23 +235,23 @@ runNLM nlm = do
 matchingBlocked :: Blocked_ -> NLM ()
 matchingBlocked = throwError
 
--- | Add substitution @i |-> v@ to result of matching.
-tellSub :: Relevance -> Int -> Term -> NLM ()
-tellSub r i v = do
+-- | Add substitution @i |-> v : a@ to result of matching.
+tellSub :: Relevance -> Int -> Type -> Term -> NLM ()
+tellSub r i a v = do
   old <- IntMap.lookup i <$> use nlmSub
   case old of
     Nothing -> nlmSub %= IntMap.insert i (r,v)
     Just (r',v')
       | isIrrelevant r  -> return ()
       | isIrrelevant r' -> nlmSub %= IntMap.insert i (r,v)
-      | otherwise       -> whenJustM (equal v v') matchingBlocked
+      | otherwise       -> whenJustM (equal a v v') matchingBlocked
 
-tellEq :: Telescope -> Telescope -> Term -> Term -> NLM ()
-tellEq gamma k u v = do
+tellEq :: Telescope -> Telescope -> Type -> Term -> Term -> NLM ()
+tellEq gamma k a u v = do
   traceSDoc "rewriting.match" 30 (sep
                [ "adding equality between" <+> addContext (gamma `abstract` k) (prettyTCM u)
                , " and " <+> addContext k (prettyTCM v) ]) $ do
-  nlmEqs %= (PostponedEquation k u v:)
+  nlmEqs %= (PostponedEquation k a u v:)
 
 type Sub = IntMap (Relevance, Term)
 
@@ -259,6 +260,7 @@ type Sub = IntMap (Relevance, Term)
 --   the substitution computed by matching.
 data PostponedEquation = PostponedEquation
   { eqFreeVars :: Telescope -- ^ Telescope of free variables in the equation
+  , eqType :: Type    -- ^ Type of the equation, living in same context as the rhs.
   , eqLhs :: Term     -- ^ Term from pattern, living in pattern context.
   , eqRhs :: Term     -- ^ Term from scrutinee, living in context where matching was invoked.
   }
@@ -382,7 +384,7 @@ instance Match Type NLPat Term where
         case ok of
           Left b         -> block b
           Right Nothing  -> no ""
-          Right (Just v) -> tellSub r (i-n) $ teleLam tel $ renameP __IMPOSSIBLE__ perm v
+          Right (Just v) -> tellSub r (i-n) t $ teleLam tel $ renameP __IMPOSSIBLE__ perm v
       _ | MetaV m es <- v -> matchingBlocked $ Blocked m ()
       PDef f ps -> traceSDoc "rewriting.match" 60 ("matching a PDef" <+> prettyTCM f) $ do
         v <- addContext k $ constructorForm =<< unLevel v
@@ -447,7 +449,7 @@ instance Match Type NLPat Term where
           match r gamma k (ct, Con c ci []) (map Apply ps') (map Apply vs)
         _ -> no ""
       PTerm u -> traceSDoc "rewriting.match" 60 ("matching a PTerm" <+> addContext (gamma `abstract` k) (prettyTCM u)) $
-        tellEq gamma k u v
+        tellEq gamma k t u v
 
 -- Checks if the given term contains any free variables that satisfy the
 -- given condition on their DBI, possibly reducing the term in the process.
@@ -487,18 +489,18 @@ makeSubstitution gamma sub =
                 Just (_         , v) -> Just v
                 Nothing              -> Nothing
 
-checkPostponedEquations :: (MonadReduce m, MonadAddContext m, HasConstInfo m, MonadDebug m)
+checkPostponedEquations :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, MonadDebug m)
                         => Substitution -> PostponedEquations -> m (Maybe Blocked_)
 checkPostponedEquations sub eqs = forM' eqs $
-  \ (PostponedEquation k lhs rhs) -> do
+  \ (PostponedEquation k a lhs rhs) -> do
       let lhs' = applySubst (liftS (size k) sub) lhs
       traceSDoc "rewriting.match" 30 (sep
         [ "checking postponed equality between" , addContext k (prettyTCM lhs')
         , " and " , addContext k (prettyTCM rhs) ]) $ do
-      addContext k $ equal lhs' rhs
+      addContext k $ equal a lhs' rhs
 
 -- main function
-nonLinMatch :: (MonadReduce m, MonadAddContext m, HasConstInfo m, MonadDebug m, Match t a b)
+nonLinMatch :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m, MonadDebug m, Match t a b)
             => Telescope -> t -> a -> b -> m (Either Blocked_ Substitution)
 nonLinMatch gamma t p v = do
   let no msg b = traceSDoc "rewriting.match" 10 (sep
@@ -513,23 +515,21 @@ nonLinMatch gamma t p v = do
       Nothing -> return $ Right sub
       Just b  -> no "checking of postponed equations" b
 
--- | Untyped βη-equality, does not handle things like empty record types.
+-- | Typed βη-equality, also handles empty record types.
 --   Returns `Nothing` if the terms are equal, or `Just b` if the terms are not
 --   (where b contains information about possible metas blocking the comparison)
-
--- TODO: implement a type-directed, lazy version of this function.
-equal :: (MonadReduce m, HasConstInfo m)
-      => Term -> Term -> m (Maybe Blocked_)
-equal u v = do
-  (u, v) <- etaContract =<< normalise (u, v)
-  let ok    = u == v
-      metas = allMetas (u, v)
-      block = caseMaybe (headMaybe metas)
-                (NotBlocked ReallyNotBlocked ())
-                (\m -> Blocked m ())
-  if ok then return Nothing else do
-    traceSDoc "rewriting.match" 10 (sep
+equal :: (MonadReduce m, MonadAddContext m, HasConstInfo m, HasBuiltins m)
+      => Type -> Term -> Term -> m (Maybe Blocked_)
+equal a u v = pureEqualTerm a u v >>= \case
+  True -> return Nothing
+  False -> traceSDoc "rewriting.match" 10 (sep
       [ "mismatch between " <+> prettyTCM u
       , " and " <+> prettyTCM v
       ]) $ do
     return $ Just block
+
+  where
+    metas = allMetas (u, v)
+    block = caseMaybe (headMaybe metas)
+              (NotBlocked ReallyNotBlocked ())
+              (\m -> Blocked m ())