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.hs14
1 files changed, 5 insertions, 9 deletions
diff --git a/src/full/Agda/TypeChecking/SyntacticEquality.hs b/src/full/Agda/TypeChecking/SyntacticEquality.hs
index 7fe28ee..49f04cc 100644
--- a/src/full/Agda/TypeChecking/SyntacticEquality.hs
+++ b/src/full/Agda/TypeChecking/SyntacticEquality.hs
@@ -1,8 +1,4 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UndecidableInstances #-}
-- | A syntactic equality check that takes meta instantiations into account,
@@ -102,7 +98,7 @@ instance SynEq Term where
-- TODO: preserve sharing!
case (ignoreSharing v, ignoreSharing v') of
(Var i vs, Var i' vs') | i == i' -> Var i <$$> synEq vs vs'
- (Con c vs, Con c' vs') | c == c' -> Con c <$$> synEq vs vs'
+ (Con c ci vs,Con c' ci' vs') | c == c' -> Con c (bestConInfo ci ci') <$$> synEq vs vs'
(Def f vs, Def f' vs') | f == f' -> Def f <$$> synEq vs vs'
(MetaV x vs, MetaV x' vs') | x == x' -> MetaV x <$$> synEq vs vs'
(Lit l , Lit l' ) | l == l' -> pure2 $ v
@@ -168,7 +164,7 @@ instance SynEq a => SynEq [a] where
instance SynEq a => SynEq (Elim' a) where
synEq e e' =
case (e, e') of
- (Proj f , Proj f' ) | f == f' -> pure2 e
+ (Proj _ f, Proj _ f') | f == f' -> pure2 e
(Apply a, Apply a') -> Apply <$$> synEq a a'
_ -> inequal (e, e')
@@ -197,6 +193,6 @@ instance SynEq a => SynEq (Dom a) where
synEq (Dom ai a) (Dom ai' a') = Dom <$$> synEq ai ai' <**> synEq a a'
instance SynEq ArgInfo where
- synEq ai@(ArgInfo h r) ai'@(ArgInfo h' r')
- | h == h', r == r' = pure2 ai
- | otherwise = inequal (ai, ai')
+ synEq ai@(ArgInfo h r o v) ai'@(ArgInfo h' r' o' v')
+ | h == h', r == r', v == v' = pure2 ai
+ | otherwise = inequal (ai, ai')