Hi! I have been attempting to write a test case with dependently typed matrices, and have been struggling to find a way to write them without statically specifying the dimensions. This isn’t ideal because I want to test on many different dimensions.

Here’s what I currently have

```
-- Need to specify dimensions :(
sensStaticHMatrixPlus = SensStaticHMatrix.plus @3 @4 @L1 @Diff
-- This generates tests automatically
$( sensCheck
"passing_tests"
[ 'Correct.solo_double
...
, 'sensStaticHMatrixMult
]
)
```

This isn’t ideal I would like to test adding two matrices with different sized columns and rows (of course with the same dimensions for addition).

Here’s one of my attempts based on this post How to create Arbitrary instance for dependent types? - #7 by tomjaguarpaw

I was able to make a arbitrary generator using that.

```
data SomeMatrix c n s where
SomeMatrix :: (KnownNat (x :: Nat), KnownNat (y :: Nat)) => SensStaticHMatrix (x :: TL.Nat) (y :: TL.Nat) c n s -> SomeMatrix c n s
example :: forall c n s. Gen (SomeMatrix c n s)
example = do
x' <- arbitrary
y' <- arbitrary
reifyNat x' $ \(x :: Proxy x) -> reifyNat y' $ \(y :: Proxy y) -> do
elems <- replicateM ( fromInteger x' * fromInteger y') (arbitrary @Double)
pure $ SomeMatrix @x @y $ SensStaticHMatrixUNSAFE $ matrix elems
-- Generate two matrices of the same dimensions
-- Useful for addition
exampleTwo :: forall c n s1 s2. Gen (SomeMatrix c n s1, SomeMatrix c n s2)
exampleTwo = do
x' <- arbitrary
y' <- arbitrary
reifyNat x' $ \(x :: Proxy x) -> reifyNat y' $ \(y :: Proxy y) -> do
elems1 <- replicateM ( fromInteger x' * fromInteger y') (arbitrary @Double)
elems2 <- replicateM ( fromInteger x' * fromInteger y') (arbitrary @Double)
pure (SomeMatrix @x @y $ SensStaticHMatrixUNSAFE $ matrix elems1, SomeMatrix @x @y $ SensStaticHMatrixUNSAFE $ matrix elems2)
```

However when I attempt to use it I think the x and y aren’t the same. I think maybe my use case is slightly different.

```
test = do
(SomeMatrix m1, SomeMatrix m2) <- generate $ exampleTwo @L2 @Diff
pure $ (plus m1 m2) == (plus m1 m2) -- toy example not the actual property I check
-- ^^^
-- Couldn't match type ‘y1’ with ‘y’
-- Expected: SensStaticHMatrix x y L2 Diff s20
-- Actual: SensStaticHMatrix x1 y1 L2 Diff s20
```

My attempted solutions can be found here: SensCheck/src/SensStaticHMatrix.hs at f89c98c40c3d7851a04cf5f44a9abf3d256261e2 · uvm-plaid/SensCheck · GitHub

I would greatly appreciate some help with this. Thanks!