From 10f26ff16fec579545e0f2333e9fdd650bbac8e6 Mon Sep 17 00:00:00 2001
From: Christiaan Baaij <christiaan.baaij@gmail.com>
Date: Sat, 2 Nov 2024 07:11:49 +0100
Subject: [PATCH] Reduce `splitAt` to undefined in illegal contexts (#2835)

Previously, the Clash compiler would try to reduce

```
splitAt d1 Nil
```
to something of type
```
(Vec 1 a, Vec (0-1) a)
```
by trying to project the head and the tail out of the `Nil`
constructor. This of course does not work resulting in an
out-of-bounds indexing error reported in:

https://github.com/clash-lang/clash-compiler/issues/2831

The compiler now reduces above expressions to:

```
undefined :: (Vec 1 a, Vec (0-1) a)
```

Which is morally equivalent to the run-time exception Haskell
evaluation would have thrown if the circuit description was
evaluated like a regular Haskell program.

Fixes #2831
---
 changelog/2024-10-29T14_54_54+01_00_fix2831   |  1 +
 .../src-ghc/Clash/GHC/Evaluator/Primitive.hs  | 23 ++++++++++++++-----
 tests/Main.hs                                 |  1 +
 tests/shouldwork/Issues/T2831.hs              | 14 +++++++++++
 4 files changed, 33 insertions(+), 6 deletions(-)
 create mode 100644 changelog/2024-10-29T14_54_54+01_00_fix2831
 create mode 100644 tests/shouldwork/Issues/T2831.hs

diff --git a/changelog/2024-10-29T14_54_54+01_00_fix2831 b/changelog/2024-10-29T14_54_54+01_00_fix2831
new file mode 100644
index 0000000000..15e1d76653
--- /dev/null
+++ b/changelog/2024-10-29T14_54_54+01_00_fix2831
@@ -0,0 +1 @@
+FIXED: Clash errors out when `Clash.Sized.Vector.splitAt` is compile-time evaluated in an illegal context
diff --git a/clash-ghc/src-ghc/Clash/GHC/Evaluator/Primitive.hs b/clash-ghc/src-ghc/Clash/GHC/Evaluator/Primitive.hs
index 68541879eb..b0460a5dec 100644
--- a/clash-ghc/src-ghc/Clash/GHC/Evaluator/Primitive.hs
+++ b/clash-ghc/src-ghc/Clash/GHC/Evaluator/Primitive.hs
@@ -3827,12 +3827,23 @@ ghcPrimStep tcm isSubj pInfo tys args mach = case primName pInfo of
          -- (x:xs) <- v
          m' | DC _ vArgs <- last args
             -- (x:fst (splitAt (m-1) xs),snd (splitAt (m-1) xs))
-            -> reduce $
-               mkApps (Data tupDc) $ (map Right tyArgs) ++
-                 [ Left (mkVecCons consCon aTy m' (Either.lefts vArgs !! 1)
-                           (splitAtSelR (Either.lefts vArgs !! 2) m1VecTy [lAlt]))
-                 , Left (splitAtSelR (Either.lefts vArgs !! 2) nVecTy [rAlt])
-                 ]
+            -> case Either.lefts vArgs of
+                (_ : x : xs : _) ->
+                  reduce $
+                    mkApps (Data tupDc) $ (map Right tyArgs) ++
+                      [ Left (mkVecCons consCon aTy m' x
+                                (splitAtSelR xs m1VecTy [lAlt]))
+                      , Left (splitAtSelR xs nVecTy [rAlt])
+                      ]
+                _ ->
+                  -- v actually reduces to Nil and not Cons, this only happens
+                  -- when 'n' would reduce to a negative number; the complement
+                  -- of 'm'.
+                  --
+                  -- See Clash issue: https://github.com/clash-lang/clash-compiler/issues/2831
+                  let resTy = getResultTy tcm ty tys
+                   in reduce (TyApp (Prim NP.undefined) resTy)
+
          -- v doesn't reduce to a data-constructor
          _  -> Nothing
 
diff --git a/tests/Main.hs b/tests/Main.hs
index 03c5e15186..5e24e96d1d 100755
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -634,6 +634,7 @@ runClashTest = defaultMain $ clashTestRoot
         , runTest "T2623CaseConFVs" def{hdlLoad=[],hdlSim=[],hdlTargets=[VHDL]}
         , runTest "T2781" def{hdlLoad=[],hdlSim=[],hdlTargets=[VHDL]}
         , runTest "T2628" def{hdlTargets=[VHDL], buildTargets=BuildSpecific ["TACacheServerStep"], hdlSim=[]}
+        , runTest "T2831" def{hdlLoad=[],hdlSim=[],hdlTargets=[VHDL]}
         ] <>
         if compiledWith == Cabal then
           -- This tests fails without environment files present, which are only
diff --git a/tests/shouldwork/Issues/T2831.hs b/tests/shouldwork/Issues/T2831.hs
new file mode 100644
index 0000000000..adb97b5edd
--- /dev/null
+++ b/tests/shouldwork/Issues/T2831.hs
@@ -0,0 +1,14 @@
+module T2831 where
+
+import Clash.Prelude
+
+f :: forall n. SNat n -> Unsigned 4
+f n@SNat = case compareSNat n (SNat @15) of
+  SNatLE -> at @n @(16 - n - 1) SNat vec
+  SNatGT -> 0
+ where
+  vec :: Vec 16 (Unsigned 4)
+  vec = repeat 1
+
+topEntity :: Unsigned 4
+topEntity = f d17