[ fix #4570 ] Don't mark levels as `NeutralLevel` unless all reductions are enabled

2 files changed, 31 insertions, 2 deletions

diff --git a/src/full/Agda/TypeChecking/Reduce.hs b/src/full/Agda/TypeChecking/Reduce.hs
index 73cb9fd..c788931 100644
--- a/src/full/Agda/TypeChecking/Reduce.hs
+++ b/src/full/Agda/TypeChecking/Reduce.hs
@@ -327,11 +327,15 @@ instance Reduce LevelAtom where
     where
       fromTm v = do
         bv <- reduceB' v
+        hasAllReductions <- (allReductions `SmallSet.isSubsetOf`) <$>
+                              asksTC envAllowedReductions
         let v = ignoreBlocking bv
         case bv of
           NotBlocked r (MetaV m vs) -> return $ NotBlocked r $ MetaLevel m vs
           Blocked m _               -> return $ Blocked m    $ BlockedLevel m v
-          NotBlocked r _            -> return $ NotBlocked r $ NeutralLevel r v
+          NotBlocked r _
+            | hasAllReductions -> return $ NotBlocked r $ NeutralLevel r v
+            | otherwise        -> return $ NotBlocked r $ UnreducedLevel v
 
 
 instance (Subst t a, Reduce a) => Reduce (Abs a) where
@@ -1089,7 +1093,7 @@ instance Normalise LevelAtom where
       MetaLevel m vs   -> MetaLevel m <$> normalise' vs
       BlockedLevel m v -> BlockedLevel m <$> normalise' v
       NeutralLevel r v -> NeutralLevel r <$> normalise' v
-      UnreducedLevel{} -> __IMPOSSIBLE__    -- I hope
+      UnreducedLevel v -> UnreducedLevel <$> normalise' v
 
 instance (Subst t a, Normalise a) => Normalise (Abs a) where
     normalise' a@(Abs x _) = Abs x <$> underAbstraction_ a normalise'
diff --git a/test/Succeed/Issue4570.agda b/test/Succeed/Issue4570.agda
new file mode 100644
index 0000000..1918ce8
--- /dev/null
+++ b/test/Succeed/Issue4570.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Nat
+open import Agda.Primitive
+
+record Graph ℓv ℓe : Set (lsuc (ℓv ⊔ ℓe)) where
+  field
+    Obj : Set ℓv
+    Hom : Obj → Obj → Set ℓe
+
+open Graph public
+
+postulate
+  t : Nat → Nat → Bool
+
+ωGr : Graph lzero lzero
+Obj ωGr = Nat
+Hom ωGr m n with t m n
+... | true = {!!} -- if n ≡ (suc m)
+... | false = {!!} -- otherwise
+
+foo : ∀ m n → Hom ωGr m n → {!!}
+foo m n f with t m n
+... | z = {!!}