[ Issue 1652 ] Added a note to the changelog.

doc/release-notes/2-4-4.txt

@@ -199,6 +199,14 @@ Pragmas and options
   If used with the OPTIONS pragma it will not affect records defined
   in other modules.
 
+* The semantics of {-# REWRITE r #-} pragmas in parametrized modules has
+  changed (see Issue 1652).
+
+  Rewrite rules are no longer lifted to the top context. Instead, they now only
+  apply to terms in (extensions of) the module context. If you want the old
+  behaviour, you should put the {-# REWRITE r #-} pragma outside of the module
+  (i.e. unindent it).
+
 
 Language
 ========

src/full/Agda/TypeChecking/DefinitionalEquality.agda

@@ -0,0 +1,22 @@
+module Agda.TypeChecking.DefinitionalEquality where
+
+import Data.Monoid
+
+import Agda.Syntax.Common
+import Agda.Syntax.Internal
+
+import Agda.TypeChecking.Reduce
+import Agda.TypeChecking.Reduce.Monad
+
+import Agda.Utils.Except
+
+type DefEqM = ExceptT Blocked_ (WriterT All ReduceM)
+
+liftRed :: ReduceM a -> DefEqM a
+liftRed = lift . lift
+
+class DefEq t a | a -> t where
+  defEq  :: t -> a -> a -> DefEqM (t,a,a)
+
+instance DefEq Type Term where
+  defEq t a b =

src/full/Agda/TypeChecking/DefinitionalEquality.hs

@@ -0,0 +1,64 @@
+{-# LANGUAGE CPP #-}
+
+module Agda.TypeChecking.DefinitionalEquality where
+
+import Data.Monoid
+
+import Agda.Syntax.Common
+import Agda.Syntax.Internal
+
+import Agda.TypeChecking.Reduce
+import Agda.TypeChecking.Reduce.Monad
+
+import Agda.Utils.Except
+
+#include "undefined.h"
+import Agda.Utils.Impossible
+
+-- | A type-directed definitional equality check that takes eta into account,
+--   and reduces terms when needed. It replaces
+--   @
+--      (v, v') <- normalise (v, v')
+--      v == v'
+--   @
+--   by a more efficient routine that also checks eta rules and produces the
+--   proper blocking tags when it encounters unsolved metas.
+
+type DefEqM = ExceptT Blocked_ (WriterT All ReduceM)
+
+blockedOnMeta :: MetaId -> DefEqM a
+blockedOnMeta m = throwError $ Blocked m ()
+
+tellNotEqual :: DefEqM ()
+tellNotEqual = lift $ tell $ All False
+
+liftRed :: ReduceM a -> DefEqM a
+liftRed = lift . lift
+
+class DefEq a t | t -> a where
+  defEq  :: a -> t -> t -> DefEqM (a,t,t)
+
+instance DefEq Type Term where
+  defEq a u v = do
+    ((u,v), equal) <- liftRed $ checkSyntacticEquality u v
+    if equal then return (a,u,v) else do
+    (a,u,v) <- liftRed $ reduce' (a,u,v)
+    case ignoreSharing (unEl a) of
+    -- TODO sizes
+    -- TODO levels
+        Var i es   -> ???
+        Lam _ _    -> __IMPOSSIBLE__
+        Lit _      -> __IMPOSSIBLE__
+        Def r es   -> do
+          isrec <- isEtaRecord r
+          if isrec then do
+            ???
+            else
+        Con _ _    -> __IMPOSSIBLE__
+        Pi a b     -> ???
+        Sort s     -> ???
+        Level _    -> __IMPOSSIBLE__
+        MetaV m es -> blockedOnMeta m
+        DontCare
+
+