-- |
-- Module      : Math.VectorSpace.DimensionAware
-- Copyright   : (c) Justus Sagemüller 2022
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 


{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE DefaultSignatures      #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE UnicodeSyntax          #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE CPP                    #-}

module Math.VectorSpace.DimensionAware where

import Data.VectorSpace

import Data.Singletons (SingI, sing, Sing)
#if MIN_VERSION_singletons(3,0,0)
import Prelude.Singletons (SNum(..))
import Data.Maybe.Singletons
import GHC.TypeLits.Singletons (withKnownNat)
#else
import Data.Singletons.Prelude.Num (SNum(..))
import Data.Singletons.Prelude.Maybe (SMaybe(..))
import Data.Singletons.TypeLits (withKnownNat)
#endif

import qualified Data.Vector.Generic as GArr
import qualified Data.Vector.Generic.Mutable as GMArr
import Control.Monad.ST (ST)

import Control.Monad

import GHC.TypeLits
import GHC.Exts (Constraint)
import Data.Proxy (Proxy(..))

import Data.Ratio

import qualified Math.VectorSpace.DimensionAware.Theorems.MaybeNat as Maybe


-- | Low-level case distinction between spaces with a dimension that is both fixed
--   and low enough that it makes sense to treat it this way, and more general
--   spaces where this is not feasible.
--
--   Use this type only when defining instances of 'DimensionAware'. When making
--   decisions based on dimensionality, 'DimensionalityCases' is more convenient.
data DimensionalityWitness v where
  IsStaticDimensional :: (n`Dimensional`v) => DimensionalityWitness v
  IsFlexibleDimensional :: StaticDimension v ~ 'Nothing => DimensionalityWitness v


-- | This class does not really pose any restrictions on a vector space type, but
--   allows it to express its dimension.
--   This is for optimisation purposes only, specifically to allow low-dimensional vectors
--   to be represented efficiently in unboxed arrays / matrices.
class VectorSpace v => DimensionAware v where
  -- | If this is `Nothing`,
  --   it can mean the dimension is infinite, or just big, or simply unknown / not
  --   considered in the implementation.
  type StaticDimension v :: Maybe Nat
  type StaticDimension v = 'Nothing

  dimensionalityWitness :: DimensionalityWitness v


instance DimensionAware Float   where
  type StaticDimension Float   = 'Just 1
  dimensionalityWitness :: DimensionalityWitness Float
dimensionalityWitness = forall (n :: Nat) v. Dimensional n v => DimensionalityWitness v
IsStaticDimensional
instance DimensionAware Double  where
  type StaticDimension Double  = 'Just 1
  dimensionalityWitness :: DimensionalityWitness Double
dimensionalityWitness = forall (n :: Nat) v. Dimensional n v => DimensionalityWitness v
IsStaticDimensional
instance DimensionAware Int     where
  type StaticDimension Int     = 'Just 1
  dimensionalityWitness :: DimensionalityWitness Int
dimensionalityWitness = forall (n :: Nat) v. Dimensional n v => DimensionalityWitness v
IsStaticDimensional
instance DimensionAware Integer where
  type StaticDimension Integer = 'Just 1
  dimensionalityWitness :: DimensionalityWitness Integer
dimensionalityWitness = forall (n :: Nat) v. Dimensional n v => DimensionalityWitness v
IsStaticDimensional
instance Integral n => DimensionAware (Ratio n) where
  type StaticDimension (Ratio n) = 'Just 1
  dimensionalityWitness :: DimensionalityWitness (Ratio n)
dimensionalityWitness = forall (n :: Nat) v. Dimensional n v => DimensionalityWitness v
IsStaticDimensional

instance ∀ u v . (DimensionAware u, DimensionAware v, Scalar u ~ Scalar v)
                   => DimensionAware (u,v) where
  type StaticDimension (u,v) = Maybe.ZipWithPlus (StaticDimension u) (StaticDimension v)
  dimensionalityWitness :: DimensionalityWitness (u, v)
dimensionalityWitness = case (forall v. DimensionAware v => DimensionalityWitness v
dimensionalityWitness @u, forall v. DimensionAware v => DimensionalityWitness v
dimensionalityWitness @v) of
    (DimensionalityWitness u
IsStaticDimensional, DimensionalityWitness v
IsStaticDimensional)
       -> forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat (forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @u forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+ forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @v)
              forall (n :: Nat) v. Dimensional n v => DimensionalityWitness v
IsStaticDimensional
    (DimensionalityWitness u
IsFlexibleDimensional, DimensionalityWitness v
_) -> forall v. (StaticDimension v ~ 'Nothing) => DimensionalityWitness v
IsFlexibleDimensional
    (DimensionalityWitness u
_, DimensionalityWitness v
IsFlexibleDimensional) -> forall v. (StaticDimension v ~ 'Nothing) => DimensionalityWitness v
IsFlexibleDimensional


class (DimensionAware v, StaticDimension v ~ 'Just n)
           => n`Dimensional`v | v -> n where
  knownDimensionalitySing :: Sing n
  {-# INLINE knownDimensionalitySing #-}
  default knownDimensionalitySing :: KnownNat n => Sing n
  knownDimensionalitySing = forall {k} (a :: k). SingI a => Sing a
sing
  -- | Read basis expansion from an array, starting at the specified offset.
  --   The array must have at least length @n + offset@, else the behaviour is undefined.
  unsafeFromArrayWithOffset :: GArr.Vector α (Scalar v) => Int -> α (Scalar v) -> v
  unsafeWriteArrayWithOffset :: GArr.Vector α (Scalar v)
          => GArr.Mutable α σ (Scalar v) -> Int -> v -> ST σ ()

-- | Batteries-included version of 'DimensionalityWitness'.
data DimensionalityCases v where
  StaticDimensionalCase :: (KnownNat n, n`Dimensional`v) => DimensionalityCases v
  FlexibleDimensionalCase :: StaticDimension v ~ 'Nothing => DimensionalityCases v

#if !MIN_VERSION_singletons(3,0,0)
type family FromJust (a :: Maybe k) :: k where
  FromJust ('Just v) = v
#endif

type Dimension v = FromJust (StaticDimension v)

#if !MIN_VERSION_singletons(3,0,0)
type family IsJust (a :: Maybe k) :: Bool where
  IsJust ('Just _) = 'True
  IsJust _ = 'False
#endif

class DimensionAware v => StaticDimensional v where
  dimensionIsStatic :: ∀ r . (∀ n . (KnownNat n, n`Dimensional`v) => r) -> r

{-# INLINE dimensionalitySing #-}
dimensionalitySing :: ∀ v n . n`Dimensional`v => Sing n
dimensionalitySing :: forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing = forall (n :: Nat) v. Dimensional n v => Sing n
knownDimensionalitySing @n @v

instance ( DimensionAware v, IsJust (StaticDimension v) ~ 'True )
       => StaticDimensional v where
  dimensionIsStatic :: forall r.
(forall (n :: Nat). (KnownNat n, Dimensional n v) => r) -> r
dimensionIsStatic = case forall v. DimensionAware v => DimensionalityWitness v
dimensionalityWitness @v of
   DimensionalityWitness v
IsStaticDimensional -> \forall (n :: Nat). (KnownNat n, Dimensional n v) => r
φ -> forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat (forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @v) forall (n :: Nat). (KnownNat n, Dimensional n v) => r
φ

dimensionality :: ∀ v . DimensionAware v => DimensionalityCases v
dimensionality :: forall v. DimensionAware v => DimensionalityCases v
dimensionality = case forall v. DimensionAware v => DimensionalityWitness v
dimensionalityWitness @v of
  DimensionalityWitness v
IsStaticDimensional -> forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat (forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @v) forall (n :: Nat) v.
(KnownNat n, Dimensional n v) =>
DimensionalityCases v
StaticDimensionalCase
  DimensionalityWitness v
IsFlexibleDimensional -> forall v. (StaticDimension v ~ 'Nothing) => DimensionalityCases v
FlexibleDimensionalCase

{-# INLINE dimension #-}
dimension :: ∀ v n a . (n`Dimensional`v, Integral a) => a
dimension :: forall v (n :: Nat) a. (Dimensional n v, Integral a) => a
dimension = forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat (forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @v) (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @n forall {k} (t :: k). Proxy t
Proxy)

-- | Convenience function. The result does never depend on the runtime input, only
--   on its type.
dimensionOf :: ∀ v n a . (n`Dimensional`v, Integral a) => v -> a
dimensionOf :: forall v (n :: Nat) a. (Dimensional n v, Integral a) => v -> a
dimensionOf v
_ = forall v (n :: Nat) a. (Dimensional n v, Integral a) => a
dimension @v

{-# INLINE unsafeFromArray #-}
-- | Read basis expansion from an array. The array must have length @n@, else the
--   behaviour is undefined.
unsafeFromArray :: ∀ v n α . (n`Dimensional`v, GArr.Vector α (Scalar v))
         => α (Scalar v) -> v
unsafeFromArray :: forall v (n :: Nat) (α :: * -> *).
(Dimensional n v, Vector α (Scalar v)) =>
α (Scalar v) -> v
unsafeFromArray = forall (n :: Nat) v (α :: * -> *).
(Dimensional n v, Vector α (Scalar v)) =>
Int -> α (Scalar v) -> v
unsafeFromArrayWithOffset Int
0

-- | Read basis expansion from an array, if the size equals the dimension.
fromArray :: ∀ v n α . (n`Dimensional`v, GArr.Vector α (Scalar v))
         => α (Scalar v) -> Maybe v
fromArray :: forall v (n :: Nat) (α :: * -> *).
(Dimensional n v, Vector α (Scalar v)) =>
α (Scalar v) -> Maybe v
fromArray α (Scalar v)
ar
 | forall (v :: * -> *) a. Vector v a => v a -> Int
GArr.length α (Scalar v)
ar forall a. Eq a => a -> a -> Bool
== forall v (n :: Nat) a. (Dimensional n v, Integral a) => a
dimension @v  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall v (n :: Nat) (α :: * -> *).
(Dimensional n v, Vector α (Scalar v)) =>
α (Scalar v) -> v
unsafeFromArray α (Scalar v)
ar
 | Bool
otherwise                       = forall a. Maybe a
Nothing

{-# INLINE toArray #-}
-- | Write out basis expansion to an array, whose length will always be @n@.
toArray :: ∀ v n α . (n`Dimensional`v, GArr.Vector α (Scalar v))
         => v -> α (Scalar v)
toArray :: forall v (n :: Nat) (α :: * -> *).
(Dimensional n v, Vector α (Scalar v)) =>
v -> α (Scalar v)
toArray v
v = forall (v :: * -> *) a.
Vector v a =>
(forall s. ST s (Mutable v s a)) -> v a
GArr.create (do
   Mutable α s (Scalar v)
ar <- forall (m :: * -> *) (v :: * -> * -> *) a.
(HasCallStack, PrimMonad m, MVector v a) =>
Int -> m (v (PrimState m) a)
GMArr.new forall a b. (a -> b) -> a -> b
$ forall v (n :: Nat) a. (Dimensional n v, Integral a) => a
dimension @v
   forall (n :: Nat) v (α :: * -> *) σ.
(Dimensional n v, Vector α (Scalar v)) =>
Mutable α σ (Scalar v) -> Int -> v -> ST σ ()
unsafeWriteArrayWithOffset Mutable α s (Scalar v)
ar Int
0 v
v
   forall (m :: * -> *) a. Monad m => a -> m a
return Mutable α s (Scalar v)
ar
  )

{-# INLINE staticDimensionSing #-}
staticDimensionSing :: ∀ v . DimensionAware v => Sing (StaticDimension v)
staticDimensionSing :: forall v. DimensionAware v => Sing (StaticDimension v)
staticDimensionSing = case forall v. DimensionAware v => DimensionalityWitness v
dimensionalityWitness @v of
  DimensionalityWitness v
IsStaticDimensional -> forall a (n :: a). Sing n -> SMaybe ('Just n)
SJust (forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @v)
  DimensionalityWitness v
IsFlexibleDimensional -> forall {k} (a :: k). SingI a => Sing a
sing

{-# INLINE scalarUnsafeFromArrayWithOffset #-}
scalarUnsafeFromArrayWithOffset :: (v ~ Scalar v, GArr.Vector α v)
          => Int -> α v -> v
scalarUnsafeFromArrayWithOffset :: forall v (α :: * -> *).
(v ~ Scalar v, Vector α v) =>
Int -> α v -> v
scalarUnsafeFromArrayWithOffset Int
i = (forall (v :: * -> *) a. Vector v a => v a -> Int -> a
`GArr.unsafeIndex`Int
i)

{-# INLINE scalarUnsafeWriteArrayWithOffset #-}
scalarUnsafeWriteArrayWithOffset :: (v ~ Scalar v, GArr.Vector α v)
          => GArr.Mutable α σ v -> Int -> v -> ST σ ()
scalarUnsafeWriteArrayWithOffset :: forall v (α :: * -> *) σ.
(v ~ Scalar v, Vector α v) =>
Mutable α σ v -> Int -> v -> ST σ ()
scalarUnsafeWriteArrayWithOffset Mutable α σ v
ar Int
i = forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> Int -> a -> m ()
GMArr.unsafeWrite Mutable α σ v
ar Int
i

{-# INLINE unsafeFromArrayWithOffsetViaList #-}
unsafeFromArrayWithOffsetViaList
          :: ∀ v n α . (n`Dimensional`v, GArr.Vector α (Scalar v))
   => ([Scalar v] -> v) -> Int -> α (Scalar v) -> v
unsafeFromArrayWithOffsetViaList :: forall v (n :: Nat) (α :: * -> *).
(Dimensional n v, Vector α (Scalar v)) =>
([Scalar v] -> v) -> Int -> α (Scalar v) -> v
unsafeFromArrayWithOffsetViaList [Scalar v] -> v
l2v Int
i
   = [Scalar v] -> v
l2v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: * -> *) a. Vector v a => v a -> [a]
GArr.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: * -> *) a. Vector v a => Int -> Int -> v a -> v a
GArr.unsafeSlice Int
i (forall v (n :: Nat) a. (Dimensional n v, Integral a) => a
dimension @v)
  
{-# INLINE unsafeWriteArrayWithOffsetViaList #-}
unsafeWriteArrayWithOffsetViaList
          :: ∀ v n α σ . (n`Dimensional`v, GArr.Vector α (Scalar v))
   => (v -> [Scalar v]) -> GArr.Mutable α σ (Scalar v)
         -> Int -> v -> ST σ ()
unsafeWriteArrayWithOffsetViaList :: forall v (n :: Nat) (α :: * -> *) σ.
(Dimensional n v, Vector α (Scalar v)) =>
(v -> [Scalar v]) -> Mutable α σ (Scalar v) -> Int -> v -> ST σ ()
unsafeWriteArrayWithOffsetViaList v -> [Scalar v]
v2l Mutable α σ (Scalar v)
ar Int
i
   = forall (m :: * -> *) (v :: * -> * -> *) a.
(PrimMonad m, MVector v a) =>
v (PrimState m) a -> v (PrimState m) a -> m ()
GMArr.unsafeCopy (forall (v :: * -> * -> *) a s.
MVector v a =>
Int -> Int -> v s a -> v s a
GMArr.unsafeSlice Int
i (forall v (n :: Nat) a. (Dimensional n v, Integral a) => a
dimension @v) Mutable α σ (Scalar v)
ar)
      forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall (m :: * -> *) (v :: * -> *) a.
(PrimMonad m, Vector v a) =>
v a -> m (Mutable v (PrimState m) a)
GArr.unsafeThaw @(ST σ) @α forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: * -> *) a. Vector v a => [a] -> v a
GArr.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> [Scalar v]
v2l
  
instance 1`Dimensional`Float   where
  {-# INLINE unsafeFromArrayWithOffset #-}
  unsafeFromArrayWithOffset :: forall (α :: * -> *).
Vector α (Scalar Float) =>
Int -> α (Scalar Float) -> Float
unsafeFromArrayWithOffset = forall v (α :: * -> *).
(v ~ Scalar v, Vector α v) =>
Int -> α v -> v
scalarUnsafeFromArrayWithOffset
  {-# INLINE unsafeWriteArrayWithOffset #-}
  unsafeWriteArrayWithOffset :: forall (α :: * -> *) σ.
Vector α (Scalar Float) =>
Mutable α σ (Scalar Float) -> Int -> Float -> ST σ ()
unsafeWriteArrayWithOffset = forall v (α :: * -> *) σ.
(v ~ Scalar v, Vector α v) =>
Mutable α σ v -> Int -> v -> ST σ ()
scalarUnsafeWriteArrayWithOffset
instance 1`Dimensional`Double  where
  {-# INLINE unsafeFromArrayWithOffset #-}
  unsafeFromArrayWithOffset :: forall (α :: * -> *).
Vector α (Scalar Double) =>
Int -> α (Scalar Double) -> Double
unsafeFromArrayWithOffset = forall v (α :: * -> *).
(v ~ Scalar v, Vector α v) =>
Int -> α v -> v
scalarUnsafeFromArrayWithOffset
  {-# INLINE unsafeWriteArrayWithOffset #-}
  unsafeWriteArrayWithOffset :: forall (α :: * -> *) σ.
Vector α (Scalar Double) =>
Mutable α σ (Scalar Double) -> Int -> Double -> ST σ ()
unsafeWriteArrayWithOffset = forall v (α :: * -> *) σ.
(v ~ Scalar v, Vector α v) =>
Mutable α σ v -> Int -> v -> ST σ ()
scalarUnsafeWriteArrayWithOffset
instance 1`Dimensional`Int     where
  {-# INLINE unsafeFromArrayWithOffset #-}
  unsafeFromArrayWithOffset :: forall (α :: * -> *).
Vector α (Scalar Int) =>
Int -> α (Scalar Int) -> Int
unsafeFromArrayWithOffset = forall v (α :: * -> *).
(v ~ Scalar v, Vector α v) =>
Int -> α v -> v
scalarUnsafeFromArrayWithOffset
  {-# INLINE unsafeWriteArrayWithOffset #-}
  unsafeWriteArrayWithOffset :: forall (α :: * -> *) σ.
Vector α (Scalar Int) =>
Mutable α σ (Scalar Int) -> Int -> Int -> ST σ ()
unsafeWriteArrayWithOffset = forall v (α :: * -> *) σ.
(v ~ Scalar v, Vector α v) =>
Mutable α σ v -> Int -> v -> ST σ ()
scalarUnsafeWriteArrayWithOffset
instance 1`Dimensional`Integer where
  {-# INLINE unsafeFromArrayWithOffset #-}
  unsafeFromArrayWithOffset :: forall (α :: * -> *).
Vector α (Scalar Integer) =>
Int -> α (Scalar Integer) -> Integer
unsafeFromArrayWithOffset = forall v (α :: * -> *).
(v ~ Scalar v, Vector α v) =>
Int -> α v -> v
scalarUnsafeFromArrayWithOffset
  {-# INLINE unsafeWriteArrayWithOffset #-}
  unsafeWriteArrayWithOffset :: forall (α :: * -> *) σ.
Vector α (Scalar Integer) =>
Mutable α σ (Scalar Integer) -> Int -> Integer -> ST σ ()
unsafeWriteArrayWithOffset = forall v (α :: * -> *) σ.
(v ~ Scalar v, Vector α v) =>
Mutable α σ v -> Int -> v -> ST σ ()
scalarUnsafeWriteArrayWithOffset
instance Integral n => 1`Dimensional`Ratio n where
  {-# INLINE unsafeFromArrayWithOffset #-}
  unsafeFromArrayWithOffset :: forall (α :: * -> *).
Vector α (Scalar (Ratio n)) =>
Int -> α (Scalar (Ratio n)) -> Ratio n
unsafeFromArrayWithOffset = forall v (α :: * -> *).
(v ~ Scalar v, Vector α v) =>
Int -> α v -> v
scalarUnsafeFromArrayWithOffset
  {-# INLINE unsafeWriteArrayWithOffset #-}
  unsafeWriteArrayWithOffset :: forall (α :: * -> *) σ.
Vector α (Scalar (Ratio n)) =>
Mutable α σ (Scalar (Ratio n)) -> Int -> Ratio n -> ST σ ()
unsafeWriteArrayWithOffset = forall v (α :: * -> *) σ.
(v ~ Scalar v, Vector α v) =>
Mutable α σ v -> Int -> v -> ST σ ()
scalarUnsafeWriteArrayWithOffset

  
instance ∀ n u m v nm . ( n`Dimensional`u, m`Dimensional`v
                        , Scalar u ~ Scalar v
                        , nm ~ (n+m) )
                   => nm`Dimensional`(u,v) where
  {-# INLINE knownDimensionalitySing #-}
  knownDimensionalitySing :: Sing nm
knownDimensionalitySing = forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @u forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+ forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @v
  {-# INLINE unsafeFromArrayWithOffset #-}
  unsafeFromArrayWithOffset :: forall (α :: * -> *).
Vector α (Scalar (u, v)) =>
Int -> α (Scalar (u, v)) -> (u, v)
unsafeFromArrayWithOffset Int
i α (Scalar (u, v))
arr
      = ( forall (n :: Nat) v (α :: * -> *).
(Dimensional n v, Vector α (Scalar v)) =>
Int -> α (Scalar v) -> v
unsafeFromArrayWithOffset Int
i α (Scalar (u, v))
arr
        , forall (n :: Nat) v (α :: * -> *).
(Dimensional n v, Vector α (Scalar v)) =>
Int -> α (Scalar v) -> v
unsafeFromArrayWithOffset (Int
i forall a. Num a => a -> a -> a
+ forall v (n :: Nat) a. (Dimensional n v, Integral a) => a
dimension @u) α (Scalar (u, v))
arr )
  {-# INLINE unsafeWriteArrayWithOffset #-}
  unsafeWriteArrayWithOffset :: forall (α :: * -> *) σ.
Vector α (Scalar (u, v)) =>
Mutable α σ (Scalar (u, v)) -> Int -> (u, v) -> ST σ ()
unsafeWriteArrayWithOffset Mutable α σ (Scalar (u, v))
arr Int
i (u
x,v
y) = do
      forall (n :: Nat) v (α :: * -> *) σ.
(Dimensional n v, Vector α (Scalar v)) =>
Mutable α σ (Scalar v) -> Int -> v -> ST σ ()
unsafeWriteArrayWithOffset Mutable α σ (Scalar (u, v))
arr Int
i u
x
      forall (n :: Nat) v (α :: * -> *) σ.
(Dimensional n v, Vector α (Scalar v)) =>
Mutable α σ (Scalar v) -> Int -> v -> ST σ ()
unsafeWriteArrayWithOffset Mutable α σ (Scalar (u, v))
arr (Int
i forall a. Num a => a -> a -> a
+ forall v (n :: Nat) a. (Dimensional n v, Integral a) => a
dimension @u) v
y

-- | To be used as an “absurd” values for implementing methods whose constraints combine
--   to require both static- and flexible dimensionality (which can thus never be called).
--
--   The actual type of this should be
--
-- @
--   notStaticDimensionalContradiction :: ∀ v n r
--     . (n`Dimensional`v, StaticDimension v ~ 'Nothing) => r
-- @
--
--   GHC 9.6 baulks at that, though. It is a self-contradicting type, but that's the whole point...
notStaticDimensionalContradiction :: ∀ v n r
  . ( -- n`Dimensional`v,
      StaticDimension v ~ 'Nothing) => r
notStaticDimensionalContradiction :: forall {k} v (n :: k) r. (StaticDimension v ~ 'Nothing) => r
notStaticDimensionalContradiction = forall a. HasCallStack => a
undefined