summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Monad/Context.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Monad/Context.hs')
-rw-r--r--src/full/Agda/TypeChecking/Monad/Context.hs24
1 files changed, 21 insertions, 3 deletions
diff --git a/src/full/Agda/TypeChecking/Monad/Context.hs b/src/full/Agda/TypeChecking/Monad/Context.hs
index 54c6671..e897bea 100644
--- a/src/full/Agda/TypeChecking/Monad/Context.hs
+++ b/src/full/Agda/TypeChecking/Monad/Context.hs
@@ -1,7 +1,10 @@
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TupleSections #-}
+
+#if __GLASGOW_HASKELL__ <= 708
{-# LANGUAGE OverlappingInstances #-}
+#endif
module Agda.TypeChecking.Monad.Context where
@@ -9,6 +12,7 @@ import Control.Monad.Reader
import Data.List hiding (sort)
import qualified Data.Map as Map
+import Data.Monoid
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
@@ -88,7 +92,11 @@ addCtx x a ret = do
class AddContext b where
addContext :: MonadTCM tcm => b -> tcm a -> tcm a
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPABLE #-} AddContext a => AddContext [a] where
+#else
instance AddContext a => AddContext [a] where
+#endif
addContext = flip (foldr addContext)
instance AddContext (Name, Dom Type) where
@@ -101,6 +109,12 @@ instance AddContext (Dom (Name, Type)) where
instance AddContext ([Name], Dom Type) where
addContext (xs, dom) = addContext (bindsToTel' id xs dom)
+instance AddContext ([WithHiding Name], Dom Type) where
+ addContext ([] , dom) = id
+ addContext (WithHiding h x : xs, dom) =
+ addContext (x , mapHiding (mappend h) dom) .
+ addContext (xs, raise 1 dom)
+
instance AddContext (String, Dom Type) where
addContext (s, dom) ret = do
x <- freshName_ s
@@ -113,7 +127,11 @@ instance AddContext (Dom (String, Type)) where
instance AddContext Name where
addContext x = addContext (x, dummyDom)
+#if __GLASGOW_HASKELL__ >= 710
+instance {-# OVERLAPPING #-} AddContext String where
+#else
instance AddContext String where
+#endif
addContext s = addContext (s, dummyDom)
instance AddContext Telescope where