diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-05-13 19:58:51 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-05-13 20:08:03 +0200 |
| commit | 0322ee0602760af914e23a2d39584bd4622c7aff (patch) | |
| tree | f630f87d337755604e3cd3e2a371106a7b95cfbb /src/Data/Array/Nested/Internal/Shape.hs | |
| parent | edffb586e99b4846d67c396e05f7adc13ac87cf4 (diff) | |
Appease GHC 9.10.2
Diffstat (limited to 'src/Data/Array/Nested/Internal/Shape.hs')
| -rw-r--r-- | src/Data/Array/Nested/Internal/Shape.hs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Data/Array/Nested/Internal/Shape.hs b/src/Data/Array/Nested/Internal/Shape.hs index 1770e38..97b9456 100644 --- a/src/Data/Array/Nested/Internal/Shape.hs +++ b/src/Data/Array/Nested/Internal/Shape.hs @@ -115,17 +115,21 @@ listrFromList (x : xs) k = listrFromList xs $ \l -> k (x ::: l) listrHead :: ListR (n + 1) i -> i listrHead (i ::: _) = i +listrHead ZR = error "unreachable" listrTail :: ListR (n + 1) i -> ListR n i listrTail (_ ::: sh) = sh +listrTail ZR = error "unreachable" listrInit :: ListR (n + 1) i -> ListR n i listrInit (n ::: sh@(_ ::: _)) = n ::: listrInit sh listrInit (_ ::: ZR) = ZR +listrInit ZR = error "unreachable" listrLast :: ListR (n + 1) i -> i listrLast (_ ::: sh@(_ ::: _)) = listrLast sh listrLast (n ::: ZR) = n +listrLast ZR = error "unreachable" listrIndex :: forall k n i. (k + 1 <= n) => SNat k -> ListR n i -> i listrIndex SZ (x ::: _) = x |