summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/Test/Generators.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/Test/Generators.hs')
-rw-r--r--src/full/Agda/TypeChecking/Test/Generators.hs14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/full/Agda/TypeChecking/Test/Generators.hs b/src/full/Agda/TypeChecking/Test/Generators.hs
index dbd1ddc..a35e969 100644
--- a/src/full/Agda/TypeChecking/Test/Generators.hs
+++ b/src/full/Agda/TypeChecking/Test/Generators.hs
@@ -1,9 +1,8 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.Test.Generators where
@@ -433,8 +432,8 @@ instance ShrinkC a b => ShrinkC (I.Dom a) (I.Dom b) where
noShrink = fmap noShrink
instance ShrinkC a b => ShrinkC (Blocked a) (Blocked b) where
- shrinkC conf (Blocked m x) = Blocked m <$> shrinkC conf x
- shrinkC conf (NotBlocked x) = NotBlocked <$> shrinkC conf x
+ shrinkC conf (Blocked m x) = Blocked m <$> shrinkC conf x
+ shrinkC conf (NotBlocked r x) = NotBlocked r <$> shrinkC conf x
noShrink = fmap noShrink
instance ShrinkC a b => ShrinkC (Elim' a) (Elim' b) where
@@ -449,6 +448,7 @@ instance ShrinkC Sort Sort where
Type n -> [] -- No Level instance yet -- Type <$> shrinkC conf n
Prop -> __IMPOSSIBLE__
Inf -> []
+ SizeUniv -> []
DLub s1 s2 -> __IMPOSSIBLE__
noShrink = id