fix: EvalFull duplicated IDs in BETA reduction

We previously were testing this in some unit tests but had no property
test. We add a property test to prevent any regression in the future.

primer/src/Primer/EvalFull.hs

@@ -492,7 +492,7 @@ runRedex = \case
   -- (Λa.t : ∀b.T) S  ~>  lettype b = S in (lettype a = S in t) : T
   BETA a t b tyT tyS
     | a == b -> letType a (pure tyS) $ pure t `ann` pure tyT
-    | otherwise -> letType b (pure tyS) $ letType a (pure tyS) (pure t) `ann` pure tyT
+    | otherwise -> letType b (regenerateTypeIDs tyS) $ letType a (pure tyS) (pure t) `ann` pure tyT
   -- case C as : T of ... ; C xs -> e ; ...   ~>  let xs=as:As in e for constructor C of type T, where args have types As
   -- (and also the non-annotated-constructor case)
   -- Note that when forming the CaseRedex we checked that the variables @xs@ were fresh for @as@ and @As@,

primer/test/Tests/EvalFull.hs

@@ -1076,6 +1076,27 @@ unit_eval_full_modules_scrutinize_imported_type =
         , moduleDefs = mempty
         }
 
+-- Test that evaluation does not duplicate node IDs
+hprop_unique_ids :: Property
+hprop_unique_ids = withTests 1000 $
+  withDiscards 2000 $
+    propertyWT testModules $ do
+      let globs = foldMap moduleDefsQualified testModules
+      tds <- asks typeDefs
+      (dir, t1, _) <- genDirTm
+      let go n t
+            | n == (0 :: Int) = pure ()
+            | otherwise = do
+                t' <- evalFull tds globs 1 dir t
+                case t' of
+                  Left (TimedOut e) -> uniqueIDs e >> go (n - 1) e
+                  Right e -> uniqueIDs e
+      go 20 t1 -- we need some bound since not all terms terminate
+  where
+    uniqueIDs e =
+      let ids = e ^.. exprIDs
+       in ids === ordNub ids
+
 -- * Utilities
 
 evalFullTest :: ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> Either EvalFullError Expr