Reduce splitAt to undefined in illegal contexts (#2835) (#2837)

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:

#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

(cherry picked from commit 10f26ff)

Co-authored-by: Christiaan Baaij <[email protected]>

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

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
 

tests/Main.hs

@@ -818,6 +818,7 @@ runClashTest = defaultMain
         , runTest "T2628" def{hdlTargets=[VHDL], buildTargets=BuildSpecific ["TACacheServerStep"], hdlSim=[]}
         , runTest "T2839" def{hdlLoad=[],hdlSim=[],hdlTargets=[VHDL]}
         , runTest "T2845" def{hdlSim=[],hdlTargets=[Verilog]}
+        , runTest "T2831" def{hdlLoad=[],hdlSim=[],hdlTargets=[VHDL]}
         ] <>
         if compiledWith == Cabal then
           -- This tests fails without environment files present, which are only

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