summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/SyntacticEquality.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/SyntacticEquality.hs')
-rw-r--r--src/full/Agda/TypeChecking/SyntacticEquality.hs16
1 files changed, 8 insertions, 8 deletions
diff --git a/src/full/Agda/TypeChecking/SyntacticEquality.hs b/src/full/Agda/TypeChecking/SyntacticEquality.hs
index 7e0f152..08adab8 100644
--- a/src/full/Agda/TypeChecking/SyntacticEquality.hs
+++ b/src/full/Agda/TypeChecking/SyntacticEquality.hs
@@ -1,9 +1,8 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TupleSections #-}
-- | A syntactic equality check that takes meta instantiations into account,
-- but does not reduce. It replaces
@@ -131,9 +130,10 @@ instance SynEq LevelAtom where
l <- lift (unBlock =<< instantiate l)
case (l, l') of
(MetaLevel m vs , MetaLevel m' vs' ) | m == m' -> MetaLevel m <$$> synEq vs vs'
- (NeutralLevel v , NeutralLevel v' ) -> NeutralLevel <$$> synEq v v'
(UnreducedLevel v, UnreducedLevel v' ) -> UnreducedLevel <$$> synEq v v'
- (BlockedLevel m v, BlockedLevel m' v') | m == m' -> BlockedLevel m <$$> synEq v v'
+ -- The reason for being blocked should not matter for equality.
+ (NeutralLevel r v, NeutralLevel r' v') -> NeutralLevel r <$$> synEq v v'
+ (BlockedLevel m v, BlockedLevel m' v') -> BlockedLevel m <$$> synEq v v'
_ -> inequal (l, l')
where
unBlock l =