summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/LevelConstraints.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/LevelConstraints.hs')
-rw-r--r--src/full/Agda/TypeChecking/LevelConstraints.hs6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/full/Agda/TypeChecking/LevelConstraints.hs b/src/full/Agda/TypeChecking/LevelConstraints.hs
index b0f87e6..15ff4ec 100644
--- a/src/full/Agda/TypeChecking/LevelConstraints.hs
+++ b/src/full/Agda/TypeChecking/LevelConstraints.hs
@@ -2,7 +2,7 @@
module Agda.TypeChecking.LevelConstraints ( simplifyLevelConstraint ) where
-import Data.List as List
+import qualified Data.List as List
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Substitute
@@ -35,8 +35,8 @@ matchLeq (a :=< b) (c :=< d)
| length xs == length ys = (a, b) == applySubst rho (c, d)
| otherwise = False
where
- free :: Free' a [Int] => a -> [Int]
- free = nub . runFree ((:[]) . fst) IgnoreNot
+ free :: Free a => a -> [Int]
+ free = List.nub . runFree (:[]) IgnoreNot -- Note: use a list to preserve order of variables
xs = free (a, b)
ys = free (c, d)
rho = mkSub $ List.sort $ zip ys xs