@@ -100,8 +100,12 @@ instance {-# OVERLAPS #-} Updatable v t ((v ':-> s) ': m) ((v ':-> t) ': m) wher
100100instance Updatable v t m n => Updatable v t ((w ':-> y) ': m) ((w ':-> y) ': n) where
101101 update (Ext w y m) v x = Ext w y (update m v x)
102102
103−instance Updatable v t '[] '[v ':-> t] where
104− update Empty v x = Ext v x Empty
103+-- instance Updatable v t '[] '[v ':-> t] where
104+-- update Empty v x = Ext v x Empty
105+
106+instance Updatable v t s ((v ':-> t) ': s) where
107+ update xs v x = Ext v x xs
108+
105109
106110{-| Predicate to check if in normalised map form -}
107111type IsMap s = (s ~ Nub (Sort s))
@@ -129,8 +133,14 @@ instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s))
129133instance Eq (Map '[]) where
130134 Empty == Empty = True
131135
132−instance (KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
133− (Ext k v m) == (Ext k' v' m') = k == k' && v == v' && m == m'
136+instance (Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
137+ (Ext Var v m) == (Ext Var v' m') = v == v' && m == m'
138+
139+instance Ord (Map '[]) where
140+ compare Empty Empty = EQ
141+
142+instance (Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) where
143+ compare (Ext Var v m) (Ext Var v' m') = compare v v' `mappend` compare m m'
134144
135145{-| Union of two finite maps (normalising) -}
136146union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)