diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-11-13 20:20:30 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-11-13 20:20:30 +0100 |
| commit | bf4a469f369f1b8c6b1c2d7cc6907177405603f4 (patch) | |
| tree | 2f62400251662a7285aeba7fff0b807432f75fff | |
| parent | dd859ea30b187880e49c0cb005cc6006a1e3bbc1 (diff) | |
Add withKnownSh{S,X}
| -rw-r--r-- | src/Data/Array/Mixed/Shape.hs | 4 | ||||
| -rw-r--r-- | src/Data/Array/Nested/Internal/Shape.hs | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/src/Data/Array/Mixed/Shape.hs b/src/Data/Array/Mixed/Shape.hs index 1d3e60a..b5a4cb9 100644 --- a/src/Data/Array/Mixed/Shape.hs +++ b/src/Data/Array/Mixed/Shape.hs @@ -31,6 +31,7 @@ import Data.Kind (Type, Constraint) import Data.Monoid (Sum(..)) import Data.Proxy import Data.Type.Equality +import GHC.Exts (withDict) import GHC.Generics (Generic) import GHC.IsList (IsList) import GHC.IsList qualified as IsList @@ -469,6 +470,9 @@ instance KnownShX '[] where knownShX = ZKX instance (KnownNat n, KnownShX sh) => KnownShX (Just n : sh) where knownShX = SKnown natSing :!% knownShX instance KnownShX sh => KnownShX (Nothing : sh) where knownShX = SUnknown () :!% knownShX +withKnownShX :: forall sh r. StaticShX sh -> (KnownShX sh => r) -> r +withKnownShX sh = withDict @(KnownShX sh) sh + -- * Flattening diff --git a/src/Data/Array/Nested/Internal/Shape.hs b/src/Data/Array/Nested/Internal/Shape.hs index b7bbf4c..59f2c9a 100644 --- a/src/Data/Array/Nested/Internal/Shape.hs +++ b/src/Data/Array/Nested/Internal/Shape.hs @@ -34,6 +34,7 @@ import Data.Kind (Type, Constraint) import Data.Monoid (Sum(..)) import Data.Proxy import Data.Type.Equality +import GHC.Exts (withDict) import GHC.IsList (IsList) import GHC.IsList qualified as IsList import GHC.TypeLits @@ -558,6 +559,9 @@ class KnownShS sh where knownShS :: ShS sh instance KnownShS '[] where knownShS = ZSS instance (KnownNat n, KnownShS sh) => KnownShS (n : sh) where knownShS = natSing :$$ knownShS +withKnownShS :: forall sh r. ShS sh -> (KnownShS sh => r) -> r +withKnownShS sh = withDict @(KnownShS sh) sh + shsKnownShS :: ShS sh -> Dict KnownShS sh shsKnownShS ZSS = Dict shsKnownShS (SNat :$$ sh) | Dict <- shsKnownShS sh = Dict |