dimensions 2.0.0.0 → 2.1.0.0

raw patch · 19 files changed

+2088/−831 lines, 19 filesdep −ghcdep ~constraints-derivingbuild-type:Customsetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies removed: ghc

Dependency ranges changed: constraints-deriving

API changes (from Hackage documentation)

Files

• Setup.hs +31/−1
• dimensions.cabal +14/−8
• src/Data/Type/List.hs +27/−149
• src/Data/Type/List/Classes.hs +489/−0
• src/Data/Type/List/Families.hs +84/−0
• src/Data/Type/List/InjectiveSnoc.hs +0/−67
• src/Data/Type/List/Internal.hs +55/−24
• src/Data/Type/Lits.hs +49/−15
• src/Numeric/Dimensions/Dim.hs +500/−290
• src/Numeric/Dimensions/Dim.hs-boot +2/−3
• src/Numeric/Dimensions/Idx.hs +455/−121
• src/Numeric/Tuple.hs +3/−0
• src/Numeric/Tuple/Lazy.hs +14/−14
• src/Numeric/Tuple/Strict.hs +14/−14
• src/Numeric/TypedList.hs +137/−106
• test/Data/Type/ListTest.hs +193/−0
• test/Numeric/Dimensions/DimTest.hs +2/−2
• test/Numeric/Dimensions/IdxTest.hs +16/−16
• test/Spec.hs +3/−1

@@ -1,2 +1,32 @@+{-+Disable some errors and warnings during the haddock pass+  (caused by compiler plugins and hs-boot)+ -}+{-# OPTIONS_GHC -Wall #-}+module Main (main) where+ import Distribution.Simple-main = defaultMain+import Distribution.Simple.Setup++main :: IO ()+main = defaultMainWithHooks simpleUserHooks+  { confHook = \a -> confHook simpleUserHooks a . tweakFlags }++tweakFlags :: ConfigFlags -> ConfigFlags+tweakFlags flags = flags+  { configProgramArgs = addHaddockArgs (configProgramArgs flags) }++addHaddockArgs :: [(String, [String])] -> [(String, [String])]+addHaddockArgs []+  = [("haddock", newHaddockGhcArgs)]+addHaddockArgs (("haddock", args):otherProgsArgs)+  = ("haddock", args ++ newHaddockGhcArgs) : otherProgsArgs+addHaddockArgs (progArgs:otherProgsArgs)+  = progArgs : addHaddockArgs otherProgsArgs++newHaddockGhcArgs :: [String]+newHaddockGhcArgs =+  [ "--optghc=-fdefer-type-errors"+  , "--optghc=-fno-warn-deferred-type-errors"+  , "--optghc=-fno-warn-missing-home-modules"+  ]

@@ -1,13 +1,13 @@-cabal-version: 1.12+cabal-version: 1.24  -- This file has been generated from package.yaml by hpack version 0.31.1. -- -- see: https://github.com/sol/hpack ----- hash: 982b8bf6393fdd487b646f7c7a3b258acba9501a6d106861757a3b4a49f3de82+-- hash: 02a12f73c300d1f3b4ea569d86f2222327243c0918b00236786ba647754dd7f2  name:           dimensions-version:        2.0.0.0+version:        2.1.0.0 synopsis:       Safe type-level dimensionality for multidimensional data. description:    Safe type-level dimensionality for multidimensional data. Please see the README on GitHub at <https://github.com/achirkin/easytensor#readme> category:       math, geometry@@ -18,13 +18,18 @@ copyright:      Copyright: (c) 2019 Artem Chirkin license:        BSD3 license-file:   LICENSE-build-type:     Simple+build-type:     Custom  source-repository head   type: git   location: https://github.com/achirkin/easytensor   subdir: dimensions +custom-setup+  setup-depends:+      Cabal+    , base+ flag unsafeindices   description: Disable bound checks on Idx and Idxs types.   manual: True@@ -42,15 +47,15 @@       Numeric.Tuple.Strict       Numeric.TypedList   other-modules:-      Data.Type.List.InjectiveSnoc+      Data.Type.List.Families+      Data.Type.List.Classes       Data.Type.List.Internal   hs-source-dirs:       src   ghc-options: -Wall -Wcompat -Wtabs -Wmissing-local-signatures -Wmissing-home-modules -Widentities   build-depends:       base >=4.10 && <5-    , constraints-deriving >=1 && <2-    , ghc+    , constraints-deriving >=1.1.1.0 && <2   if flag(unsafeindices)     cpp-options: -DUNSAFE_INDICES   default-language: Haskell2010@@ -59,6 +64,7 @@   type: exitcode-stdio-1.0   main-is: Spec.hs   other-modules:+      Data.Type.ListTest       Numeric.Dimensions.DimTest       Numeric.Dimensions.IdxTest       Paths_dimensions@@ -69,6 +75,6 @@       Cabal     , QuickCheck     , base-    , constraints-deriving >=1 && <2+    , constraints-deriving >=1.1.1.0 && <2     , dimensions   default-language: Haskell2010

@@ -1,15 +1,15 @@-{-# LANGUAGE ConstraintKinds        #-}-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE FlexibleContexts       #-}-{-# LANGUAGE FlexibleInstances      #-}-{-# LANGUAGE GADTs                  #-}-{-# LANGUAGE PolyKinds              #-}-{-# LANGUAGE ScopedTypeVariables    #-}-{-# LANGUAGE TypeApplications       #-}-{-# LANGUAGE TypeFamilyDependencies #-}-{-# LANGUAGE TypeInType             #-}-{-# LANGUAGE TypeOperators          #-}-{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE ConstraintKinds      #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE ExplicitNamespaces   #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE TypeApplications     #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeInType           #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+ -------------------------------------------------------------------------------- -- | -- Module      :  Data.Type.List@@ -29,48 +29,25 @@   , StripPrefix, StripSuffix   , Reverse, Take, Drop, Length     -- * Operations on elements-  , All, Map, Elem-    -- * Concatenation and its evidence-  , ConcatList, evStripSuffix, evStripPrefix, evConcat+  , All, Map, UnMap, Elem+    -- * Classes that simplify inference of type equalities+  , SnocList, ReverseList, ConcatList+  , inferStripSuffix, inferStripPrefix, inferConcat     -- * Data.Typeable   , inferTypeableCons   ) where -import Data.Constraint         ((:-) (..), Constraint, Dict (..))-import Data.Type.List.Internal (Snoc)+import Data.Constraint         (Constraint, Dict (..))+import Data.Type.List.Classes+import Data.Type.List.Families import Data.Type.Lits-import GHC.Base                (Type) import Type.Reflection-import Unsafe.Coerce           (unsafeCoerce)  -- | Empty list, same as @'[]@.-type Empty = '[]+type Empty = ('[] :: [k])  -- | Appending a list, represents an @Op@ counterpart of @(':)@.-type Cons (a :: k) (as :: [k])-    = a ': as---- | Extract the first element of a list, which must be non-empty.-type family Head (xs :: [k]) :: k where-    Head ('[] :: [k]) = TypeError ( ListError k "Head: empty type-level list." )-    Head (x ': _)     = x---- | Extract the elements after the head of a list, which must be non-empty.-type family Tail (xs :: [k]) :: [k] where-    Tail ('[] :: [k]) = TypeError ( ListError k "Tail: empty type-level list." )-    Tail (_ ': xs)    = xs---- | Extract the last element of a list, which must be non-empty.-type family Last (xs :: [k]) :: k where-    Last ('[] :: [k]) = TypeError ( ListError k "Last: empty type-level list." )-    Last '[x]         = x-    Last (_ ': xs)    = Last xs---- | Extract all but last elements of a list, which must be non-empty.-type family Init (xs :: [k]) :: [k] where-    Init ('[] :: [k]) = TypeError ( ListError k "Init: empty type-level list." )-    Init '[x]         = '[]-    Init (x ': xs)    = x ': Init xs+type Cons (a :: k) (as :: [k]) = a ': as  -- | @Take n xs@ returns the prefix of a list of length @max n (length xs)@. type family Take (n :: Nat) (xs :: [k]) :: [k] where@@ -84,64 +61,6 @@     Drop n (_ ': xs) = Drop (n - 1) xs     Drop _ '[]       = '[] --- | Append two lists.-type family Concat (as :: [k]) (bs :: [k]) :: [k] where-    Concat '[]        bs       = bs-    Concat  as       '[]       = as-    Concat (a ': as)  bs       = a ': Concat as bs---- | Remove prefix @as@ from a list @asbs@ if @as@ is a prefix; fail otherwise.-type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where-    StripPrefix  as        as         = '[]-    StripPrefix '[]        asbs       = asbs-    StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs-    StripPrefix (a ': as) (b ': asbs)-      = TypeError-        ( 'Text "StripPrefix: the first argument is not a prefix of the second."-        ':$$:-          'Text "Failed prefix: " ':<>: 'ShowType (a ': as)-        ':$$:-          'Text "Second argument: " ':<>: 'ShowType (b ': asbs)-        )-    StripPrefix (a ': as) '[]-      = TypeError-        ( 'Text "StripPrefix: the first argument is longer than the second."-        ':$$:-          'Text "Failed prefix: " ':<>: 'ShowType (a ': as)-        ':$$:-          'Text "The reduced second argument is empty."-        )---- | Remove suffix @bs@ from a list @asbs@ if @bs@ is a suffix; fail otherwise.-type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where-    StripSuffix  bs        bs         = '[]-    StripSuffix '[]        asbs       = asbs-    StripSuffix (a ': bs) (b ': bs)-      = TypeError-        ( 'Text "StripSuffix: the first argument is not a suffix of the second."-        ':$$:-          'Text "Failed match: "-            ':<>: 'ShowType ((a ': bs) ~ (b ': bs))-        )-    StripSuffix (b ': bs) '[]-      = TypeError-        ( 'Text "StripSuffix: the first argument is longer than the second."-        ':$$:-          'Text "Failed suffix: " ':<>: 'ShowType (b ': bs)-        ':$$:-          'Text "The reduced second argument is empty."-        )-    StripSuffix  bs       (a ': asbs) = a ': StripSuffix bs asbs---- | Returns the elements of a list in reverse order.-type family Reverse (xs :: [k]) :: [k] where-    -- Note: the goal is not to write a fast implementation,-    --       but make it easier for the type checker to simplify things.-    --       This is only going to be executed during compile time,-    --       so there is no real performance impact.-    Reverse '[] = '[]-    Reverse (x ': xs) = Snoc (Reverse xs) x- -- | Number of elements in a list. type family Length (xs :: [k]) :: Nat where     Length '[]       = 0@@ -169,59 +88,18 @@     Map f '[]       = '[]     Map f (x ': xs) = f x ': Map f xs +-- | Unmap a functor over the elements of a type list.+type family UnMap (f :: a -> b) (xs :: [b]) :: [a] where+    UnMap f '[]         = '[]+    UnMap f (f x ': ys) = x ': UnMap f ys+ -- | Check if an item is a member of a list. type family Elem (x :: k) (xs :: [k]) :: Constraint where     Elem x (x ': xs) = ()     Elem x (_ ': xs) = Elem x xs -type ListError k t-    = 'Text t ':$$:-    ( 'Text "Type-level error occured when operating on a list of kind "-      ':<>: 'ShowType [k] ':<>: 'Text "."-    )---- | Represent a triple of lists forming a relation @(as ++ bs) ~ asbs@-type ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) =-    ( asbs ~ Concat as bs-    , as   ~ StripSuffix bs asbs-    , bs   ~ StripPrefix as asbs-    )---- | Derive @ConcatList@ given @Concat@-evConcat :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])-          . (asbs ~ Concat as bs) :- ConcatList as bs asbs-evConcat = Sub $ unsafeCoerce-  ( Dict :: Dict-    ( asbs ~ Concat as bs-    , as   ~ as-    , bs   ~ bs-    )-  )---- | Derive @ConcatList@ given @StripSuffix@-evStripSuffix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])-               . (as ~ StripSuffix bs asbs) :- ConcatList as bs asbs-evStripSuffix = Sub $ unsafeCoerce-  ( Dict :: Dict-    ( asbs ~ asbs-    , as   ~ StripSuffix bs asbs-    , bs   ~ bs-    )-  )---- | Derive @ConcatList@ given @StripPrefix@-evStripPrefix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])-               . (bs ~ StripPrefix as asbs) :- ConcatList as bs asbs-evStripPrefix = Sub $ unsafeCoerce-  ( Dict :: Dict-    ( asbs ~ asbs-    , as   ~ as-    , bs   ~ StripPrefix as asbs-    )-  )- -- | Given a @Typeable@ list, infer this constraint for its parts.-inferTypeableCons :: forall (k :: Type) (ys :: [k]) (x :: k) (xs :: [k])+inferTypeableCons :: forall ys x xs                    . (Typeable ys, ys ~ (x ': xs))                   => Dict (Typeable x, Typeable xs) inferTypeableCons = case typeRep @ys of

@@ -0,0 +1,489 @@+{-# OPTIONS_HADDOCK hide, prune     #-}+{-# LANGUAGE AllowAmbiguousTypes     #-}+{-# LANGUAGE ConstraintKinds         #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE FunctionalDependencies  #-}+{-# LANGUAGE MultiParamTypeClasses   #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE TypeApplications        #-}+{-# LANGUAGE TypeFamilyDependencies  #-}+{-# LANGUAGE TypeInType              #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE UndecidableInstances    #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}+module Data.Type.List.Classes+  ( -- * Classes that simplify inference of type equalities+    SnocList, ReverseList, ConcatList+  , inferStripSuffix, inferStripPrefix, inferConcat+    -- auto-generating instances+  , nilInstSnocList, consInstSnocList, incohInstSnocList+  , consInstReverseList, incohInstReverseList+  , nilInstConcatList, consInstConcatList, incohInstConcatList+  ) where++import Data.Constraint          (Dict (..))+import Data.Constraint.Bare+import Data.Constraint.Deriving+import Data.Kind+import Data.Type.Equality+import Unsafe.Coerce            (unsafeCoerce)++import Data.Type.List.Families+import Data.Type.List.Internal+++-- | Represent a decomposition of a list by appending an element to its end.+class+    ( bs ~ Snoc as a, as ~ Init bs, a ~ Last bs+    , SnocListCtx as a bs, ConcatList as '[a] bs)+      => SnocList (as :: [k]) (a :: k) (bs :: [k])+            | as a -> bs, bs -> as a, as -> k, a -> a, bs -> k where++-- | Represent two lists that are `Reverse` of each other+class+    ( as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as+    , ReverseListCtx as bs)+      => ReverseList (as :: [k]) (bs :: [k])+            | as -> bs, bs -> as, as -> k, bs -> k++-- | Represent a triple of lists forming a relation @(as ++ bs) ~ asbs@+--+--   NB: functional dependency @bs asbs -> as@ does not seem to be possible,+--       because dependency checking happens before constraints checking+--        and does not take constraints into account.+class+    ( asbs ~ Concat as bs+    , as   ~ StripSuffix bs asbs+    , bs   ~ StripPrefix as asbs+    , ConcatListCtx1 as bs asbs+    , ConcatListCtx2 as bs asbs (bs == asbs)+    ) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k])+            | as bs -> asbs, as asbs -> bs --, bs asbs -> as+            , as -> k, bs -> k, asbs -> k+++++{- Type-dependent constraints - XxxCtx type familes++Extra "given" constraints provided by class instances via superclass mechanics+  (the constraints that depend on the expansion of the type variables)+++These type families give very handy evidence when you know the structure of+the type variables (e.g. as ~ '[] or as ~ (a' ': 'as)).++A huge problem with this approach is that sometimes I need to provide these+constraints for incoherent instances when I don't know how the type variables expand.+To workaround this, I need to provide such constraint families that:++  1. Their runtime representation is the same for all parameter values+  2. If a constraint does not make sense for a given parameter expansion,+     replace it with a useless but harmless alternative+  3. XxxCtx must not be in loop with Xxx+     (otherwise, typechecker stack overflow occurs at the call site)++ -}+++type family SnocListCtx (as :: [k]) (a :: k) (bs :: [k]) :: Constraint where+    SnocListCtx '[]       z bs =+      ( Head bs ~ z+      , Tail bs ~ '[]+      , bs ~ '[z]+      , UnreachableConstraint (SnocList (Tail '[]) (Head '[]) (Tail bs))+             "SnocListCtx '[] z bs -- SnocList (Tail '[]) (Head '[]) (Tail bs)"+      )+    SnocListCtx (a ': as) z bs =+      ( Head bs ~ a+      , Tail bs ~ Snoc as z+      , bs ~ (Head bs ': Head (Tail bs) ': Tail (Tail bs))+      , SnocList as z (Tail bs)+      )++type family ReverseListCtx (as :: [k]) (bs :: [k]) :: Constraint where+    ReverseListCtx '[]       bs =+      ( bs ~ '[]+      , UnreachableConstraint (ReverseList (Tail '[]) (Init bs))+             "ReverseListCtx '[] bs -- ReverseList (Tail '[]) (Init bs)"+      , UnreachableConstraint (SnocList (Init bs) (Head '[]) bs)+             "ReverseListCtx '[] bs -- SnocList (Init bs) (Head '[]) bs"+      )+    ReverseListCtx (a ': as) bs =+      ( bs ~ (Head bs ': Tail bs)+      , ReverseList as (Init bs)+      , SnocList (Init bs) a bs+      )++-- | Extra evidence provided by `ConcatList` in various cases+type family ConcatListCtx1 (as :: [k]) (bs :: [k]) (asbs :: [k]) :: Constraint where+    ConcatListCtx1 '[] bs asbs =+      ( asbs ~ bs+      , (bs == asbs) ~ 'True+      , UnreachableConstraint (Head '[] ~ Head asbs)+             "ConcatListCtx1 '[] bs asbs -- (Head '[] ~ Head asbs)"+      , UnreachableConstraint (ConcatList (Tail '[]) bs (Tail asbs))+             "ConcatListCtx1 '[] bs asbs -- ConcatList (Tail '[]) bs (Tail asbs)"+      , UnreachableConstraint (ConcatList (Init '[]) (Last '[] ': bs) asbs)+             "ConcatListCtx1 '[] bs asbs -- ConcatList (Init '[]) (Last '[] ': bs) asbs"+      )+    ConcatListCtx1 (a ': as) bs asbs =+      ( asbs ~ (a ': Tail asbs)+      , (bs == asbs) ~ 'False+      , a ~ Head asbs+      , ConcatList as bs (Tail asbs)+      , ConcatList (Init (a ': as)) (Last (a ': as) ': bs) asbs+      )+-- | Extra evidence provided by `ConcatList` in various cases+type family ConcatListCtx2 (as :: [k]) (bs :: [k]) (asbs :: [k]) (bsEq :: Bool) :: Constraint where+    ConcatListCtx2 as bs asbs 'True =+      ( as ~ '[]+      , bs ~ asbs+      , UnreachableConstraint (ConcatList (Tail as) bs (Tail asbs))+             "ConcatListCtx2 as bs asbs 'True -- ConcatList (Tail as) bs (Tail asbs)"+      )+    ConcatListCtx2 as bs (a ': asbs) 'False =+      ( as ~ (a ': Tail as)+      , a ~ Head as+      , ConcatList (Tail as) bs asbs+      )+    ConcatListCtx2 as bs '[] _ =+      ( as ~ '[]+      , bs ~ '[]+      , UnreachableConstraint (ConcatList (Tail as) bs (Tail '[]))+             "ConcatListCtx2 as bs '[] _ -- ConcatList (Tail as) bs (Tail '[])"+      )++{- Lookup class data constructors.++I use my plugin called ClassDict from constraints-deriving package.+It takes a data constructor for a given class and wraps it in Dict.++The signatures of the functions below are fully determined by the structure+of the corresponding type classes.+But as a user of the ClassDict API, I have to write these signatures by hand+  (otherwise the plugin displays a compile-time error with the correct signatures).++ -}++{-# ANN defineSnocList ClassDict #-}+defineSnocList :: forall (k :: Type) (as :: [k]) (a :: k) (bs :: [k])+                . ( bs ~ Snoc as a, as ~ Init bs, a ~ Last bs+                  , SnocListCtx as a bs+                  , ConcatList as '[a] bs+                  )+               => Dict (SnocList as a bs)+defineSnocList = defineSnocList++{-# ANN defineReverseList ClassDict #-}+defineReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])+                   . (as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as, ReverseListCtx as bs)+                  => Dict (ReverseList as bs)+defineReverseList = defineReverseList++{-# ANN defineConcatList ClassDict #-}+defineConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])+                  . ( asbs ~ Concat as bs+                    , as   ~ StripSuffix bs asbs+                    , bs   ~ StripPrefix as asbs+                    , ConcatListCtx1 as bs asbs+                    , ConcatListCtx2 as bs asbs (bs == asbs)+                    )+                 => Dict (ConcatList as bs asbs)+defineConcatList = defineConcatList+++{- Creating instances++The constraints defined about have a lot of recursive references to each other.+This makes defining instances using the standard syntax virtually impossible.++That is why I create most of the instances manually via the ClassDict+toInstance plugins.++Even on this way, there are some problems with passing dictionaries recursively;+if I just used `Dict` all the time and pattern match against it, I would get+a lot of <<loop>> or "unreachable instances" errors.+Instead, I use the `BareConstraint` abstract data type and pass it to `defineXxx`+functions as if constraints were vanilla values.++The functions below are helpers that break reference loops.+They also unsafely create all type equality constraints;+  it is very easy to introduce a bug here, because I bypass most of the typechecker.+ -}++++unsafeBareSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])+                    . BareConstraint (SnocListCtx as z bs)+                   -> BareConstraint (SnocList as z bs)+unsafeBareSnocList = runMagic m+  where+    m :: SnocListCtx as z bs =-> BareConstraint (SnocList as z bs)+    m | Dict <- unsafeEqTypes @bs @(Snoc as z)+      , Dict <- unsafeEqTypes @as @(Init bs)+      , Dict <- unsafeEqTypes @z @(Last bs)+      , Dict <- unsafeEqTypes @bs @(Concat as '[z])+      , Dict <- inferConcat @as @'[z] @bs+      = Magic (dictToBare $ defineSnocList @k @as @z @bs)++unsafeBareReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])+                       . BareConstraint (ReverseList bs as)+                      -> BareConstraint (ReverseListCtx as bs)+                      -> BareConstraint (ReverseList as bs)+unsafeBareReverseList = runMagic . runMagic m+  where+    m :: ReverseList bs as+      =-> ReverseListCtx as bs+      =-> BareConstraint (ReverseList as bs)+    m | Dict <- unsafeEqTypes @as @(Reverse bs)+      , Dict <- unsafeEqTypes @bs @(Reverse as)+      = Magic (Magic (dictToBare $ defineReverseList @k @as @bs))++unsafeBareConcatList ::+     forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])+  .  BareConstraint (ConcatListCtx1 as bs asbs)+  -> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))+  -> BareConstraint (ConcatList as bs asbs)+unsafeBareConcatList = runMagic . runMagic m+  where+    m :: ConcatListCtx1 as bs asbs+      =-> ConcatListCtx2 as bs asbs (bs == asbs)+      =-> BareConstraint (ConcatList as bs asbs)+    m | Dict <- unsafeEqTypes @as @(StripSuffix bs asbs)+      , Dict <- unsafeEqTypes @bs @(StripPrefix as asbs)+      , Dict <- unsafeEqTypes @asbs @(Concat as bs)+      = Magic (Magic (dictToBare $ defineConcatList @k @as @bs @asbs))+++unsafeBareSnocListCtx :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])+                       . BareConstraint (SnocList (Tail as) z (Tail bs))+                      -> BareConstraint (SnocListCtx as z bs)+unsafeBareSnocListCtx = runMagic m+  where+    m :: SnocList (Tail as) z (Tail bs) =-> BareConstraint (SnocListCtx as z bs)+    m = Magic (dictToBare d)+    d :: SnocList (Tail as) z (Tail bs) => Dict (SnocListCtx as z bs)+    d = unsafeCoerce $ Dict+      @(Head as ~ Head as, Tail bs ~ Tail bs, bs ~ bs, SnocList (Tail as) z (Tail bs))++unsafeBareReverseListCtx :: forall (k :: Type) (as :: [k]) (bs :: [k])+                          . BareConstraint (ReverseList (Tail as) (Init bs))+                         -> BareConstraint (ReverseListCtx as bs)+unsafeBareReverseListCtx+    = runMagic (runMagic m unsafeIncohBareSnocList)+  where+    m :: SnocList (Init bs) (Head as) bs+      =-> ReverseList (Tail as) (Init bs)+      =-> BareConstraint (ReverseListCtx as bs)+    m = Magic (Magic (dictToBare f))+    f :: ( SnocList (Init bs) (Last bs) bs+         , ReverseList (Tail as) (Init bs)+         )+      => Dict (ReverseListCtx as bs)+    f | Dict <- unsafeEqTypes @(Head as) @(Last bs)+      = unsafeCoerce (+            Dict @( bs ~ bs+                  , ReverseList (Tail as) (Init bs)+                  , SnocList (Init bs) (Head as) bs)+          )++unsafeBareConcatListCtx1 :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])+                          . BareConstraint (ConcatList (Tail as) bs (Tail asbs))+                         -> BareConstraint (ConcatList (Init as) (Last as ': bs) asbs)+                         -> BareConstraint (ConcatListCtx1 as bs asbs)+unsafeBareConcatListCtx1 = runMagic . runMagic m+  where+    m :: ConcatList (Tail as) bs (Tail asbs)+      =-> ConcatList (Init as) (Last as ': bs) asbs+      =-> BareConstraint (ConcatListCtx1 as bs asbs)+    m = Magic (Magic (dictToBare d))+    d :: ( ConcatList (Tail as) bs (Tail asbs)+         , ConcatList (Init as) (Last as ': bs) asbs)+      => Dict (ConcatListCtx1 as bs asbs)+    d = unsafeCoerce $ Dict+      @( asbs ~ asbs, (bs == asbs) ~ (bs == asbs)+       , Head asbs ~ Head asbs+       , ConcatList (Tail as) bs (Tail asbs)+       , ConcatList (Init as) (Last as ': bs) asbs+       )++unsafeBareConcatListCtx2 :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])+                          . BareConstraint (ConcatList (Tail as) bs (Tail asbs))+                         -> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))+unsafeBareConcatListCtx2 = runMagic m+  where+    m :: ConcatList (Tail as) bs (Tail asbs)+      =-> BareConstraint (ConcatListCtx2 as bs asbs (bs == asbs))+    m = Magic (dictToBare d)+    d :: ConcatList (Tail as) bs (Tail asbs)+      => Dict (ConcatListCtx2 as bs asbs (bs == asbs))+    d = unsafeCoerce $ Dict+      @(as ~ as, Head as ~ Head as, ConcatList (Tail as) bs (Tail asbs))+++{- Recursive bindings for generic incoherent instances++Since all three classes consist solely of some combination of equality constraints+(nested inside algebraic class constructors and constraint tuples),+one can construct instances  "from nothing".+These are the three functions below.++ -}++unsafeIncohBareSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])+                         . BareConstraint (SnocList as z bs)+unsafeIncohBareSnocList = unsafeBareSnocList $+    unsafeBareSnocListCtx @k @as @z @bs unsafeIncohBareSnocList++unsafeIncohBareReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])+                            . BareConstraint (ReverseList as bs)+unsafeIncohBareReverseList = unsafeBareReverseList @k @as @bs+    unsafeIncohBareReverseList+    (unsafeBareReverseListCtx @k @as @bs unsafeIncohBareReverseList)++unsafeIncohBareConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k])+                           . BareConstraint (ConcatList as bs asbs)+unsafeIncohBareConcatList = unsafeBareConcatList @k @as @bs @asbs+    (unsafeBareConcatListCtx1 @k @as @bs @asbs unsafeIncohBareConcatList unsafeIncohBareConcatList)+    (unsafeBareConcatListCtx2 @k @as @bs @asbs unsafeIncohBareConcatList)+++++{- Declaring instances++The simplest instances can be created using the vanilla syntax;+the rest is derived via the three recursive definitions above.+ -}++-- instance SnocList '[] a '[a] where+{-# ANN nilInstSnocList (ToInstance NoOverlap) #-}+nilInstSnocList :: forall (k :: Type) (a :: k)+                 . Dict (SnocList '[] a '[a])+nilInstSnocList+  | Dict <- nilInstConcatList @k @'[a]+    = defineSnocList @k @'[] @a @'[a]++-- instance SnocList as z bs => SnocList (a ': as) z (a ': bs)+{-# ANN consInstSnocList (ToInstance NoOverlap) #-}+consInstSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k]) (a :: k) (b :: k)+                  . SnocList as z (b ': bs)+                 => Dict (SnocList (a ': as) z (a ': b ': bs))+consInstSnocList+  | Dict <- unsafeEqTypes @(a ': b ': bs) @(Snoc (a ': as) z)+  , Dict <- unsafeEqTypes @(a ': as) @(Init (a ': b ': bs))+  , Dict <- unsafeEqTypes @z @(Last (a ': b ': bs))+  , Dict <- consInstConcatList @_ @as @'[z] @(b ': bs) @a+    = defineSnocList @k @(a ': as) @z @(a ': b ': bs)+++-- instance {-# INCOHERENT #-} SnocList as z bs+{-# ANN incohInstSnocList (ToInstance Incoherent) #-}+incohInstSnocList :: forall (k :: Type) (as :: [k]) (z :: k) (bs :: [k])+                   . bs ~ Snoc as z+                  => Dict (SnocList as z bs)+incohInstSnocList = bareToDict $ unsafeIncohBareSnocList @k @as @z @bs+++instance ReverseList ('[] :: [k]) ('[] :: [k])++-- instance (ReverseList as bs', SnocList bs' a (b ': bs))+--          => ReverseList (a ': as) (b ': bs)+{-# ANN consInstReverseList (ToInstance NoOverlap) #-}+consInstReverseList :: forall (k :: Type)+                              (a :: k) (as :: [k]) (b :: k) (bs :: [k])+                     . (ReverseList as (Init (b ': bs)), SnocList (Init (b ': bs)) a (b ': bs))+                    => Dict (ReverseList (a ': as) (b ': bs))+consInstReverseList = bareToDict d+  where+    d = runMagic m (rev d)++    m :: ReverseList (b ': bs) (a ': as)+      =-> BareConstraint (ReverseList (a ': as) (b ': bs))+    m = Magic f+    f :: ReverseList (b ': bs) (a ': as)+      => BareConstraint (ReverseList (a ': as) (b ': bs))+    f | Dict <- unsafeEqTypes @(a ': as) @(Reverse (b ': bs))+      , Dict <- unsafeEqTypes @(b ': bs) @(Reverse (a ': as))+      = dictToBare $ defineReverseList++    {- Since both classes, ReverseList and SnocList actually bear no runtime references+       to their parameters, the only thing that matters is the length of the list+         (the only parameter that affects the content of an instance).+       Thus, I can cast the class instances between the lists of the same lengths.+     -}+    rev :: BareConstraint (ReverseList (a ': as) (b ': bs))+        -> BareConstraint (ReverseList (b ': bs) (a ': as))+    rev = unsafeCoerce+++{-# ANN incohInstReverseList (ToInstance Incoherent) #-}+incohInstReverseList :: forall (k :: Type) (as :: [k]) (bs :: [k])+                      . bs ~ Reverse as+                     => Dict (ReverseList as bs)+incohInstReverseList = bareToDict $ unsafeIncohBareReverseList @k @as @bs+++++-- instance {-# INCOHERENT #-} ConcatList as '[] as+{-# ANN incohInstConcatList (ToInstance Incoherent) #-}+incohInstConcatList :: forall (k :: Type) (as :: [k])+                     . Dict (ConcatList as ('[] :: [k]) as)+incohInstConcatList = bareToDict $ unsafeIncohBareConcatList @k @as @'[] @as++-- instance ConcatList '[] bs bs+{-# ANN nilInstConcatList (ToInstance NoOverlap) #-}+nilInstConcatList :: forall (k :: Type) (bs :: [k])+                    . Dict (ConcatList '[] bs bs)+nilInstConcatList+  | Dict <- unsafeEqTypes @(bs == bs) @'True+    = defineConcatList @k @'[] @bs @bs++-- instance ConcatList  as bs asbs => ConcatList (a ': as) bs (a ': asbs)+{-# ANN consInstConcatList (ToInstance NoOverlap) #-}+consInstConcatList :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]) (a :: k)+                    . ConcatList as bs asbs+                   => Dict (ConcatList (a ': as) bs (a ': asbs))+consInstConcatList+  | Dict <- unsafeEqTypes @(bs == (a ': asbs)) @'False+  , Dict <- unsafeEqTypes @(a ': as)   @(StripSuffix bs (a ': asbs))+  , Dict <- unsafeEqTypes @bs          @(StripPrefix (a ': as) (a ': asbs))+  , Dict <- unsafeEqTypes @(a ': asbs) @(Concat (a ': as) bs)+    = let x :: ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)+            => Dict (ConcatList (a ': as) bs (a ': asbs))+          x = defineConcatList @k @(a ': as) @bs @(a ': asbs)+          m :: ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs)+            =-> BareConstraint (ConcatList (a ': as) bs (a ': asbs))+          m = Magic (dictToBare x)++          shiftedCL :: BareConstraint+            (ConcatList (Init (a : as)) (Last (a : as) : bs) (a : asbs))+          shiftedCL = unsafeIncohBareConcatList+      in bareToDict $ runMagic m shiftedCL+++++-- | Derive @ConcatList@ given @Concat@+inferConcat :: forall as bs asbs+             . asbs ~ Concat as bs+            => Dict (ConcatList as bs asbs)+inferConcat = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs++-- | Derive @ConcatList@ given @StripSuffix@+inferStripSuffix :: forall as bs asbs+                  . as ~ StripSuffix bs asbs+                 => Dict (ConcatList as bs asbs)+inferStripSuffix = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs++-- | Derive @ConcatList@ given @StripPrefix@+inferStripPrefix :: forall as bs asbs+                  . bs ~ StripPrefix as asbs+                 => Dict (ConcatList as bs asbs)+inferStripPrefix = bareToDict $ unsafeIncohBareConcatList @_ @as @bs @asbs

@@ -0,0 +1,84 @@+{-# OPTIONS_HADDOCK hide, prune     #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-}+module Data.Type.List.Families+  ( Head, Tail+  , Snoc, Init, Last, Reverse+  , StripSuffix, StripPrefix, Concat+    -- * Internals+  , List (..), RunList, Snoc', Reverse'+  ) where+++-- | Extract the first element of a list, which must be non-empty.+type family Head (xs :: [k]) :: k where+    Head (x ': _)     = x++-- | Extract the elements after the head of a list, which must be non-empty.+type family Tail (xs :: [k]) :: [k] where+    Tail (_ ': xs)    = xs++-- | Extract the last element of a list, which must be non-empty.+type family Last (xs :: [k]) :: k where+    Last '[x]         = x+    Last (_ ': xs)    = Last xs++-- | Extract all but last elements of a list, which must be non-empty.+type family Init (xs :: [k]) = (ys :: [k]) | ys -> k where+    Init ('[x] :: [k]) = ('[] :: [k])+    Init (x ': xs)     = x ': Init xs++-- | Appending a list on the other side (injective).+type Snoc (xs :: [k]) (x :: k) = (RunList (Snoc' xs x :: List k) :: [k])++-- | Reverse elements of a list (injective).+type Reverse (xs :: [k]) = (RunList (Reverse' xs :: List k) :: [k])++-- | A helper data type that makes possible injective `Snoc` and `Reverse` families.+--+--   It assures GHC type checker that the `Snoc` operation on a non-empty list+--   yields a list that contains at least two elements.+data List k+  = Empty+  | Single k+  | TwoOrMore [k]+    -- ^ An important invariant: the argument list contains at least two elements.++type family RunList (xs :: List k) = (ys :: [k]) | ys -> k xs where+    RunList ('Empty :: List k)          = ('[] :: [k])+    RunList ('Single x)                 = '[x]+    RunList ('TwoOrMore (x ': y ': xs)) = x ': y ': xs++type family Snoc' (xs :: [k]) (x :: k) = (ys :: List k) | ys -> k xs x where+    Snoc' '[]       y = 'Single y+    Snoc' (x ': xs) y = 'TwoOrMore (x ': RunList (Snoc' xs y))++type family Reverse' (xs :: [k]) = (ys :: List k) | ys -> k xs where+    Reverse' ('[] :: [k])   = ('Empty :: List k)+    Reverse' '[x]           = 'Single x+    Reverse' (y ': x ': xs) = 'TwoOrMore (Snoc (RunList (Reverse' (x ': xs))) y)+++-- | Append two lists.+type family Concat (as :: [k]) (bs :: [k]) :: [k] where+    Concat  as       '[]       = as -- "incoherent instance"+    Concat '[]        bs       = bs+    Concat (a ': as)  bs       = a ': Concat as bs++-- | Remove prefix @as@ from a list @asbs@ if @as@ is a prefix; fail otherwise.+type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where+    StripPrefix  as        as         = '[] -- "incoherent instance"+    StripPrefix '[]        bs         = bs+    StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs++-- | Remove suffix @bs@ from a list @asbs@ if @bs@ is a suffix; fail otherwise.+type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where+    StripSuffix '[]        as         = as -- "incoherent instance"+    StripSuffix  bs        bs         = '[]+    StripSuffix  bs       (a ': asbs) = a ': StripSuffix bs asbs

@@ -1,67 +0,0 @@-{-# OPTIONS_GHC -fobject-code   #-}-{-# OPTIONS_HADDOCK hide, prune #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Type.List.InjectiveSnoc--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ A small core plugin to make GHC think that @Snoc@ is injective----------------------------------------------------------------------------------------module Data.Type.List.InjectiveSnoc ( plugin ) where---import           CoAxiom    (CoAxBranch (..), CoAxiom (..), mapAccumBranches)-import           Data.Maybe (fromMaybe)-import           GhcPlugins---- NB: check out---  https://github.com/ghc/ghc/blob/bf73419518ca550e85188616f860961c7e2a336b/compiler/typecheck/TcTypeNats.hs---  for further ideas.---  Maybe, I can use BuiltInSynFamily to do a lot of super cool stuff!---- | A small core plugin to make GHC think that @Snoc@ is injective-plugin :: Plugin-plugin = defaultPlugin-  { installCoreToDos =-      const $ pure . (CoreDoPluginPass "InjectiveSnoc" injectiveSnocPass :)-  }--injectiveSnocPass :: ModGuts -> CoreM ModGuts-injectiveSnocPass = pure . modSnocFam updateSnocFam--modSnocFam :: (TyCon -> TyCon) -> ModGuts -> ModGuts-modSnocFam f guts = guts {mg_tcs = map g (mg_tcs guts)}-  where-    g tc-      | nameOccName (tyConName tc) == mkTcOcc "Snoc" = f tc-      | otherwise = tc--updateSnocFam :: TyCon -> TyCon-updateSnocFam tc = fromMaybe tc $ do-    axiom <- isClosedSynFamilyTyConWithAxiom_maybe tc-    let newAxiom = axiom-          { co_ax_tc = newTc-          , co_ax_branches = mapAccumBranches f (co_ax_branches axiom)-          }-        f _ b = b { cab_rhs = repTc (cab_rhs b) }-        repTc t = case splitTyConApp_maybe t of-          Just (c, ts)-            | nameOccName (tyConName c) == mkTcOcc "Snoc"-              -> mkTyConApp newTc $ map repTc ts-            | otherwise-              -> mkTyConApp c $ map repTc ts-          Nothing-              -> t-        newTc = mkFamilyTyCon-          (tyConName tc)    -- Name-          (tyConBinders tc)   -- [TyConBinder]-          (tyConResKind tc) -- Kind-          (famTcResVar tc)  -- Maybe Name-          (ClosedSynFamilyTyCon (Just newAxiom)) -- FamTyConFlav-          (tyConAssoc_maybe tc)  -- Maybe Class-          -- Injectivity copied from a dummy injective TF with the same head-          (Injective [True, True, True])     -- Injectivity-    return newTc

@@ -1,27 +1,58 @@-{-# OPTIONS_GHC -fobject-code       #-}-{-# OPTIONS_GHC -fplugin Data.Type.List.InjectiveSnoc #-} {-# OPTIONS_HADDOCK hide, prune     #-}-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE PolyKinds              #-}-{-# LANGUAGE TypeFamilyDependencies #-}-{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE AllowAmbiguousTypes     #-}+{-# LANGUAGE ConstraintKinds         #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE ExplicitNamespaces      #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE KindSignatures          #-}+{-# LANGUAGE MultiParamTypeClasses   #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE TypeApplications        #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE UndecidableSuperClasses #-}+module Data.Type.List.Internal+  ( UnreachableConstraint (..)+  , type (=->) (..), runMagic, unsafeEqTypes+  ) where -{-# LANGUAGE TypeInType             #-}-{-# LANGUAGE UndecidableInstances   #-}------------------------------------------------------------------------------------ |--- Module      :  Data.Type.List.Internal--- Copyright   :  (c) Artem Chirkin--- License     :  BSD3------ Thanks to @Data.Type.List.InjectiveSnoc@, @Snoc@ appears to be injective--- for an oustide viewer.----------------------------------------------------------------------------------------module Data.Type.List.Internal ( Snoc ) where+import Data.Constraint      (Dict (..))+import Data.Constraint.Bare+import Data.Kind+import Data.Proxy+import GHC.TypeLits+import Unsafe.Coerce        (unsafeCoerce) --- | Appending a list on the other side.-type family Snoc (xs :: [k]) (x :: k) = (ys :: [k]) where-    Snoc (x ': xs) y = x ': Snoc xs y-    Snoc '[]       y = '[y]++{- |+This class should have the same runtime representation as its parameter ctx.+The point is to make sure GHC won't segfault if it mixes up `UnreachableConstraint ctx`+with `ctx` itself:++  If GHC mistakenly recognizes `UnreachableConstraint ctx` dictionary as+   `ctx` dictionary, a call to this dictionary should return an error+    as defined by `unreachable` function rather than the panic.++Note, I must not put `ctx` in the superclass position to prevent GHC from+trying to use it.+ -}+class UnreachableConstraint (ctx :: Constraint) (msg :: Symbol) where+  unreachable :: BareConstraint ctx++instance KnownSymbol msg+      => UnreachableConstraint ctx msg where+  unreachable = error $ "Unreachable constraint:: " ++ symbolVal (Proxy @msg)+++newtype c =-> r = Magic (c => r)+infixr 0 =->++runMagic :: (c =-> r) -> BareConstraint c -> r+runMagic = unsafeCoerce+{-# NOINLINE runMagic #-}+++unsafeEqTypes :: forall a b+               . Dict (a ~ b)+unsafeEqTypes = unsafeCoerce (Dict :: Dict (a ~ a))

@@ -1,17 +1,19 @@-{-# LANGUAGE CPP                  #-}-{-# LANGUAGE ConstraintKinds      #-}-{-# LANGUAGE DataKinds            #-}-{-# LANGUAGE ExplicitForAll       #-}-{-# LANGUAGE GADTs                #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeOperators        #-}-{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE CPP                    #-}+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE ExplicitForAll         #-}+{-# LANGUAGE ExplicitNamespaces     #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE TypeFamilies           #-}+{-# LANGUAGE TypeFamilyDependencies #-}+{-# LANGUAGE TypeOperators          #-}+{-# LANGUAGE UndecidableInstances   #-} #if __GLASGOW_HASKELL__ >= 806-{-# LANGUAGE NoStarIsType         #-}+{-# LANGUAGE NoStarIsType           #-} #endif  -{-# LANGUAGE FlexibleContexts     #-} -------------------------------------------------------------------------------- -- | -- Module      :  Data.Type.List@@ -26,6 +28,7 @@ module Data.Type.Lits   ( -- * Kinds     TN.Nat, TL.Symbol+  , KindOf, KindOfEl     -- * Linking type and value level   , TN.KnownNat, TN.natVal, TN.natVal'   , TL.KnownSymbol, TL.symbolVal, TL.symbolVal'@@ -35,6 +38,7 @@     -- * Functions on type literals   , type (+), type (*), type (^), type (-)   , type TN.Div, type TN.Mod, type TN.Log2+  , type Min, type Max   , TL.AppendSymbol, ShowNat   , TN.CmpNat, TL.CmpSymbol, type (<=)   , SOrdering (..), cmpNat, cmpSymbol@@ -101,15 +105,45 @@     GT -> unsafeCoerce SGT {-# INLINE cmpSymbol #-} +-- | Miminum among two type-level naturals.+type Min (a :: TN.Nat) (b :: TN.Nat) = Min' a b (TN.CmpNat a b)++-- | Maximum among two type-level naturals.+type Max (a :: TN.Nat) (b :: TN.Nat) = Min' a b (TN.CmpNat a b)++type family Min' (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: TN.Nat where+    Min' a _ 'LT = a+    Min' a _ 'EQ = a+    Min' _ b 'GT = b++type family Max' (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: TN.Nat where+    Max' _ b 'LT = b+    Max' _ b 'EQ = b+    Max' a _ 'GT = a+ -- | Comparison of type-level naturals, as a constraint. type (<=) (a :: TN.Nat) (b :: TN.Nat) = LE a b (TN.CmpNat a b) -type family LE (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering) :: Constraint where-    LE _ _ 'LT = ()-    LE _ _ 'EQ = ()-    LE a b 'GT = TL.TypeError+type family LE (a :: TN.Nat) (b :: TN.Nat) (r :: Ordering)+                                         = (y :: Constraint) | y -> r where+    LE a b 'LT = ('LT ~ TN.CmpNat a b)+    LE a b 'EQ = ('EQ ~ TN.CmpNat a b)+    LE a b 'GT = ('GT ~ TL.TypeError       ('TL.Text "Cannot deduce type-level Nat relation: "           'TL.:<>: 'TL.ShowType a           'TL.:<>: 'TL.Text " <= "           'TL.:<>: 'TL.ShowType b-      )+      ))+++-- | Get the kind of a given type.+--   Useful when we don't want to introduce another type parameter into+--   a type signature (because the kind is determined by the type),+--   but need to have some constraints on the type's kind.+type KindOf   (t :: k) = k++-- | Get the kind of a given list type.+--   Useful when we don't want to introduce another type parameter into+--   a type signature (because the kind is determined by the type),+--   but need to have some constraints on the type's kind.+type KindOfEl (ts :: [k]) = k

@@ -4,6 +4,7 @@ {-# LANGUAGE DataKinds                 #-} {-# LANGUAGE DeriveDataTypeable        #-} {-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE ExplicitNamespaces        #-} {-# LANGUAGE FlexibleContexts          #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE GADTs                     #-}@@ -25,6 +26,7 @@ #if __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType              #-} #endif+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-} ----------------------------------------------------------------------------- -- | -- Module      :  Numeric.Dimensions.Dim@@ -47,21 +49,24 @@ -----------------------------------------------------------------------------  module Numeric.Dimensions.Dim-  ( -- * @Dim@ -- a @Nat@-indexed dimension+  ( -- * @Dim@: a @Nat@-indexed dimension     -- ** Type level numbers that can be unknown.-    XNat (..), XN, N, XNatType (..)+    Nat, XNat (..), XN, N+  , DimType (..), KnownDimType(..), DimKind (..), KnownDimKind(..)     -- ** Term level dimension   , Dim ( D, Dn, Dx         , D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, D10, D11, D12, D13         , D14, D15, D16, D17, D18, D19, D20, D21, D22, D23, D24, D25         )   , SomeDim-  , KnownDim (..), BoundedDim (..), minDim, KnownXNatType (..), FixedDim+  , KnownDim (..), withKnownXDim+  , BoundedDim (..), minimalDim, ExactDim, FixedDim   , dimVal, dimVal', typeableDim, someDimVal   , sameDim, sameDim'+  , lessOrEqDim, lessOrEqDim'   , compareDim, compareDim'   , constrainBy, relax-    -- * Simple Dim arithmetics+    -- ** Simple Dim arithmetics     --     --   The functions below create singleton values that work as a witness     --   of `KnownDim` instance for type-level Nat operations.@@ -76,63 +81,115 @@     --   The good side is the confidence that they behave exactly as     --   their @Word@ counterparts.   , plusDim, minusDim, minusDimM, timesDim, powerDim, divDim, modDim, log2Dim+  , minDim, maxDim     -- ** Re-export part of `Data.Type.Lits` for convenience-  , Nat, CmpNat, SOrdering (..), type (+), type (-), type (*), type (^), type (<=)-    -- ** Inferring kind of type-level dimension-  , KnownDimKind (..), DimKind (..)-    -- * @Dims@ -- a list of dimensions-  , Dims, SomeDims (..), Dimensions (..), BoundedDims (..), minDims-  , TypedList ( Dims, XDims, AsXDims, KnownDims+  , CmpNat, SOrdering (..), type (+), type (-), type (*), type (^), type (<=)+  , Min, Max+    -- * @Dims@: a list of dimensions+  , Dims, SomeDims (..), Dimensions (..), withKnownXDims+  , BoundedDims (..), DimsBound, minimalDims+  , ExactDims, FixedDims, inferFixedDims, inferExactFixedDims+  , TypedList ( Dims, XDims, KnownDims               , U, (:*), Empty, TypeList, Cons, Snoc, Reverse)   , typeableDims, inferTypeableDims   , listDims, someDimsVal, totalDim, totalDim'   , sameDims, sameDims'-  , inSpaceOf, asSpaceOf-  , xDims, xDims'+  , inSpaceOf   , stripPrefixDims, stripSuffixDims-    -- ** Type-level programming-    --   Provide type families to work with lists of dimensions (`[Nat]` or `[XNat]`)-  , AsXDims, AsDims, FixedDims, KnownXNatTypes     -- ** Re-export type list   , RepresentableList (..), TypeList, types   , order, order'+  , KindOf, KindOfEl+#if !(defined(__HADDOCK__) || defined(__HADDOCK_VERSION__))+    -- hide a plugin-related func+  , incohInstBoundedDims+#endif   ) where  -import           Data.Bits         (countLeadingZeros, finiteBitSize)+import           Data.Bits                (countLeadingZeros, finiteBitSize) import           Data.Coerce import           Data.Constraint-import           Data.Data         hiding (TypeRep, typeRep, typeRepTyCon)-import           Data.Kind         (Constraint, Type)-import qualified Data.List         (stripPrefix)+import           Data.Constraint.Bare+import           Data.Constraint.Deriving+import           Data.Data                hiding (TypeRep, typeRep,+                                           typeRepTyCon)+import           Data.Kind                (Type)+import qualified Data.List                (stripPrefix) import           Data.Type.List+import           Data.Type.List.Internal import           Data.Type.Lits-import           GHC.Exts          (Proxy#, proxy#, unsafeCoerce#)-import qualified GHC.Generics      as G-import           Numeric.Natural   (Natural)+import           GHC.Exts                 (Proxy#, RuntimeRep, TYPE, proxy#)+import qualified GHC.Generics             as G+import           Numeric.Natural          (Natural) import           Numeric.TypedList-import qualified Text.Read         as Read-import qualified Text.Read.Lex     as Read+import qualified Text.Read                as Read+import qualified Text.Read.Lex            as Read import           Type.Reflection-+import           Unsafe.Coerce            (unsafeCoerce)  -- | Either known or unknown at compile-time natural number data XNat = XN Nat | N Nat -- | Unknown natural number, known to be not smaller than the given Nat-type XN (n::Nat) = 'XN n+type XN = 'XN -- | Known natural number-type N (n::Nat) = 'N n+type N = 'N --- | Find out whether @XNat@ is of known or constrained type.-data XNatType :: XNat -> Type where+-- | GADT to support `KnownDimType` type class.+--   Find out if this type variable is a @Nat@ or @XNat@,+--   and whether @XNat@ is of known or constrained type.+data DimType (d :: k) where+    -- | This is a plain @Nat@+    DimTNat   :: DimType (n :: Nat)     -- | Given @XNat@ is known-    Nt  :: XNatType ('N n)+    DimTXNatN :: DimType (N n)     -- | Given @XNat@ is constrained unknown-    XNt :: XNatType ('XN m)+    DimTXNatX :: DimType (XN m) --- | Same as `SomeNat`-type SomeDim = Dim ('XN 0)+-- | GADT to support `KnownDimKind` type class.+--   Match against its constructors to know if @k@ is @Nat@ or @XNat@+data DimKind (k :: Type) where+    -- | Working on @Nat@.+    DimKNat  :: DimKind Nat+    -- | Working on @XNat@.+    DimKXNat :: DimKind XNat +-- | Figure out whether the type-level dimension is `Nat`, or `N Nat`, or `XN Nat`.+class KnownDimType d where+    -- | Pattern-match against this to out the value (type) of the dim type variable.+    dimType :: DimType d++-- | Figure out whether the type-level dimension is `Nat` or `XNat`.+class KnownDimKind k where+    -- | Pattern-match against this to out the kind of the dim type variable.+    dimKind :: DimKind k++instance KnownDimType (n :: Nat) where+    dimType = DimTNat+    {-# INLINE dimType #-}++instance KnownDimType ('N n :: XNat) where+    dimType = DimTXNatN+    {-# INLINE dimType #-}++instance KnownDimType ('XN n :: XNat) where+    dimType = DimTXNatX+    {-# INLINE dimType #-}++instance KnownDimKind Nat where+    dimKind = DimKNat+    {-# INLINE dimKind #-}++instance KnownDimKind XNat where+    dimKind = DimKXNat+    {-# INLINE dimKind #-}++instance Class (KnownDimKind k) (KnownDimType (n :: k)) where+    cls = Sub $ case dimType @n of+      DimTNat   -> Dict+      DimTXNatN -> Dict+      DimTXNatX -> Dict+ -- | Singleton type to store type-level dimension value. -- --   On the one hand, it can be used to let type-inference system know@@ -146,39 +203,61 @@ newtype Dim (x :: k) = DimSing Word   deriving ( Typeable ) +-- | Same as `SomeNat`+type SomeDim = Dim (XN 0)+ -- | Type-level dimensionality.-type Dims (xs :: [k]) = TypedList Dim xs+type Dims = (TypedList Dim :: [k] -> Type) +#define PLEASE_STYLISH_HASKELL \+  forall d . KnownDimType d => \+  (KindOf d ~ Nat, KnownDim d) => \+  Dim d+ -- | Match against this pattern to bring `KnownDim` instance into scope.-pattern D :: forall (n :: Nat) . () => KnownDim n => Dim n-pattern D <- (dimEv -> Dict)+pattern D :: PLEASE_STYLISH_HASKELL+pattern D <- (patDim (dimType @d) -> PatNat)   where-    D = dim @n-{-# COMPLETE D #-}+    D = dim @d+#undef PLEASE_STYLISH_HASKELL ++#define PLEASE_STYLISH_HASKELL \+  forall d . KnownDimType d => \+  forall (n :: Nat) . (KindOf d ~ XNat, d ~ N n) => \+  Dim n -> Dim d+ -- | Statically known `XNat`-pattern Dn :: forall (xn :: XNat) . KnownXNatType xn-           => forall (n :: Nat) . (KnownDim n, xn ~ 'N n) => Dim n -> Dim xn-pattern Dn k <- (dimXNEv (xNatType @xn) -> PatN k)+pattern Dn :: PLEASE_STYLISH_HASKELL+pattern Dn k <- (patDim (dimType @d) -> PatXNatN k)   where     Dn k = coerce k+#undef PLEASE_STYLISH_HASKELL +#define PLEASE_STYLISH_HASKELL \+  forall d . KnownDimType d => \+  forall (m :: Nat) (n :: Nat) . (KindOf d ~ XNat, d ~ XN m, m <= n) => \+  Dim n -> Dim d+ -- | `XNat` that is unknown at compile time. --   Same as `SomeNat`, but for a dimension: --   Hide dimension size inside, but allow specifying its minimum possible value.-pattern Dx :: forall (xn :: XNat) . KnownXNatType xn-           => forall (n :: Nat) (m :: Nat)-            . (KnownDim n, m <= n, xn ~ 'XN m) => Dim n -> Dim xn-pattern Dx k <- (dimXNEv (xNatType @xn) -> PatXN k)+pattern Dx :: PLEASE_STYLISH_HASKELL+pattern Dx k <- (patDim (dimType @d) -> PatXNatX k)   where     Dx k = coerce k+#undef PLEASE_STYLISH_HASKELL++{-# COMPLETE D #-} {-# COMPLETE Dn, Dx #-}+{-# COMPLETE D, Dn, Dx #-}  -- | This class provides the `Dim` associated with a type-level natural. -----   Note, kind of the @KnownDim@ argument is always @Nat@, because+--   Note, kind of the @KnownDim@ argument is usually @Nat@, because --     it is impossible to create a unique @KnownDim (XN m)@ instance.-class KnownDim (n :: Nat) where+--   Nevertheless, you can have @KnownDim (N n)@, which is useful in some cases.+class KnownDim n where     -- | Get value of type-level dim at runtime.     --     --   Note, this function is supposed to be used with @TypeApplications@.@@ -198,21 +277,27 @@ -- | Get a minimal or exact bound of a @Dim@. -- --   To satisfy the @BoundedDim@ means to be equal to @N n@ or be not less than @XN m@.-class KnownDimKind k => BoundedDim (n :: k) where+class (KnownDimKind (KindOf d), KnownDimType d, KnownDim (DimBound d))+    => BoundedDim d where     -- | Minimal or exact bound of a @Dim@.     --   Useful for indexing: it is safe to index something by an index less than     --   @DimBound n@ (for both @Nat@ and @Xnat@ indexed dims).-    type family DimBound n :: Nat+    type family DimBound d :: Nat     -- | Get such a minimal @Dim (DimBound n)@, that @Dim n@ is guaranteed     --   to be not less than @dimBound@ if @n ~ XN a@,-  --     otherwise, the return @Dim@ is the same as @n@.-    dimBound :: Dim (DimBound n)-    -- | If the runtime value of @Dim y@ satisfies @dimBound @k @x@,+    --     otherwise, the return @Dim@ is the same as @n@.+    dimBound :: Dim (DimBound d)+    -- | If the runtime value of @Dim y@ satisfies @dimBound @x@,     --   then coerce to @Dim x@. Otherwise, return @Nothing@.     --     --   To satisfy the @dimBound@ means to be equal to @N n@ or be not less than @XN m@.-    constrainDim :: forall (l :: Type) (y :: l) . Dim y -> Maybe (Dim n)+    constrainDim :: forall y . Dim y -> Maybe (Dim d) +-- | Returns the minimal @Dim@ that satisfies the @BoundedDim@ constraint+--   (this is the exact @dim@ for @Nat@s and the minimal bound for @XNat@s).+minimalDim :: forall n . BoundedDim n => Dim n+minimalDim = coerce (dimBound @n)+{-# INLINE minimalDim #-}  instance KnownDim n => BoundedDim (n :: Nat) where     type DimBound n = n@@ -223,8 +308,8 @@        | otherwise       = Nothing     {-# INLINE constrainDim #-} -instance KnownDim n => BoundedDim ('N n) where-    type DimBound ('N n) = n+instance KnownDim n => BoundedDim (N n) where+    type DimBound (N n) = n     dimBound = dim @n     {-# INLINE dimBound #-}     constrainDim (DimSing y)@@ -232,7 +317,7 @@        | otherwise       = Nothing     {-# INLINE constrainDim #-} -instance KnownDim m => BoundedDim ('XN m) where+instance KnownDim m => BoundedDim (XN m) where     type DimBound ('XN m) = m     dimBound = dim @m     {-# INLINE dimBound #-}@@ -241,33 +326,20 @@        | otherwise       = Nothing     {-# INLINE constrainDim #-} -minDim :: forall (k :: Type) (d :: k) . BoundedDim d => Dim d-minDim = coerce (dimBound @k @d)---- | Find out the type of `XNat` constructor-class KnownXNatType (n :: XNat) where-    -- | Pattern-match against this to out the type of `XNat` constructor-    xNatType :: XNatType n--instance KnownXNatType ('N n) where-    xNatType = Nt-    {-# INLINE xNatType #-}--instance KnownXNatType ('XN n) where-    xNatType = XNt-    {-# INLINE xNatType #-}- -- | Similar to `natVal` from `GHC.TypeNats`, but returns `Word`.-dimVal :: forall (k :: Type) (x :: k) . Dim (x :: k) -> Word+dimVal :: forall x . Dim x -> Word dimVal = coerce {-# INLINE dimVal #-}  -- | Similar to `natVal` from `GHC.TypeNats`, but returns `Word`.-dimVal' :: forall (n :: Nat) . KnownDim n => Word+dimVal' :: forall n . KnownDim n => Word dimVal' = coerce (dim @n) {-# INLINE dimVal' #-}  -- | Construct a @Dim n@ if there is an instance of @Typeable n@ around.+--+--   Note: we can do this only for @Nat@-indexed dim, because the type @XN m@+--         does not have enough information to create a dim at runtime. typeableDim :: forall (n :: Nat) . Typeable n => Dim n {- YES, that's right. TyCon of a Nat is a string containing the Nat value.    There simply no place in a TyCon to keep the Nat as a number@@ -288,7 +360,12 @@     FixedDim ('N a)  b = a ~ b     FixedDim ('XN m) b = m <= b -instance {-# OVERLAPPABLE #-} KnownNat n => KnownDim n where+-- | This is either @Nat@, or a known @XNat@ (i.e. @N n@).+type family ExactDim (d :: k) :: Constraint where+    ExactDim (_ :: Nat)  = ()+    ExactDim (x :: XNat) = (x ~ N (DimBound x))++instance KnownNat n => KnownDim n where     {-# INLINE dim #-}     dim = DimSing (fromIntegral (natVal' (proxy# :: Proxy# n))) @@ -345,6 +422,23 @@ instance {-# OVERLAPPING #-} KnownDim 25 where   { {-# INLINE dim #-}; dim = DimSing 25 } +instance KnownDim n => KnownDim (N n) where+    {-# INLINE dim #-}+    dim = coerce (dim @n)++-- | If you have @KnownDim d@, then @d@ can only be @Nat@ or a known type of+--   @XNat@ (i.e. @N n@).+--   This function assures the type checker that this is indeed the case.+withKnownXDim :: forall (d :: XNat) (rep :: RuntimeRep) (r :: TYPE rep)+               . KnownDim d+              => ( (KnownDim (DimBound d), ExactDim d+                 , KnownDimType d, FixedDim d (DimBound d)) => r)+              -> r+withKnownXDim+  | Dict <- unsafeEqTypes @d @(N (DimBound d))+    = reifyDim @Nat @(DimBound d) (coerce (dim @d))+{-# INLINE withKnownXDim #-}+ instance Class (KnownNat n) (KnownDim n) where     cls = Sub $ reifyNat @_ @n (fromIntegral $ dimVal' @n) Dict @@ -355,9 +449,9 @@  -- | `constrainDim` with explicitly-passed constraining @Dim@ --   to avoid @AllowAmbiguousTypes@.-constrainBy :: forall (k :: Type) (x :: k) (p :: k -> Type) (l :: Type) (y :: l)+constrainBy :: forall x p y              . BoundedDim x => p x -> Dim y -> Maybe (Dim x)-constrainBy = const (constrainDim @k @x @l @y)+constrainBy = const (constrainDim @x @y) {-# INLINE constrainBy #-}  -- | Decrease minimum allowed size of a @Dim (XN x)@.@@ -374,18 +468,32 @@ sameDim :: forall (x :: Nat) (y :: Nat)          . Dim x -> Dim y -> Maybe (Dict (x ~ y)) sameDim (DimSing a) (DimSing b)-  | a == b    = Just (unsafeCoerceDict @(x ~ x) Dict)+  | a == b    = Just (unsafeEqTypes @x @y)   | otherwise = Nothing {-# INLINE sameDim #-}  -- | We either get evidence that this function --   was instantiated with the same type-level numbers, or Nothing.-sameDim' :: forall (x :: Nat) (y :: Nat) (p :: Nat -> Type) (q :: Nat -> Type)-          . (KnownDim x, KnownDim y)-         => p x -> q y -> Maybe (Dict (x ~ y))-sameDim' = const . const $ sameDim (dim @x) (dim @y)+sameDim' :: forall (x :: Nat) (y :: Nat)+          . (KnownDim x, KnownDim y) => Maybe (Dict (x ~ y))+sameDim' = sameDim (dim @x) (dim @y) {-# INLINE sameDim' #-} +-- | We either get evidence that @x@ is not greater than @y@, or Nothing.+lessOrEqDim :: forall (x :: Nat) (y :: Nat)+             . Dim x -> Dim y -> Maybe (Dict (x <= y))+lessOrEqDim a b = case compareDim a b of+  SLT -> Just Dict+  SEQ -> Just Dict+  SGT -> Nothing+{-# INLINE lessOrEqDim #-}++-- | We either get evidence that @x@ is not greater than @y@, or Nothing.+lessOrEqDim' :: forall (x :: Nat) (y :: Nat)+              . (KnownDim x, KnownDim y) => Maybe (Dict (x <= y))+lessOrEqDim' = lessOrEqDim (dim @x) (dim @y)+{-# INLINE lessOrEqDim' #-}+ -- | Ordering of dimension values. -- --   Note: `CmpNat` forces type parameters to kind `Nat`;@@ -394,73 +502,90 @@             . Dim a -> Dim b -> SOrdering (CmpNat a b) compareDim a b   = case coerce (compare :: Word -> Word -> Ordering) a b of-    LT -> unsafeCoerce# SLT-    EQ -> unsafeCoerce# SEQ-    GT -> unsafeCoerce# SGT+    LT -> unsafeCoerce SLT+    EQ -> unsafeCoerce SEQ+    GT -> unsafeCoerce SGT {-# INLINE compareDim #-}  -- | Ordering of dimension values. -- --   Note: `CmpNat` forces type parameters to kind `Nat`; --         if you want to compare unknown `XNat`s, use `Ord` instance of `Dim`.-compareDim' :: forall (a :: Nat) (b :: Nat) (p :: Nat -> Type) (q :: Nat -> Type)-             . (KnownDim a, KnownDim b) => p a -> q b -> SOrdering (CmpNat a b)-compareDim' = const . const $ compareDim (dim @a)  (dim @b)+compareDim' :: forall (a :: Nat) (b :: Nat)+             . (KnownDim a, KnownDim b) => SOrdering (CmpNat a b)+compareDim' = compareDim (dim @a)  (dim @b) {-# INLINE compareDim' #-} +-- | Same as `Prelude.(+)`.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (n + m)@. plusDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (n + m) plusDim = coerce ((+) :: Word -> Word -> Word) {-# INLINE plusDim #-} +-- | Same as `Prelude.(-)`.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (n - m)@. minusDim :: forall (n :: Nat) (m :: Nat) . (<=) m n => Dim n -> Dim m -> Dim (n - m) minusDim = coerce ((-) :: Word -> Word -> Word) {-# INLINE minusDim #-} +-- | Similar to `minusDim`, but returns @Nothing@ if the result would be negative.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (n - m)@. minusDimM :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Maybe (Dim (n - m)) minusDimM (DimSing a) (DimSing b)   | a >= b    = Just (coerce (a - b))   | otherwise = Nothing {-# INLINE minusDimM #-} +-- | Same as `Prelude.(*)`.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (n * m)@. timesDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((*) n m) timesDim = coerce ((*) :: Word -> Word -> Word) {-# INLINE timesDim #-} +-- | Same as `Prelude.(^)`.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (n ^ m)@. powerDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim ((^) n m) powerDim = coerce ((^) :: Word -> Word -> Word) {-# INLINE powerDim #-} +-- | Same as `Prelude.div`.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (Div n m)@. divDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Div n m) divDim = coerce (div :: Word -> Word -> Word) +-- | Same as `Prelude.mod`.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (Mod n m)@. modDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Mod n m) modDim = coerce (mod :: Word -> Word -> Word) +-- | Returns log base 2 (round down).+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (Log2 n)@. log2Dim :: forall (n :: Nat) . Dim n -> Dim (Log2 n) log2Dim (DimSing 0) = undefined log2Dim (DimSing x) = DimSing . fromIntegral $ finiteBitSize x - 1 - countLeadingZeros x +-- | Same as `Prelude.min`.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (Min n m)@.+minDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Min n m)+minDim = coerce (min :: Word -> Word -> Word) --- | GADT to support `KnownDimKind` type class.---   Match against its constructors to know if @k@ is @Nat@ or @XNat@-data DimKind :: Type -> Type where-    -- | Working on @Nat@.-    DimNat  :: DimKind Nat-    -- | Working on @XNat@.-    DimXNat :: DimKind XNat+-- | Same as `Prelude.max`.+--   Pattern-matching against the result would produce the evindence+--    @KnownDim (Max n m)@.+maxDim :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Dim (Max n m)+maxDim = coerce (max :: Word -> Word -> Word) --- | Figure out whether the type-level dimension is `Nat` or `XNat`.---   Useful for generalized inference functions.-class KnownDimKind (k :: Type) where-    dimKind :: DimKind k -instance KnownDimKind Nat where-    dimKind = DimNat -instance KnownDimKind XNat where-    dimKind = DimXNat-- -- | Match @Dim n@ against a concrete @Nat@ pattern D0 :: forall (n :: Nat) . () => n ~ 0 => Dim n pattern D0 <- (sameDim (D @0) -> Just Dict)@@ -592,16 +717,42 @@   where D25 = DimSing 25  +#define PLEASE_STYLISH_HASKELL \+  forall ds . KnownDimKind (KindOfEl ds) => \+  (KindOfEl ds ~ Nat, Dimensions ds) => \+  Dims ds  -- | @O(1)@ Pattern-matching against this constructor brings a `Dimensions` --   instance into the scope. --   Thus, you can do arbitrary operations on your dims and use this pattern --   at any time to reconstruct the class instance at runtime.-pattern Dims :: forall (ds :: [Nat]) . () => Dimensions ds => Dims ds-pattern Dims <- (dimsEv -> Dict)+pattern Dims :: PLEASE_STYLISH_HASKELL+pattern Dims <- (patDims (dimKind @(KindOfEl ds)) -> PatNats)   where     Dims = dims @ds+#undef PLEASE_STYLISH_HASKELL+++#define PLEASE_STYLISH_HASKELL \+  forall ds . KnownDimKind (KindOfEl ds) => \+  forall (ns :: [Nat]) . (KindOfEl ds ~ XNat, FixedDims ds ns) => \+  Dims ns -> Dims ds++-- | @O(n)@+--   Pattern-matching against this constructor reveals Nat-kinded list of dims,+--   pretending the dimensionality is known at compile time within the scope+--   of the pattern match.+--   This is the main recommended way to get `Dims` at runtime;+--   for example, reading a list of dimensions from a file.+pattern XDims :: PLEASE_STYLISH_HASKELL+pattern XDims ns <- (patDims (dimKind @(KindOfEl ds)) -> PatXNats ns)+  where+    XDims = unsafeCastTL+#undef PLEASE_STYLISH_HASKELL+ {-# COMPLETE Dims #-}+{-# COMPLETE XDims #-}+{-# COMPLETE Dims, XDims #-}  -- | @O(Length ds)@ A heavy weapon against all sorts of type errors pattern KnownDims :: forall (ds :: [Nat]) . ()@@ -613,31 +764,6 @@     KnownDims = dims @ds {-# COMPLETE KnownDims #-} --- | Pattern-matching against this constructor reveals Nat-kinded list of dims,---   pretending the dimensionality is known at compile time within the scope---   of the pattern match.---   This is the main recommended way to get `Dims` at runtime;---   for example, reading a list of dimensions from a file.------   In order to use this pattern, one must know @XNat@ type constructors in---   each dimension at compile time.-pattern XDims :: forall (xns :: [XNat]) . KnownXNatTypes xns-              => forall (ns :: [Nat]) . (FixedDims xns ns, Dimensions ns)-              => Dims ns -> Dims xns-pattern XDims ns <- (patXDims -> PatXDims ns)-  where-    XDims ns = unsafeCoerce# ns-{-# COMPLETE XDims #-}---- | An easy way to convert Nat-indexed dims into XNat-indexed dims.-pattern AsXDims :: forall (ns :: [Nat]) . ()-                => (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))-                => Dims (AsXDims ns) -> Dims ns-pattern AsXDims xns <- (patAsXDims -> PatAsXDims xns)-  where-    AsXDims xns = unsafeCoerce# xns-{-# COMPLETE AsXDims #-}- -- | Same as SomeNat, but for Dimensions: --   Hide all information about Dimensions inside data SomeDims = forall (ns :: [Nat]) . SomeDims (Dims ns)@@ -645,10 +771,11 @@ -- | Put runtime evidence of `Dims` value inside function constraints. --   Similar to `KnownDim` or `KnownNat`, but for lists of numbers. -----   Note, kind of the @Dimensions@ list is always @Nat@, restricted by+--   Note, kind of the @Dimensions@ list is usually @Nat@, restricted by --   @KnownDim@ being also @Nat@-indexed --     (it is impossible to create a unique @KnownDim (XN m)@ instance).-class Dimensions (ds :: [Nat]) where+--   Nevertheless, you can have @KnownDim (N n)@, which is useful in some cases.+class Dimensions ds where     -- | Get dimensionality of a space at runtime,     --   represented as a list of `Dim`.     --@@ -668,15 +795,51 @@     --     dims :: Dims ds -instance Dimensions '[] where++instance Dimensions ('[] :: [k]) where     dims = U     {-# INLINE dims #-} -instance (KnownDim d, Dimensions ds) => Dimensions (d ': ds) where+instance (KnownDim d, Dimensions ds) => Dimensions ((d ': ds) :: [k]) where     dims = dim :* dims     {-# INLINE dims #-} +-- | If you have @Dimensions ds@, then @ds@ can only be @[Nat]@ or a known type of+--   @[XNa]t@ (i.e. all @N n@).+--   This function assures the type checker that this is indeed the case.+withKnownXDims :: forall (ds :: [XNat]) (rep :: RuntimeRep) (r :: TYPE rep)+                . Dimensions ds+               => (( Dimensions (DimsBound ds), ExactDims ds+                   , All KnownDimType ds, FixedDims ds (DimsBound ds)) => r)+               -> r+withKnownXDims f+  | Dict <- unsafeEqTypes @ds @(Map 'N (DimsBound ds))+    = reifyDims @Nat @(DimsBound ds) dsN+        (withBareConstraint (dictToBare (inferExactFixedDims @ds dsN)) (\_ -> f) ())+  where+    dsN :: Dims (DimsBound ds)+    dsN = unsafeCastTL (dims @ds)+{-# INLINE withKnownXDims #-} +-- | Minimal or exact bound of @Dims@.+--   This is a plural form of `DimBound`.+type family DimsBound (ds :: [k]) :: [Nat] where+    DimsBound (ns :: [Nat]) = ns+    DimsBound ('[] :: [XNat]) = '[]+    DimsBound (n ': ns) = DimBound n ': DimsBound ns++-- | Every dim in a list is either @Nat@, or a known @XNat@ (i.e. @N n@).+type family ExactDims (d :: [k]) :: Constraint where+    ExactDims (_  :: [Nat])  = ()+    ExactDims (xs :: [XNat]) = xs ~ Map 'N (DimsBound xs)++-- | This is a technical "helper" family that allows to infer BoundedDims+--   constraint on a tail of a list via the superclass relation.+type family BoundedDimsTail (ds :: [k]) where+    BoundedDimsTail '[] = UnreachableConstraint (BoundedDims (Tail '[]))+                           "BoundDimsTail '[] -- BoundedDims (Tail '[])"+    BoundedDimsTail (_ ': ns) = BoundedDims ns+ -- | Get a minimal or exact bound of @Dims@. -- --   This is a plural form of `BoundedDim`.@@ -685,82 +848,105 @@ -- --    * It is defined for both @[Nat]@ and @[XNat]@; --    * Instance of @Dimensions ds@ always implies @BoundedDims ds@.-class KnownDimKind k => BoundedDims (ds :: [k]) where-    -- | Minimal or exact bound of @Dims@.-    --   This is a plural form of `DimBound`.-    type family DimsBound ds :: [Nat]+--+--   @BoundedDims@ is a powerful inference tool:+--     its instances do not require much, but it provides a lot via the superclass+--     constraints.+class ( KnownDimKind (KindOfEl ds), All BoundedDim ds, RepresentableList ds+      , Dimensions (DimsBound ds), BoundedDimsTail ds)+   => BoundedDims ds where     -- | Plural form for `dimBound`     dimsBound :: Dims (DimsBound ds)     -- | Plural form for `constrainDim`.     --     --   Given a @Dims ys@, test if its runtime value satisfies constraints imposed by-    --   @BoundedDims ds@, and returns it back coerced to @Dims ds@ on success.+    --   @BoundedDims xs@, and returns it back coerced to @Dims xs@ on success.     --     --   This function allows to guess safely individual dimension values,     --   as well as the length of the dimension list.-    --   It returns @Nothing@ if @ds@ and @xds@ have different length or if any-    --   of the values in @ys@ are less than the corresponding values of @ds@.-    constrainDims :: forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds)-    -- | BoundedDims means every element dim is @BoundedDim@ and also-    --   the length of a dim list is known.-    ---    --   Enforcing this as a superclass would complicate instance relations,-    --   so it is better to provide these dictionaries on-demand.-    inferAllBoundedDims :: Dict (All BoundedDim ds, RepresentableList ds)+    --   It returns @Nothing@ if @xs@ and @ys@ have different length or if any+    --   of the values in @ys@ are less than the corresponding values of @xs@.+    constrainDims :: forall ys . Dims ys -> Maybe (Dims ds) +-- | Minimal runtime @Dims ds@ value that satifies the constraints imposed by+--   the type signature of @Dims ds@+--   (this is the exact @dims@ for @Nat@s and the minimal bound for @XNat@s).+minimalDims :: forall ds . BoundedDims ds => Dims ds+minimalDims = unsafeCastTL (dimsBound @ds) -instance Dimensions ns => BoundedDims (ns :: [Nat]) where-    type DimsBound ns = ns-    dimsBound = dims @ns-    {-# INLINE dimsBound #-}-    constrainDims ys-      | listDims ys == listDims (dims @ns)-                  = Just (unsafeCoerce# ys)++{-# ANN defineBoundedDims ClassDict #-}+defineBoundedDims ::+       forall (k :: Type) (ds :: [k])+     . ( KnownDimKind (KindOfEl ds), All BoundedDim ds, RepresentableList ds+       , Dimensions (DimsBound ds), BoundedDimsTail ds)+    => Dims (DimsBound ds)+    -> (forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds))+    -> Dict (BoundedDims ds)+defineBoundedDims = defineBoundedDims++-- instance {-# INCOHERENT #-} Dimensions ns => BoundedDims (ns :: [k])+{-# ANN incohInstBoundedDims (ToInstance Incoherent) #-}+incohInstBoundedDims ::+       forall (k :: Type) (ds :: [k])+     . (Dimensions ds, KnownDimKind k) => Dict (BoundedDims ds)+incohInstBoundedDims+    = incohInstBoundedDims' @k @ds dims (inferAllBoundedDims ds)+  where+    ds = dims @ds++incohInstBoundedDims' ::+       forall (k :: Type) (ds :: [k])+     . KnownDimKind k+    => Dims ds+    -> Dict (All BoundedDim ds, RepresentableList ds)+    -> Dict (BoundedDims ds)+incohInstBoundedDims' ds Dict = case dimsBound' of+  Dims -> case ds of+    U   -> defineBoundedDims dimsBound' constrainDims'+    _ :* ds'+      | _ :* TypeList <- tList @ds+      , Dict <- incohInstBoundedDims' ds' Dict+        -> defineBoundedDims dimsBound' constrainDims'+    _ -> error "incohInstBoundedDims': impossible pattern"+  where+    dimsBound' :: Dims (DimsBound ds)+    dimsBound' = unsafeCastTL ds+    constrainDims' :: forall (l :: Type) (ys :: [l]) . Dims ys -> Maybe (Dims ds)+    constrainDims' ys+      | listDims ys == listDims dimsBound'+                  = Just (unsafeCastTL ys)       | otherwise = Nothing-    {-# INLINE constrainDims #-}-    inferAllBoundedDims = go (dims @ns)-      where-        go :: forall (ds :: [Nat]) . Dims ds-           -> Dict (All BoundedDim ds, RepresentableList ds)-        go  U             = Dict-        go (D :* ds)-          | Dict <- go ds = Dict +#if defined(__HADDOCK__) || defined(__HADDOCK_VERSION__)+instance Dimensions ns => BoundedDims (ns :: [Nat]) where+    dimsBound = undefined+    constrainDims = undefined+#endif++ instance BoundedDims ('[] :: [XNat]) where-    type DimsBound '[] = '[]     dimsBound = U-    constrainDims = const $ Just U-    inferAllBoundedDims = Dict+    constrainDims U        = Just U+    constrainDims (_ :* _) = Nothing  instance (BoundedDim n, BoundedDims ns) => BoundedDims ((n ': ns) :: [XNat]) where-    type DimsBound (n ': ns) = DimBound n ': DimsBound ns-    dimsBound = dimBound @XNat @n :* dimsBound @XNat @ns+    dimsBound = dimBound @n :* dimsBound @ns     constrainDims U         = Nothing     constrainDims (y :* ys) = (:*) <$> constrainDim y <*> constrainDims ys-    inferAllBoundedDims = case inferAllBoundedDims @XNat @ns of Dict -> Dict  --- | Minimal runtime @Dims ds@ value that satifies the constraints imposed by---   the type signature of @Dims ds@.-minDims :: forall (k :: Type) (ds :: [k])-         . BoundedDims ds => Dims ds-minDims = unsafeCoerce# (dimsBound @k @ds) --- -- | Construct a @Dims ds@ if there is an instance of @Typeable ds@ around. typeableDims :: forall (ds :: [Nat]) . Typeable ds => Dims ds typeableDims = case typeRep @ds of     App (App _ (tx :: TypeRep (n :: k1))) (txs :: TypeRep (ns :: k2))-      -> case unsafeCoerceDict @(Nat ~ Nat, [Nat] ~ [Nat])-                               @(Nat ~ k1 , [Nat] ~ k2) Dict of-          Dict -> case unsafeCoerceDict @(ds ~ ds)-                                        @(ds ~ (n ': ns)) Dict of-            Dict -> withTypeable tx (typeableDim @n)-                 :* withTypeable txs (typeableDims @ns)+      | Dict <- unsafeEqTypes @k1 @Nat+      , Dict <- unsafeEqTypes @k2 @[Nat]+      , Dict <- unsafeEqTypes @ds @(n ': ns)+      -> withTypeable tx (typeableDim @n) :* withTypeable txs (typeableDims @ns)     Con _-      -> unsafeCoerce# U+      -> unsafeCoerce U     r -> error ("typeableDims -- impossible typeRep: " ++ show r) {-# INLINE typeableDims #-} @@ -773,49 +959,37 @@     = Dict  --- | Convert `Dims xs` to a plain haskell list of dimension sizes @O(1)@.+-- | @O(1)@ Convert @Dims xs@ to a plain haskell list of dimension sizes. -- --   Note, for @XNat@-indexed list it returns actual content dimensions, --   not the constraint numbers (@XN m@)-listDims :: forall (k :: Type) (xs :: [k]) . Dims xs -> [Word]-listDims = unsafeCoerce#+listDims :: forall xs . Dims xs -> [Word]+listDims = unsafeCoerce {-# INLINE listDims #-}  -- | Convert a plain haskell list of dimension sizes into an unknown --   type-level dimensionality  @O(1)@. someDimsVal :: [Word] -> SomeDims-someDimsVal = SomeDims . unsafeCoerce#+someDimsVal = SomeDims . unsafeCoerce {-# INLINE someDimsVal #-}  -- | Product of all dimension sizes @O(Length xs)@.-totalDim :: forall (k :: Type) (xs :: [k]) . Dims xs -> Word+totalDim :: forall xs . Dims xs -> Word totalDim = product . listDims {-# INLINE totalDim #-}  -- | Product of all dimension sizes @O(Length xs)@.-totalDim' :: forall (xs :: [Nat]) . Dimensions xs => Word+totalDim' :: forall xs . Dimensions xs => Word totalDim' = totalDim (dims @xs) {-# INLINE totalDim' #-} --- | Get XNat-indexed dims given their fixed counterpart.-xDims :: forall (xns :: [XNat]) (ns :: [Nat])-       . FixedDims xns ns => Dims ns -> Dims xns-xDims = unsafeCoerce#-{-# INLINE xDims #-}---- | Get XNat-indexed dims given their fixed counterpart.-xDims' :: forall (xns :: [XNat]) (ns :: [Nat])-        . (FixedDims xns ns, Dimensions ns) => Dims xns-xDims' = xDims @xns (dims @ns)-{-# INLINE xDims' #-}- -- | Drop the given prefix from a Dims list. --   It returns Nothing if the list did not start with the prefix given, --    or Just the Dims after the prefix, if it does. stripPrefixDims :: forall (xs :: [Nat]) (ys :: [Nat])                  . Dims xs -> Dims ys                 -> Maybe (Dims (StripPrefix xs ys))-stripPrefixDims = unsafeCoerce# (Data.List.stripPrefix :: [Word] -> [Word] -> Maybe [Word])+stripPrefixDims = unsafeCoerce (Data.List.stripPrefix :: [Word] -> [Word] -> Maybe [Word]) {-# INLINE stripPrefixDims #-}  -- | Drop the given suffix from a Dims list.@@ -824,7 +998,7 @@ stripSuffixDims :: forall (xs :: [Nat]) (ys :: [Nat])                  . Dims xs -> Dims ys                 -> Maybe (Dims (StripSuffix xs ys))-stripSuffixDims = unsafeCoerce# stripSuf+stripSuffixDims = unsafeCoerce stripSuf   where     stripSuf :: [Word] -> [Word] -> Maybe [Word]     stripSuf suf whole = go pref whole@@ -844,7 +1018,7 @@           . Dims as -> Dims bs -> Maybe (Dict (as ~ bs)) sameDims as bs   | listDims as == listDims bs-    = Just (unsafeCoerceDict @(as ~ as) Dict)+    = Just (unsafeEqTypes @as @bs)   | otherwise = Nothing {-# INLINE sameDims #-} @@ -857,32 +1031,16 @@ {-# INLINE sameDims' #-}  --- | Similar to `const` or `asProxyTypeOf`;---   to be used on such implicit functions as `dim`, `dimMax`, etc.-inSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] -> Type) (q :: [k] -> Type)+-- | Restricted version of `const`, similar to `asProxyTypeOf`;+--   to be used on such implicit functions as `dims`, `dimsBound` etc.+inSpaceOf :: forall ds p q            . p ds -> q ds -> p ds inSpaceOf = const {-# INLINE inSpaceOf #-} --- | Similar to `asProxyTypeOf`,---   Give a hint to type checker to fix the type of a function argument.-asSpaceOf :: forall (k :: Type) (ds :: [k])-                    (p :: [k] -> Type) (q :: [k] -> Type) (r :: Type)-           . p ds -> (q ds -> r) -> (q ds -> r)-asSpaceOf = const id-{-# INLINE asSpaceOf #-}---- | Map Dims onto XDims (injective)-type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where-    AsXDims '[] = '[]-    AsXDims (n ': ns) = N n ': AsXDims ns---- | Map XDims onto Dims (injective)-type family AsDims (xns::[XNat]) = (ns :: [Nat]) | ns -> xns where-    AsDims '[] = '[]-    AsDims (N x ': xs) = x ': AsDims xs- -- | Constrain @Nat@ dimensions hidden behind @XNat@s.+--   This is a link connecting the two types of type-level dims;+--   you often need it to convert @Dims@, @Idxs@, and data. type family FixedDims (xns::[XNat]) (ns :: [Nat]) :: Constraint where     FixedDims '[] ns = (ns ~ '[])     FixedDims (xn ': xns) ns@@ -890,11 +1048,54 @@         , FixedDim xn (Head ns)         , FixedDims xns (Tail ns)) --- | Know the structure of each dimension-type KnownXNatTypes xns = All KnownXNatType xns-+-- | Try to instantiate the `FixedDims` constraint given two @Dims@ lists.+--+--   The first @Dims@ is assumed to be the output of @minimalDims@,+--   i.e. @listDims xns == toList (listDims xns)@.+--+--   If you input a list that is not equal to its type-level @DimsBound@,+--   you will just have a lower chance to get @Just Dict@ result.+inferFixedDims :: forall (xns :: [XNat]) (ns :: [Nat])+                . All KnownDimType xns+               => Dims xns -> Dims ns -> Maybe (Dict (FixedDims xns ns))+inferFixedDims U U = Just Dict+inferFixedDims (Dx (a :: Dim n) :* xns) (b :* ns)+  | Dict <- unsafeEqTypes @n @(DimBound (Head xns))+  , Just Dict <- lessOrEqDim a b+  , Just Dict <- inferFixedDims xns ns+    = Just Dict+inferFixedDims (Dn a :* xns) (b :* ns)+  | Just Dict <- sameDim a b+  , Just Dict <- inferFixedDims xns ns+    = Just Dict+inferFixedDims _ _ = Nothing +-- | A very unsafe function that bypasses all type-level checks and constructs+--   the evidence from nothing.+unsafeInferFixedDims :: forall (xns :: [XNat]) (ns :: [Nat])+                      . Dims ns -> Dict (FixedDims xns ns)+unsafeInferFixedDims U+  | Dict <- unsafeEqTypes @xns @'[] = Dict+unsafeInferFixedDims ((D :: Dim n) :* ns)+    {-+    Very unsafe operation.+    I rely here on the fact that FixedDim xn n has the same+    runtime rep as a single type equality.+    If that changes, then the code is broke.+     -}+  | Dict <- unsafeEqTypes @xns @(N n ': Tail xns)+  , Dict <- unsafeInferFixedDims @(Tail xns) ns = Dict+{-# INLINE unsafeInferFixedDims #-} +-- | Infer `FixedDims` if you know that all of dims are exact (@d ~ N n@).+--   This function is totally safe and faithful.+inferExactFixedDims :: forall (ds :: [XNat]) . ExactDims ds+                    => Dims (DimsBound ds)+                    -> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))+inferExactFixedDims U = Dict+inferExactFixedDims (_ :* ns)+  | Dict <- inferExactFixedDims @(Tail ds) ns = Dict+{-# INLINE inferExactFixedDims #-}  instance Typeable d => Data (Dim (d :: Nat)) where     gfoldl _ = id@@ -934,9 +1135,9 @@     {-# INLINE (/=) #-}  instance Eq (Dims (ds :: [XNat])) where-    (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)+    (==) = unsafeCoerce ((==) :: [Word] -> [Word] -> Bool)     {-# INLINE (==) #-}-    (/=) = unsafeCoerce# ((/=) :: [Word] -> [Word] -> Bool)+    (/=) = unsafeCoerce ((/=) :: [Word] -> [Word] -> Bool)     {-# INLINE (/=) #-}  instance Eq SomeDims where@@ -958,7 +1159,7 @@     {-# INLINE compare #-}  instance Ord (Dims (ds :: [XNat])) where-    compare = unsafeCoerce# (compare :: [Word] -> [Word] -> Ordering)+    compare = unsafeCoerce (compare :: [Word] -> [Word] -> Ordering)     {-# INLINE compare #-}  instance Ord SomeDims where@@ -970,7 +1171,7 @@     {-# INLINE showsPrec #-}  instance Show (Dims (xs :: [k])) where-    showsPrec = typedListShowsPrec @k @Dim @xs showsPrec+    showsPrec = typedListShowsPrec @Dim @xs showsPrec  instance Show SomeDims where     showsPrec p (SomeDims ds)@@ -981,22 +1182,21 @@     readPrec = Read.lexP >>= \case       Read.Ident ('D':s)         | Just d <- Read.readMaybe s-            >>= constrainDim @k @x @XNat @(XN 0) . DimSing+            >>= constrainDim @x @(XN 0) . DimSing           -> return d       _  -> Read.pfail     readList = Read.readListDefault     readListPrec = Read.readListPrecDefault  instance BoundedDims xs => Read (Dims (xs :: [k])) where-    readPrec = case inferAllBoundedDims @k @xs of-        Dict -> typedListReadPrec @k @BoundedDim ":*" Read.readPrec (tList @k @xs)+    readPrec = typedListReadPrec @BoundedDim ":*" Read.readPrec (tList @xs)     readList = Read.readListDefault     readListPrec = Read.readListPrecDefault  instance Read SomeDims where     readPrec = Read.parens . Read.prec 10 $ do       Read.lift . Read.expect $ Read.Ident "SomeDims"-      withTypedListReadPrec @Nat @Dim @SomeDims+      withTypedListReadPrec @Dim @SomeDims         (\g -> (\(Dx d) -> g d) <$> Read.readPrec @(Dim (XN 0)))         SomeDims @@ -1006,72 +1206,79 @@ --   to create an instance of `KnownDim` typeclass at runtime. --   The trick is taken from Edward Kmett's reflection library explained --   in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection-reifyDim :: forall (r :: Type) (d :: Nat) . Dim d -> (KnownDim d => r) -> r-reifyDim d k = unsafeCoerce# (MagicDim k :: MagicDim d r) d+reifyDim :: forall (k :: Type) (d :: k) (rep :: RuntimeRep) (r :: TYPE rep)+          . Dim d -> (KnownDim d => r) -> r+reifyDim d k = unsafeCoerce (MagicDim k :: MagicDim d r) d {-# INLINE reifyDim #-}-newtype MagicDim (d :: Nat) (r :: Type) = MagicDim (KnownDim d => r)+newtype MagicDim (d :: k) (r :: TYPE rep) = MagicDim (KnownDim d => r)  reifyNat :: forall (r :: Type) (d :: Nat) . Natural -> (KnownNat d => r) -> r-reifyNat d k = unsafeCoerce# (MagicNat k :: MagicNat d r) d+reifyNat d k = unsafeCoerce (MagicNat k :: MagicNat d r) d {-# INLINE reifyNat #-} newtype MagicNat (d :: Nat) (r :: Type) = MagicNat (KnownNat d => r) -dimEv :: forall (d :: Nat) . Dim d -> Dict (KnownDim d)-dimEv d = reifyDim d Dict-{-# INLINE dimEv #-}--reifyDims :: forall (r :: Type) (ds :: [Nat]) . Dims ds -> (Dimensions ds => r) -> r-reifyDims ds k = unsafeCoerce# (MagicDims k :: MagicDims ds r) ds+reifyDims :: forall (k :: Type) (ds :: [k]) (rep :: RuntimeRep) (r :: TYPE rep)+           . Dims ds -> (Dimensions ds => r) -> r+reifyDims ds k = unsafeCoerce (MagicDims k :: MagicDims ds r) ds {-# INLINE reifyDims #-}-newtype MagicDims (ds :: [Nat]) (r :: Type) = MagicDims (Dimensions ds => r)--dimsEv :: forall (ds :: [Nat]) . Dims ds -> Dict (Dimensions ds)-dimsEv ds = reifyDims ds Dict-{-# INLINE dimsEv #-}+newtype MagicDims (ds :: [k]) (r :: TYPE rep) = MagicDims (Dimensions ds => r)  -data PatXDim (xn :: XNat) where-  PatN :: KnownDim n => Dim n -> PatXDim ('N n)-  PatXN :: (KnownDim n, m <= n) => Dim n -> PatXDim ('XN m)+data PatDim (d :: k) where+  PatNat   :: KnownDim n =>          PatDim (n :: Nat)+  PatXNatN ::               Dim n -> PatDim (N n)+  PatXNatX :: (m <= n)   => Dim n -> PatDim (XN m) -dimXNEv :: forall (xn :: XNat) . XNatType xn -> Dim xn -> PatXDim xn-dimXNEv Nt (DimSing k) = reifyDim dd (PatN dd)-  where-    dd = DimSing @Nat @_ k-dimXNEv XNt xn@(DimSing k) = reifyDim dd (f dd xn)+patDim :: forall (k :: Type) (d :: k) . DimType d -> Dim d -> PatDim d+patDim DimTNat   d = reifyDim d  PatNat+patDim DimTXNatN d = PatXNatN (coerce d)+patDim DimTXNatX d = f (coerce d) d   where-    dd = DimSing @Nat @_ k-    f :: forall (d :: Nat) (m :: Nat)-       . KnownDim d => Dim d -> Dim ('XN m) -> PatXDim ('XN m)-    f d = case unsafeCoerceDict @(m <= m) @(m <= d) Dict of-      Dict -> const (PatXN d)-{-# INLINE dimXNEv #-}--data PatXDims (xns :: [XNat])-  = forall (ns :: [Nat])-  . (FixedDims xns ns, Dimensions ns) => PatXDims (Dims ns)+    f :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim (XN m) -> PatDim (XN m)+    f n = case unsafeCoerceDict @(m <= m) @(m <= n) Dict of+            Dict -> const (PatXNatX n)+{-# INLINE patDim #-} -patXDims :: forall (xns :: [XNat])-          . All KnownXNatType xns => Dims xns -> PatXDims xns-patXDims U = PatXDims U-patXDims (Dn n :* xns) = case patXDims xns of-  PatXDims ns -> PatXDims (n :* ns)-patXDims (Dx n :* xns) = case patXDims xns of-  PatXDims ns -> PatXDims (n :* ns)-{-# INLINE patXDims #-}+data PatDims (ds :: [k]) where+  PatNats  :: Dimensions ds   =>            PatDims (ds :: [Nat])+  PatXNats :: FixedDims ds ns => Dims ns -> PatDims (ds :: [XNat]) -data PatAsXDims (ns :: [Nat])-  = (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns))-  => PatAsXDims (Dims (AsXDims ns))+patDims :: forall (k :: Type) (ds :: [k]) . DimKind k -> Dims ds -> PatDims ds+patDims DimKNat  ds = reifyDims ds PatNats+patDims DimKXNat ds = withBareConstraint+    (dictToBare (unsafeInferFixedDims @ds ds')) (PatXNats ds')+  where+    ds' = unsafeCastTL ds -- convert to *some* [Nat]+{-# INLINE patDims #-} -patAsXDims :: forall (ns :: [Nat]) . Dims ns -> PatAsXDims ns-patAsXDims U = PatAsXDims U-patAsXDims (n@D :* ns) = case patAsXDims ns of-  PatAsXDims xns -> PatAsXDims (Dn n :* xns)-{-# INLINE patAsXDims #-}+{-+I know that Dimensions can be either Nats or N-known XNats.+Therefore, inside the worker function I can (un)safely pick up a BoundedDim+instance for (d ~ N n)+ -}+inferAllBoundedDims :: forall (k :: Type) (ds :: [k])+                     . (Dimensions ds, KnownDimKind k)+                    => Dims ds -> Dict (All BoundedDim ds, RepresentableList ds)+inferAllBoundedDims = go+  where+    reifyBoundedDim :: forall (d :: k) . Dim d -> Dict (BoundedDim d)+    reifyBoundedDim = case dimKind @k of+      DimKNat -> \d -> reifyDim d Dict+      DimKXNat+        | Dict <- unsafeEqTypes @d @(N (DimBound d))+              -> \d -> reifyDim (coerce d :: Dim (DimBound d)) Dict+    go :: forall (xs :: [k]) . Dims xs+       -> Dict (All BoundedDim xs, RepresentableList xs)+    go U             = Dict+    go (d :* ds)+      | Dict <- reifyBoundedDim d+      , Dict <- go ds = Dict+{-# INLINE inferAllBoundedDims #-}  data PatKDims (ns :: [Nat])-  = (All KnownDim ns, All BoundedDim ns, RepresentableList ns, Dimensions ns) => PatKDims+  = ( All KnownDim ns, All BoundedDim ns+    , RepresentableList ns, Dimensions ns)+  => PatKDims  patKDims :: forall (ns :: [Nat]) . Dims ns -> PatKDims ns patKDims U = PatKDims@@ -1081,4 +1288,7 @@  unsafeCoerceDict :: forall (a :: Constraint) (b :: Constraint)                   . Dict a -> Dict b-unsafeCoerceDict = unsafeCoerce#+unsafeCoerceDict = unsafeCoerce++unsafeCastTL :: TypedList f (xs :: [k]) -> TypedList g (ys :: [l])+unsafeCastTL = unsafeCoerce

@@ -5,9 +5,8 @@ {-# LANGUAGE TypeOperators  #-} -- This module recursively depends on Numeric.TypedList. -- I thought hs-boot is better than orphan instances.-module Numeric.Dimensions.Dim ( Dim, Nat, dimVal, minusDimM ) where-import Data.Kind      (Type)+module Numeric.Dimensions.Dim ( Dim, dimVal, minusDimM ) where import Data.Type.Lits (type (-), Nat) newtype Dim (x :: k) = DimSing Word-dimVal :: forall (k :: Type) (x :: k) . Dim (x :: k) -> Word+dimVal :: forall x . Dim x -> Word minusDimM :: forall (n :: Nat) (m :: Nat) . Dim n -> Dim m -> Maybe (Dim (n - m))

@@ -17,7 +17,12 @@ {-# LANGUAGE TypeApplications           #-} {-# LANGUAGE UnboxedTuples              #-} {-# LANGUAGE UndecidableInstances       #-}-+{-# LANGUAGE ViewPatterns               #-}+#if defined(__HADDOCK__) || defined(__HADDOCK_VERSION__)+{-# LANGUAGE StandaloneDeriving         #-}+#else+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}+#endif ----------------------------------------------------------------------------- -- | -- Module      :  Numeric.Dimensions.Idx@@ -32,86 +37,144 @@ --          is i = i1*n1*n2*...*n(k-1) + ... + i(k-2)*n1*n2 + i(k-1)*n1 + ik -- This corresponds to row-first layout of matrices and multidimenional arrays. --+-- == Type safety+--+-- Same as `Dim` and `Dims`, `Idx` and `Idxs` defined in this module incorporate+-- two different indexing mechanics.+-- Both of them can be specified with exact @Nat@ values+--   (when @d :: Nat@ or @d ~ N n@),+-- or with lower bound values (i.e. @d ~ XN m@).+-- In the former case, the @Idx@/@Idxs@ type itself guarantees that the value+-- inside is within the @Dim@/@Dims@ bounds.+-- In the latter case, @Idx@/@Idxs@ can contain any values of type @Word@.+-- In other words:+--+--   * @(d :: Nat) || (d ~ N n) =>@ using @Idx d@ to index data is always safe,+--     but creating an index using unsafe functions can yield an `OutOfDimBounds`+--     exception at runtime.+--   * @(d ~ XN m) =>@ using @Idx d@ to index data can result in an `OutOfDimBounds`+--     exception, but you can safely manipulate the index itself+--     using familiar interfaces, such as @Enum@, @Num@, etc; as if @Idx d@+--     was a plain synonym to @Word@.+-- -----------------------------------------------------------------------------  module Numeric.Dimensions.Idx   ( -- * Data types     Idx (Idx), Idxs-  , idxFromWord, unsafeIdxFromWord, idxToWord+  , idxFromWord, idxToWord   , listIdxs, idxsFromWords+  , liftIdxs, unliftIdxs, unsafeUnliftIdxs+  , TypedList ( XIdxs, U, (:*), Empty, Cons, Snoc, Reverse)+    -- * Checking the index bounds+  , OutOfDimBounds (..), outOfDimBounds, outOfDimBoundsNoCallStack+#if !defined(__HADDOCK__) && !defined(__HADDOCK_VERSION__)+  , xnatNInstEnumIdx, xnatXInstEnumIdx, incohInstEnumIdx+  , xnatNInstNumIdx, xnatXInstNumIdx, incohInstNumIdx+  , instRealIdx, instIntegralIdx+#endif   ) where   import           Data.Coerce-import           Data.Constraint  (Dict (..)) import           Data.Data        (Data) import           Foreign.Storable (Storable) import           GHC.Enum import           GHC.Generics     (Generic) import qualified Text.Read        as P+import           Unsafe.Coerce +import GHC.Exception+import GHC.Stack #ifdef UNSAFE_INDICES-import GHC.Base (Int (..), Type, Word (..), int2Word#, unsafeCoerce#, word2Int#)+import GHC.Base (Int (..), Type, Word (..), int2Word#, word2Int#) #else import GHC.Base (Int (..), Type, Word (..), int2Word#, maxInt, plusWord2#,-                 timesWord2#, unsafeCoerce#, word2Int#)+                 timesWord2#, word2Int#) #endif +#if !defined(__HADDOCK__) && !defined(__HADDOCK_VERSION__)+import Data.Constraint+import Data.Constraint.Bare+import Data.Constraint.Deriving+#endif+ import Numeric.Dimensions.Dim import Numeric.TypedList      (typedListReadPrec, typedListShowsPrec)  --- | This type is used to index a single dimension;---   the range of indices is from @0@ to @n-1@.----newtype Idx (n :: k) = Idx' Word-  deriving ( Data, Generic, Integral, Real, Storable, Eq, Ord )+{- | This type is used to index a single dimension. +  * @(k ~ Nat)  =>@ the range of indices is from @0@ to @d-1@.+  * @(d ~ N n)  =>@ the range of indices is from @0@ to @n-1@.+  * @(d ~ XN m) =>@ the range of indices is from @0@ to @maxBound :: Word@. --- | Convert between `Word` and `Idx`.------   If the word is outside of the bounds, fails with an error---     (unless @unsafeindices@ flag is turned on).----pattern Idx :: forall (k :: Type) (n :: k) . BoundedDim n => Word -> Idx n+That is, using @Idx (n :: Nat)@ or @Idx (N n)@ is guaranteed to be safe by the+type system.+But an index of type @Idx (XN m)@ can have any value, and using it may yield+an `OutOfDimBounds` exception -- just the same as a generic @index@ function that+takes a plain @Int@ or @Word@ as an argument.+Thus, if you have data indexed by @(XN m)@, I would suggest to use @lookup@-like+functions that return @Maybe@. You're warned.++ -}+newtype Idx (d :: k) = Idx' Word+  deriving ( Data, Generic, Storable, Eq, Ord )+++{- | Convert between `Word` and `Idx`.++Converting from `Idx` to `Word` is always safe.++Converting from `Word` to `Idx` generally is unsafe:++  * @(k ~ Nat)  =>@ if @w >= d@, it fails with an `OutOfDimBounds` exception.+  * @(d ~ N n)  =>@ if @w >= n@, it fails with an `OutOfDimBounds` exception.+  * @(d ~ XN m) =>@ the constructor always succeeds, but using the result for+      indexing may fail with an `OutOfDimBounds` exception later.++If @unsafeindices@ flag it turned on, this function always succeeds.+ -}+pattern Idx :: forall d . BoundedDim d => Word -> Idx d pattern Idx w <- Idx' w   where     Idx = unsafeIdxFromWord {-# COMPLETE Idx #-}  -- | Type-level dimensional indexing with arbitrary Word values inside.---   Most of the operations on it require `Dimensions` constraint,+--   Most of the operations on it require `Dimensions` or `BoundedDims` constraint, --   because the @Idxs@ itself does not store info about dimension bounds.-type Idxs (xs :: [k]) = TypedList Idx xs+type Idxs = (TypedList Idx :: [k] -> Type) --- | Convert an arbitrary Word to @Idx@.------   If the word is outside of the bounds, fails with an error---     (unless @unsafeindices@ flag is turned on).---+ unsafeIdxFromWord :: forall (k :: Type) (d :: k) . BoundedDim d => Word -> Idx d #ifdef UNSAFE_INDICES unsafeIdxFromWord = coerce #else unsafeIdxFromWord w+  | DimTXNatX <- dimType @d+              = coerce w   | w < d     = coerce w-  | otherwise = errorWithoutStackTrace-              $ "idxFromWord{" ++ showIdxType @k @d ++ "}: word "-              ++ show w ++ " is outside of index bounds."+  | otherwise = outOfDimBoundsNoCallStack "unsafeIdxFromWord" w d Nothing Nothing   where-    d = dimVal (dimBound @k @d)+    d = dimVal (dimBound @d) #endif {-# INLINE unsafeIdxFromWord #-}  -- | Convert an arbitrary Word to @Idx@.-idxFromWord :: forall (k :: Type) (d :: k) . BoundedDim d => Word -> Maybe (Idx d)+--   This is a safe alternative to the pattern @Idx@.+--+--   Note, when @(d ~ XN m)@, it returns @Nothing@ if @w >= m@.+--   Thus, the resulting index is always safe to use+--    (but you cannot index stuff beyond @DimBound d@ this way).+idxFromWord :: forall d . BoundedDim d => Word -> Maybe (Idx d) idxFromWord w-  | w < dimVal (dimBound @k @d) = Just (coerce w)-  | otherwise                   = Nothing+  | w < dimVal (dimBound @d) = Just (coerce w)+  | otherwise                = Nothing {-# INLINE idxFromWord #-}  -- | Get the value of an @Idx@.-idxToWord :: forall (k :: Type) (d :: k) . Idx d -> Word+idxToWord :: forall d . Idx d -> Word idxToWord = coerce {-# INLINE idxToWord #-} @@ -120,13 +183,18 @@   fromIntegral = idxToWord   #-} -listIdxs :: forall (k :: Type) (xs :: [k]) . Idxs xs -> [Word]-listIdxs = unsafeCoerce#+-- | /O(1)/ Convert @Idxs xs@ to a plain list of words.+listIdxs :: forall ds . Idxs ds -> [Word]+listIdxs = unsafeCoerce {-# INLINE listIdxs #-} -idxsFromWords :: forall (k :: Type) (xs :: [k])-               . BoundedDims xs => [Word] -> Maybe (Idxs xs)-idxsFromWords = unsafeCoerce# . go (listDims (dimsBound @k @xs))+-- | /O(n)/ Convert a plain list of words into an @Idxs@, while checking+--   the index bounds.+--+--   Same as with `idxFromWord`, it is always safe to use the resulting index,+--     but you cannot index stuff outside of the @DimsBound ds@ this way.+idxsFromWords :: forall ds . BoundedDims ds => [Word] -> Maybe (Idxs ds)+idxsFromWords = unsafeCoerce . go (listDims (dimsBound @ds))   where     go :: [Word] -> [Word] -> Maybe [Word]     go [] [] = Just []@@ -135,33 +203,87 @@     go _ _   = Nothing  +-- | Transform between @Nat@-indexed and @XNat@-indexed @Idxs@.+--+--   Note, this pattern is not a @COMPLETE@ match, because converting from @XNat@+--   to @Nat@ indexed @Idxs@ may fail (see `unliftIdxs`).+pattern XIdxs :: forall (ds :: [XNat]) (ns :: [Nat])+               . (FixedDims ds ns, Dimensions ns) => Idxs ns -> Idxs ds+pattern XIdxs ns <- (unliftIdxs -> Just ns)+  where+    XIdxs = liftIdxs -instance BoundedDim x => Read (Idx (x :: k)) where+-- | @O(1)@ Coerce a @Nat@-indexed list of indices into a @XNat@-indexed one.+--   This function does not need any runtime checks and thus runs in constant time.+liftIdxs :: forall (ds :: [XNat]) (ns :: [Nat])+         . FixedDims ds ns => Idxs ns -> Idxs ds+liftIdxs = unsafeCoerce+{-# INLINE liftIdxs #-}++-- | @O(n)@ Coerce a @XNat@-indexed list of indices into a @Nat@-indexed one.+--   This function checks if an index is within Dim bounds for every dimension.+unliftIdxs :: forall (ds :: [XNat]) (ns :: [Nat])+            . (FixedDims ds ns, Dimensions ns) => Idxs ds -> Maybe (Idxs ns)+unliftIdxs U = Just U+unliftIdxs (Idx' i :* is)+  | d :* Dims <- dims @ns+  , i < dimVal d = (Idx' i :*) <$> unliftIdxs is+  | otherwise    = Nothing+{-# INLINE unliftIdxs #-}++-- | Coerce a @XNat@-indexed list of indices into a @Nat@-indexed one.+--   Can throw an `OutOfDimBounds` exception unless @unsafeindices@ flag is active.+unsafeUnliftIdxs :: forall (ds :: [XNat]) (ns :: [Nat])+                  . (FixedDims ds ns, Dimensions ns) => Idxs ds -> Idxs ns+#ifdef UNSAFE_INDICES+unsafeUnliftIdxs = unsafeCoerce+#else+unsafeUnliftIdxs is' = unsafeCoerce (zipWith f is ds)+  where+    f i d | i < d     = i+          | otherwise = err i d+    is = listIdxs is'+    ds = listDims (dims @ns)+    err i d = outOfDimBoundsNoCallStack+      "unsafeUnliftIdxs" i d Nothing (Just (ds, is))+#endif+{-# INLINE unsafeUnliftIdxs #-}+++instance BoundedDim d => Read (Idx d) where     readPrec = do       w <- P.readPrec-      if w < dimVal (dimBound @k @x)-      then return (Idx' w)-      else P.pfail+      case dimType @d of+        DimTXNatX     -> return (Idx' w)+        _ | w < dimVal (dimBound @d)+                      -> return (Idx' w)+          | otherwise -> P.pfail     readList = P.readListDefault     readListPrec = P.readListPrecDefault -instance Show (Idx (x :: k)) where+instance Show (Idx d) where     showsPrec = coerce (showsPrec :: Int -> Word -> ShowS) -instance BoundedDim n => Bounded (Idx (n :: k)) where-    minBound = 0+instance BoundedDim d => Bounded (Idx d) where+    minBound = coerce (0 :: Word)     {-# INLINE minBound #-}-    maxBound = coerce (dimVal(dimBound @k @n)  - 1)+    {- | Note, @maxBound == Idx (dimVal (dimBound @d) - 1)@+            -- is defined in terms of @BoundedDim@.+         Thus, when @(d ~ XN m)@, your actual index may be larger than @maxBound@.+     -}+    maxBound = coerce (dimVal (dimBound @d) - 1)     {-# INLINE maxBound #-} -instance BoundedDim n => Enum (Idx (n :: k)) where +instance KnownDim n => Enum (Idx (n :: Nat)) where+ #ifdef UNSAFE_INDICES     succ = coerce ((+ 1) :: Word -> Word) #else     succ x@(Idx' i)       | x < maxBound = coerce (i + 1)-      | otherwise = succError $ showIdxType @k @n+      | otherwise = outOfDimBoundsNoCallStack+         "Enum.succ{Idx}" (i + 1) (dimVal' @n) Nothing Nothing #endif     {-# INLINE succ #-} @@ -170,7 +292,8 @@ #else     pred x@(Idx' i)       | x > minBound = coerce (i - 1)-      | otherwise = predError $ showIdxType @k @n+      | otherwise = outOfDimBoundsNoCallStack+         "Enum.pred{Idx}" (-1 :: Int) (dimVal' @n) Nothing Nothing #endif     {-# INLINE pred #-} @@ -179,9 +302,10 @@ #else     toEnum i         | i >= 0 && i' < d = coerce i'-        | otherwise        = toEnumError (showIdxType @k @n) i (0, d - 1)+        | otherwise        = outOfDimBoundsNoCallStack+           "Enum.toEnum{Idx}" i d Nothing Nothing       where-        d  = dimVal (dimBound @k @n)+        d  = dimVal' @n         i' = fromIntegral i #endif     {-# INLINE toEnum #-}@@ -191,19 +315,17 @@ #else     fromEnum (Idx' x@(W# w#))         | x <= maxIntWord = I# (word2Int# w#)-        | otherwise       = fromEnumError (showIdxType @k @n) x+        | otherwise       = fromEnumError "Idx" x         where           maxIntWord = W# (case maxInt of I# i -> int2Word# i) #endif     {-# INLINE fromEnum #-}--    enumFrom (Idx' n)-      = coerce (enumFromTo n (dimVal (dimBound @k @n) - 1))+    enumFrom (Idx' n) = coerce (enumFromTo n (dimVal' @n - 1))     {-# INLINE enumFrom #-}     enumFromThen (Idx' n0) (Idx' n1)       = coerce (enumFromThenTo n0 n1 lim)       where-        lim = if n1 >= n0 then dimVal (dimBound @k @n) - 1 else 0+        lim = if n1 >= n0 then maxBound else minBound     {-# INLINE enumFromThen #-}     enumFromTo       = coerce (enumFromTo :: Word -> Word -> [Word])@@ -212,22 +334,22 @@       = coerce (enumFromThenTo :: Word -> Word -> Word -> [Word])     {-# INLINE enumFromThenTo #-} -instance BoundedDim n => Num (Idx (n :: k)) where +instance KnownDim n => Num (Idx (n :: Nat)) where+ #ifdef UNSAFE_INDICES     (+) = coerce ((+) :: Word -> Word -> Word) #else-    (Idx' a@(W# a#)) + b@(Idx' (W# b#))+    (Idx' a@(W# a#)) + (Idx' b@(W# b#))         | ovf || r >= d-          = errorWithoutStackTrace-          $ "Num.(+){" ++ showIdxType @k @n ++ "}: sum of "-            ++ show a ++ " and " ++ show b-            ++ " is outside of index bounds."+          = outOfDimBoundsNoCallStack+              ("Num.(" ++ show a ++ " + " ++ show b ++ "){Idx}")+              (toInteger a + toInteger b) d Nothing Nothing         | otherwise = coerce r       where         (ovf, r) = case plusWord2# a# b# of           (# r2#, r1# #) -> ( W# r2# > 0 , W# r1# )-        d = dimVal (dimBound @k @n)+        d = dimVal' @n #endif     {-# INLINE (+) #-} @@ -236,10 +358,9 @@ #else     (Idx' a) - (Idx' b)         | b > a-          = errorWithoutStackTrace-          $ "Num.(-){" ++ showIdxType @k @n ++ "}: difference of "-            ++ show a ++ " and " ++ show b-            ++ " is negative."+          = outOfDimBoundsNoCallStack+              ("Num.(" ++ show a ++ " - " ++ show b ++ "){Idx}")+              (toInteger a - toInteger b) (dimVal' @n) Nothing Nothing         | otherwise = coerce (a - b) #endif     {-# INLINE (-) #-}@@ -247,22 +368,26 @@ #ifdef UNSAFE_INDICES     (*) = coerce ((*) :: Word -> Word -> Word) #else-    (Idx' a@(W# a#)) * b@(Idx' (W# b#))+    (Idx' a@(W# a#)) * (Idx' b@(W# b#))         | ovf || r >= d-          = errorWithoutStackTrace-          $ "Num.(*){" ++ showIdxType @k @n ++ "}: product of "-            ++ show a ++ " and " ++ show b-            ++ " is outside of index bounds."+          = outOfDimBoundsNoCallStack+              ("Num.(" ++ show a ++ " * " ++ show b ++ "){Idx}")+              (toInteger a * toInteger b) d Nothing Nothing         | otherwise = coerce r       where         (ovf, r) = case timesWord2# a# b# of           (# r2#, r1# #) -> ( W# r2# > 0 , W# r1# )-        d = dimVal (dimBound @k @n)+        d = dimVal' @n #endif     {-# INLINE (*) #-} -    negate = errorWithoutStackTrace-           $ "Num.(*){" ++ showIdxType @k @n ++ "}: cannot negate index."+#ifdef UNSAFE_INDICES+    negate = id+#else+    negate (Idx' 0) = Idx' 0+    negate (Idx' i) = outOfDimBoundsNoCallStack+        "Num.negate{Idx}" (- toInteger i) (dimVal' @n) Nothing Nothing+#endif     {-# INLINE negate #-}     abs = id     {-# INLINE abs #-}@@ -273,20 +398,128 @@     fromInteger = coerce (fromInteger :: Integer -> Word) #else     fromInteger i-      | i >= 0 && i < d = Idx' $ fromInteger i-      | otherwise       = errorWithoutStackTrace-                        $ "Num.fromInteger{" ++ showIdxType @k @n ++ "}: integer "-                        ++ show i ++ " is outside of index bounds."+      | i >= 0 && i < toInteger d+                  = Idx' (fromInteger i)+      | otherwise = outOfDimBoundsNoCallStack+          "Num.fromInteger{Idx}" i d Nothing Nothing       where-        d = toInteger $ dimVal (dimBound @k @n)+        d =  dimVal' @n #endif     {-# INLINE fromInteger #-}   +#if defined(__HADDOCK__) || defined(__HADDOCK_VERSION__) +{- |+Although @Enum (Idx d)@ requires @BoundedDim d@, it does not use @maxBound@+when @(d ~ XN m)@.+You can use list comprehensions safely for known dims+(@(k ~ Nat)@ or @(d ~ N d)@),+but you may get an index larger than your struct to be indexed when @d ~ XN m@.+ -}+deriving instance BoundedDim d => Enum (Idx d)+deriving instance BoundedDim d => Integral (Idx d)+deriving instance BoundedDim d => Real (Idx d)+{- |+Although @Num (Idx d)@ requires @BoundedDim d@, it does not use @maxBound@+when @(d ~ XN m)@.+That is, if @(d ~ XN m)@ then @i = fromIntegral n@ always succeeds.+ -}+deriving instance BoundedDim d => Num (Idx d)++#else++{-# ANN xnatNInstEnumIdx (ToInstance NoOverlap) #-}+xnatNInstEnumIdx ::+       forall (n :: Nat)+     . KnownDim n => Dict (Enum (Idx (N n)))+xnatNInstEnumIdx = unsafeCoerce (Dict @(Enum (Idx n)))++{-# ANN xnatXInstEnumIdx (ToInstance NoOverlap) #-}+xnatXInstEnumIdx ::+       forall (m :: Nat)+     . Dict (Enum (Idx (XN m)))+xnatXInstEnumIdx = unsafeCoerce (Dict @(Enum Word))++{-# ANN incohInstEnumIdx (ToInstance Incoherent) #-}+incohInstEnumIdx ::+       forall (k :: Type) (d :: k)+     . BoundedDim d => Dict (Enum (Idx d))+incohInstEnumIdx = case dimType @d of+  DimTNat   -> Dict+  DimTXNatN -> xnatNInstEnumIdx+  DimTXNatX -> xnatXInstEnumIdx++{-# ANN xnatNInstNumIdx (ToInstance NoOverlap) #-}+xnatNInstNumIdx ::+       forall (n :: Nat)+     . KnownDim n => Dict (Num (Idx (N n)))+xnatNInstNumIdx = unsafeCoerce (Dict @(Num (Idx n)))++{-# ANN xnatXInstNumIdx (ToInstance NoOverlap) #-}+xnatXInstNumIdx ::+       forall (m :: Nat)+     . Dict (Num (Idx (XN m)))+xnatXInstNumIdx = unsafeCoerce (Dict @(Num Word))++{-# ANN incohInstNumIdx (ToInstance Incoherent) #-}+incohInstNumIdx ::+       forall (k :: Type) (d :: k)+     . BoundedDim d => Dict (Num (Idx d))+incohInstNumIdx = case dimType @d of+  DimTNat   -> Dict+  DimTXNatN -> xnatNInstNumIdx+  DimTXNatX -> xnatXInstNumIdx++{-# ANN defineReal ClassDict #-}+defineReal ::+       forall a+     . (Num a, Ord a)+    => (a -> Rational) -- toRational+    -> Dict (Real a)+defineReal = defineReal++{-# ANN instRealIdx (ToInstance NoOverlap) #-}+instRealIdx ::+       forall (k :: Type) (d :: k)+     . BoundedDim d => Dict (Real (Idx d))+instRealIdx+  = withBareConstraint (dictToBare (incohInstNumIdx @k @d))+  $ defineReal (coerce (toRational @Word))++{-# ANN defineIntegral ClassDict #-}+defineIntegral ::+       forall a+     . (Real a, Enum a)+    => (a -> a -> a) -- quot+    -> (a -> a -> a) -- rem+    -> (a -> a -> a) -- div+    -> (a -> a -> a) -- mod+    -> (a -> a -> (a,a)) -- quotRem+    -> (a -> a -> (a,a)) -- divMod+    -> (a -> Integer) -- toInteger+    -> Dict (Integral a)+defineIntegral = defineIntegral++{-# ANN instIntegralIdx (ToInstance NoOverlap) #-}+instIntegralIdx ::+       forall (k :: Type) (d :: k)+     . BoundedDim d => Dict (Integral (Idx d))+instIntegralIdx+  = withBareConstraint (dictToBare (instRealIdx @k @d))+  $ withBareConstraint (dictToBare (incohInstEnumIdx @k @d))+  $ defineIntegral+    (coerce (quot @Word)) (coerce (rem @Word))+    (coerce (div @Word))  (coerce (mod @Word))+    (coerce (quotRem @Word)) (coerce (divMod @Word))+    (coerce (toInteger @Word))+++#endif+ instance Eq (Idxs (xs :: [k])) where-    (==) = unsafeCoerce# ((==) :: [Word] -> [Word] -> Bool)+    (==) = unsafeCoerce ((==) :: [Word] -> [Word] -> Bool)     {-# INLINE (==) #-}  -- | Compare indices by their importance in lexicorgaphic order@@ -303,60 +536,43 @@ --   > sort == sortOn fromEnum -- instance Ord (Idxs (xs :: [k])) where-    compare = unsafeCoerce# (compare :: [Word] -> [Word] -> Ordering)+    compare = unsafeCoerce (compare :: [Word] -> [Word] -> Ordering)     {-# INLINE compare #-}  instance Show (Idxs (xs :: [k])) where-    showsPrec = typedListShowsPrec @k @Idx @xs showsPrec+    showsPrec = typedListShowsPrec @Idx @xs showsPrec  instance BoundedDims xs => Read (Idxs (xs :: [k])) where-    readPrec = case inferAllBoundedDims @k @xs of-      Dict -> typedListReadPrec @k @BoundedDim ":*" P.readPrec (tList @k @xs)+    readPrec = typedListReadPrec @BoundedDim ":*" P.readPrec (tList @xs)     readList = P.readListDefault     readListPrec = P.readListPrecDefault --- | With this instance we can slightly reduce indexing expressions, e.g.------   > x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U)----instance BoundedDim n => Num (Idxs '[(n :: k)]) where-    (a:*U) + (b:*U) = (a+b) :* U-    {-# INLINE (+) #-}-    (a:*U) - (b:*U) = (a-b) :* U-    {-# INLINE (-) #-}-    (a:*U) * (b:*U) = (a*b) :* U-    {-# INLINE (*) #-}-    signum (a:*U)   = signum a :* U-    {-# INLINE signum #-}-    abs (a:*U)      = abs a :* U-    {-# INLINE abs #-}-    fromInteger i   = fromInteger i :* U-    {-# INLINE fromInteger #-}- instance BoundedDims ds => Bounded (Idxs (ds :: [k])) where-    maxBound = f (minDims @k @ds)+    maxBound = f (minimalDims @ds)       where         f :: forall (ns :: [k]) . Dims ns -> Idxs ns         f U         = U         f (d :* ds) = coerce (dimVal d - 1) :* f ds     {-# INLINE maxBound #-}-    minBound = f (minDims @k @ds)+    minBound = f (minimalDims @ds)       where         f :: forall (ns :: [k]) . Dims ns -> Idxs ns         f U         = U         f (_ :* ds) = Idx' 0 :* f ds     {-# INLINE minBound #-} --- @ds@ must be @[Nat]@ for @Enum (Idxs ds)@,---   because succ and pred would break otherwise-instance Dimensions ds => Enum (Idxs (ds :: [Nat])) where+{- |+@ds@ must be fixed (either @[Nat]@ or all (N n)) to know exact bounds in+each dimension.+ -}+instance Dimensions ds => Enum (Idxs ds) where      succ idx = case go dds idx of         (True , _ ) -> succError $ showIdxsType dds         (False, i') -> i'       where         dds = dims @ds-        go :: forall (ns :: [Nat]) . Dims ns -> Idxs ns -> (Bool, Idxs ns)+        go :: forall ns . Dims ns -> Idxs ns -> (Bool, Idxs ns)         go U U = (True, U)         go (d :* ds) (Idx' i :* is) = case go ds is of           (True , is')@@ -370,7 +586,7 @@         (False, i') -> i'       where         dds = dims @ds-        go :: forall (ns :: [Nat]) . Dims ns -> Idxs ns -> (Bool, Idxs ns)+        go :: forall ns . Dims ns -> Idxs ns -> (Bool, Idxs ns)         go U U = (True, U)         go (d :* ds) (Idx' i :* is) = case go ds is of           (True , is')@@ -384,7 +600,7 @@         _      -> toEnumError (showIdxsType dds) off0 (0, totalDim dds - 1)       where         dds = dims @ds-        go :: forall (ns :: [Nat]) . Dims ns -> (Word, Idxs ns)+        go :: forall ns . Dims ns -> (Word, Idxs ns)         go  U = (fromIntegral off0, U)         go (d :* ds)           | (off , is) <- go ds@@ -400,7 +616,7 @@         f (d, i) (td, off) = (d * td, off + td * i)     {-# INLINE fromEnum #-} -    enumFrom = unsafeCoerce# go True (dims @ds)+    enumFrom = unsafeCoerce go True (dims @ds)       where         go :: Bool -> [Word] -> [Word] -> [[Word]]         go b (d:ds) (i:is) =@@ -410,7 +626,7 @@         go _ _ _  = [[]]     {-# INLINE enumFrom #-} -    enumFromTo = unsafeCoerce# go True True (dims @ds)+    enumFromTo = unsafeCoerce go True True (dims @ds)       where         go :: Bool -> Bool -> [Word] -> [Word] -> [Word] -> [[Word]]         go bl bu (d:ds) (x:xs) (y:ys) =@@ -428,9 +644,17 @@     {-# INLINE enumFromTo #-}      enumFromThen x0 x1 = case compare x1 x0 of-      EQ -> repeat x0-      GT -> enumFromThenTo x0 x1 maxBound-      LT -> enumFromThenTo x0 x1 minBound+        EQ -> repeat x0+        GT -> enumFromThenTo x0 x1 $ maxB ds+        LT -> enumFromThenTo x0 x1 $ minB ds+      where+        ds = dims @ds+        maxB :: forall ns . Dims ns -> Idxs ns+        maxB U         = U+        maxB (x :* xs) = coerce (dimVal x - 1) :* maxB xs+        minB :: forall ns . Dims ns -> Idxs ns+        minB U         = U+        minB (_ :* xs) = Idx' 0 :* minB xs     {-# INLINE enumFromThen #-}      enumFromThenTo x0 x1 y = case dir of@@ -442,7 +666,7 @@                         (0, is') -> repeatStep is'                         _        -> []                       else []-              in unsafeCoerce# (repeatStep allX0s)+              in unsafeCoerce (repeatStep allX0s)         LT -> let (_, allDXs) = idxMinus allDs allX1s allX0s                   repeatStep is                     = if is >= allYs@@ -450,7 +674,7 @@                         (0, is') -> repeatStep is'                         _        -> []                       else []-              in unsafeCoerce# (repeatStep allX0s)+              in unsafeCoerce (repeatStep allX0s)       where         allDs  = listDims $ dims @ds         allX0s = listIdxs x0@@ -473,11 +697,121 @@     {-# INLINE enumFromThenTo #-}  ---- | Show type of Idx (for displaying nice errors).-showIdxType :: forall (k :: Type) (x :: k) . BoundedDim x => String-showIdxType = "Idx " ++ show (dimVal (dimBound @k @x))- -- | Show type of Idxs (for displaying nice errors). showIdxsType :: Dims ns -> String showIdxsType ds = "Idxs '" ++ show (listDims ds)++-- | Throw an `OutOfDimBounds` exception without the CallStack attached.+outOfDimBoundsNoCallStack ::+       Integral i+    => String  -- ^ Label (e.g. function name)+    -> i       -- ^ Bad index+    -> Word    -- ^ Target dim+    -> Maybe Word -- ^ SubSpace Dim, if applicable.+    -> Maybe ([Word], [Word]) -- ^ Larger picture: Dims and Idxs+    -> a+outOfDimBoundsNoCallStack s i d msubd dimsCtx+  = throw OutOfDimBounds+  { oodIdx       = toInteger i+  , oodDim       = d+  , oodSubDim    = msubd+  , oodDimsCtx   = dimsCtx+  , oodName      = s+  , oodCallStack = Nothing+  }++-- | Throw an `OutOfDimBounds` exception.+outOfDimBounds ::+       (HasCallStack, Integral i)+    => String  -- ^ Label (e.g. function name)+    -> i       -- ^ Bad index+    -> Word    -- ^ Target dim+    -> Maybe Word -- ^ SubSpace Dim, if applicable.+    -> Maybe ([Word], [Word]) -- ^ Larger picture: Dims and Idxs+    -> a+outOfDimBounds s i d msubd dimsCtx+  = throw OutOfDimBounds+  { oodIdx       = toInteger i+  , oodDim       = d+  , oodSubDim    = msubd+  , oodDimsCtx   = dimsCtx+  , oodName      = s+  , oodCallStack = Just callStack+  }++{- |+Typically, this exception can occur in the following cases:++  * Converting from integral values to @Idx d@ when @d ~ N n@ or @d :: Nat@.+  * Using @Enum@ and @Num@ when @d ~ N n@ or @d :: Nat@.+  * Converting from @Idx (XN m :: XNat)@ to @Idx (n :: Nat)@.+  * Indexing or slicing data using  @Idx (XN m :: XNat)@.++If you are mad and want to avoid any overhead related to bounds checking and the+related error handling, you can turn on the @unsafeindices@ flag to remove all of+this from the library at once.+ -}+data OutOfDimBounds+  = OutOfDimBounds+  { oodIdx       :: Integer+    -- ^ A value that should have been a valid `Idx`+  , oodDim       :: Word+    -- ^ A runtime value of a `Dim`+  , oodSubDim    :: Maybe Word+    -- ^ When used for slicing, this should have satisfied+    --   @oodIdx + oodSubDim <= oodDim@.+  , oodDimsCtx   :: Maybe ([Word], [Word])+    -- ^ If available, contains (Dims xns, Idxs xns).+  , oodName      :: String+    -- ^ Short description of the error location, typically a function name.+  , oodCallStack :: Maybe CallStack+    -- ^ Function call stack, if available.+    --   Note, this field is ignored in the `Eq` and `Ord` instances.+  }++-- | Note, this instance ignores `oodCallStack`+instance Eq OutOfDimBounds where+  (==) a b = and+    [ (==) (oodIdx a) (oodIdx b)+    , (==) (oodDim a) (oodDim b)+    , (==) (oodSubDim a) (oodSubDim b)+    , (==) (oodDimsCtx a) (oodDimsCtx b)+    , (==) (oodName a) (oodName b)+    ]++-- | Note, this instance ignores `oodCallStack`+instance Ord OutOfDimBounds where+  compare a b = mconcat+    [ compare (oodIdx a) (oodIdx b)+    , compare (oodDim a) (oodDim b)+    , compare (oodSubDim a) (oodSubDim b)+    , compare (oodDimsCtx a) (oodDimsCtx b)+    , compare (oodName a) (oodName b)+    ]++instance Show OutOfDimBounds where+  showsPrec p e = addLoc errStr+    where+      addLoc s+        = let someE = case oodCallStack e of+                Nothing -> errorCallException s+                Just st -> errorCallWithCallStackException s st+              errc :: ErrorCall+              errc = case fromException someE of+                Nothing -> ErrorCall s+                Just ec -> ec+          in  showsPrec p errc+      errStr = oodName e ++ ": " ++ errContent ++ errCtx+      errContent = case oodSubDim e of+        Nothing -> "index " ++ show (oodIdx e) +++                   " is outside of Dim bounds (0 <= i < " ++ show (oodDim e) ++ ")"+        Just sd -> "index " ++ show (oodIdx e) +++                   " and subspace dim " ++ show sd +++                   " together exceed the original space dim " ++ show (oodDim e)+      errCtx = case oodDimsCtx e of+        Nothing -> "."+        Just (ds, is)+            -> ";\n  dims: " ++ (case someDimsVal ds of SomeDims x -> show x)+            ++  "\n  idxs: " ++ show (unsafeCoerce is :: Idxs ns)++instance Exception OutOfDimBounds

@@ -16,6 +16,8 @@ import           Numeric.Tuple.Strict as TS import           Unsafe.Coerce        (unsafeCoerce) +-- | /O(n)/ Convert a lazy @Tuple@ to a strict @Tuple@, forcing all its values+--   to the WHNF along the way. toStrict :: TL.Tuple xs -> TS.Tuple xs toStrict U = U toStrict (TL.Id x :* xs)@@ -23,6 +25,7 @@         !ys = toStrict xs     in y :* ys +-- | /O(n)/ Convert a strict @Tuple@ to a lazy @Tuple@ by means of a simple coercion. fromStrict :: TS.Tuple xs -> TL.Tuple xs fromStrict = unsafeCoerce {-# INLINE fromStrict #-}

@@ -49,10 +49,10 @@ import           Data.Semigroup       as Sem (Semigroup (..)) import           Data.String          (IsString) import           Foreign.Storable     (Storable)-import           GHC.Base             (Type)-import           GHC.Exts+import           GHC.Base             (Type, Any) import           GHC.Generics         (Generic, Generic1) import qualified Text.Read            as P+import           Unsafe.Coerce        (unsafeCoerce)  import Data.Type.List import Numeric.TypedList@@ -126,7 +126,7 @@   -- | A tuple indexed by a list of types-type Tuple (xs :: [Type]) = TypedList Id xs+type Tuple = (TypedList Id :: [Type] -> Type)  {-# COMPLETE U, (:$) #-} {-# COMPLETE U, (:!) #-}@@ -157,32 +157,32 @@  -- | Grow a tuple on the left O(1). (*$) :: x -> Tuple xs -> Tuple (x :+ xs)-(*$) x xs = unsafeCoerce# (unsafeCoerce# x : unsafeCoerce# xs :: [Any])+(*$) x xs = unsafeCoerce (unsafeCoerce x : unsafeCoerce xs :: [Any]) {-# INLINE (*$) #-} infixr 5 *$  -- | Grow a tuple on the left while evaluating arguments to WHNF O(1). (*!) :: x -> Tuple xs -> Tuple (x :+ xs)-(*!) !x !xs = let !r = unsafeCoerce# x : unsafeCoerce# xs :: [Any]-              in unsafeCoerce# r+(*!) !x !xs = let !r = unsafeCoerce x : unsafeCoerce xs :: [Any]+              in unsafeCoerce r {-# INLINE (*!) #-} infixr 5 *!  -- | Grow a tuple on the right. --   Note, it traverses an element list inside O(n). ($*) :: Tuple xs -> x -> Tuple (xs +: x)-($*) xs x = unsafeCoerce# (unsafeCoerce# xs ++ [unsafeCoerce# x] :: [Any])+($*) xs x = unsafeCoerce (unsafeCoerce xs ++ [unsafeCoerce x] :: [Any]) {-# INLINE ($*) #-} infixl 5 $*  -- | Grow a tuple on the right while evaluating arguments to WHNF. --   Note, it traverses an element list inside O(n). (!*) :: Tuple xs -> x -> Tuple (xs +: x)-(!*) !xs !x = let !r = go (unsafeCoerce# x) (unsafeCoerce# xs) :: [Any]+(!*) !xs !x = let !r = go (unsafeCoerce x) (unsafeCoerce xs) :: [Any]                   go :: Any -> [Any] -> [Any]                   go z []       = z `seq` [z]                   go z (y : ys) = y `seq` y : go z ys-              in unsafeCoerce# r+              in unsafeCoerce r {-# INLINE (!*) #-} infixl 5 !* @@ -194,7 +194,7 @@ instance ( RepresentableList xs          , All Semigroup xs          , All Monoid xs) => Mon.Monoid (Tuple xs) where-    mempty = go (tList @Type @xs)+    mempty = go (tList @xs)       where         go :: forall (ys :: [Type])             . All Monoid ys => TypeList ys -> Tuple ys@@ -206,13 +206,13 @@   instance (RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) where-    minBound = go (tList @Type @xs)+    minBound = go (tList @xs)       where         go :: forall (ys :: [Type])             . All Bounded ys => TypeList ys -> Tuple ys         go U         = U         go (_ :* xs) = minBound *$ go xs-    maxBound = go (tList @Type @xs)+    maxBound = go (tList @xs)       where         go :: forall (ys :: [Type])             . All Bounded ys => TypeList ys -> Tuple ys@@ -231,10 +231,10 @@     compare (x :* tx) (y :* ty) = compare1 x y <> compare tx ty  instance All Show xs => Show (Tuple xs) where-   showsPrec = typedListShowsPrecC @Type @Show ":$" showsPrec1+   showsPrec = typedListShowsPrecC @Show ":$" showsPrec1  instance (All Read xs, RepresentableList xs) => Read (Tuple xs) where-   readPrec = typedListReadPrec @Type @Read ":$" readPrec1 (tList @Type @xs)+   readPrec = typedListReadPrec @Read ":$" readPrec1 (tList @xs)    readList = P.readListDefault    readListPrec = P.readListPrecDefault 

@@ -49,10 +49,10 @@ import           Data.Semigroup       as Sem (Semigroup (..)) import           Data.String          (IsString) import           Foreign.Storable     (Storable)-import           GHC.Base             (Type)-import           GHC.Exts+import           GHC.Base             (Type, Any) import           GHC.Generics         (Generic, Generic1) import qualified Text.Read            as P+import           Unsafe.Coerce        (unsafeCoerce)  import Data.Type.List import Numeric.TypedList@@ -126,7 +126,7 @@   -- | A tuple indexed by a list of types-type Tuple (xs :: [Type]) = TypedList Id xs+type Tuple = (TypedList Id :: [Type] -> Type)  {-# COMPLETE U, (:$) #-} {-# COMPLETE U, (:!) #-}@@ -157,32 +157,32 @@  -- | Grow a tuple on the left O(1). (*$) :: x -> Tuple xs -> Tuple (x :+ xs)-(*$) x xs = unsafeCoerce# (unsafeCoerce# x : unsafeCoerce# xs :: [Any])+(*$) x xs = unsafeCoerce (unsafeCoerce x : unsafeCoerce xs :: [Any]) {-# INLINE (*$) #-} infixr 5 *$  -- | Grow a tuple on the left while evaluating arguments to WHNF O(1). (*!) :: x -> Tuple xs -> Tuple (x :+ xs)-(*!) !x !xs = let !r = unsafeCoerce# x : unsafeCoerce# xs :: [Any]-              in unsafeCoerce# r+(*!) !x !xs = let !r = unsafeCoerce x : unsafeCoerce xs :: [Any]+              in unsafeCoerce r {-# INLINE (*!) #-} infixr 5 *!  -- | Grow a tuple on the right. --   Note, it traverses an element list inside O(n). ($*) :: Tuple xs -> x -> Tuple (xs +: x)-($*) xs x = unsafeCoerce# (unsafeCoerce# xs ++ [unsafeCoerce# x] :: [Any])+($*) xs x = unsafeCoerce (unsafeCoerce xs ++ [unsafeCoerce x] :: [Any]) {-# INLINE ($*) #-} infixl 5 $*  -- | Grow a tuple on the right while evaluating arguments to WHNF. --   Note, it traverses an element list inside O(n). (!*) :: Tuple xs -> x -> Tuple (xs +: x)-(!*) !xs !x = let !r = go (unsafeCoerce# x) (unsafeCoerce# xs) :: [Any]+(!*) !xs !x = let !r = go (unsafeCoerce x) (unsafeCoerce xs) :: [Any]                   go :: Any -> [Any] -> [Any]                   go z []       = z `seq` [z]                   go z (y : ys) = y `seq` y : go z ys-              in unsafeCoerce# r+              in unsafeCoerce r {-# INLINE (!*) #-} infixl 5 !* @@ -194,7 +194,7 @@ instance ( RepresentableList xs          , All Semigroup xs          , All Monoid xs) => Mon.Monoid (Tuple xs) where-    mempty = go (tList @Type @xs)+    mempty = go (tList @xs)       where         go :: forall (ys :: [Type])             . All Monoid ys => TypeList ys -> Tuple ys@@ -206,13 +206,13 @@   instance (RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) where-    minBound = go (tList @Type @xs)+    minBound = go (tList @xs)       where         go :: forall (ys :: [Type])             . All Bounded ys => TypeList ys -> Tuple ys         go U         = U         go (_ :* xs) = minBound *! go xs-    maxBound = go (tList @Type @xs)+    maxBound = go (tList @xs)       where         go :: forall (ys :: [Type])             . All Bounded ys => TypeList ys -> Tuple ys@@ -231,10 +231,10 @@     compare (x :* tx) (y :* ty) = compare1 x y <> compare tx ty  instance All Show xs => Show (Tuple xs) where-   showsPrec = typedListShowsPrecC @Type @Show ":!" showsPrec1+   showsPrec = typedListShowsPrecC @Show ":!" showsPrec1  instance (All Read xs, RepresentableList xs) => Read (Tuple xs) where-   readPrec = typedListReadPrec @Type @Read ":!" readPrec1 (tList @Type @xs)+   readPrec = typedListReadPrec @Read ":!" readPrec1 (tList @xs)    readList = P.readListDefault    readListPrec = P.readListPrecDefault 

@@ -38,7 +38,7 @@     ( TypedList (U, (:*), Empty, TypeList, EvList, Cons, Snoc, Reverse)     , RepresentableList (..)     , Dict1 (..), DictList-    , TypeList, types, typeables,inferTypeableList+    , TypeList, types, typeables, inferTypeableList     , order, order'     , cons, snoc     , Numeric.TypedList.reverse@@ -65,6 +65,8 @@ import           Data.Constraint                 hiding ((***)) import           Data.Data import           Data.Type.List+import           Data.Type.List.Internal+import           Data.Type.Lits import           Data.Void import           GHC.Base                        (Type) import           GHC.Exts@@ -73,8 +75,9 @@ import qualified Text.Read                       as Read import qualified Text.Read.Lex                   as Read import qualified Type.Reflection                 as R+import           Unsafe.Coerce                   (unsafeCoerce) -import {-# SOURCE #-} Numeric.Dimensions.Dim (Dim, Nat, dimVal, minusDimM)+import {-# SOURCE #-} Numeric.Dimensions.Dim (Dim, dimVal, minusDimM)  -- | Type-indexed list newtype TypedList (f :: (k -> Type)) (xs :: [k]) = TypedList [Any]@@ -96,11 +99,11 @@ instance (Typeable k, Typeable f, Typeable xs, All Data (Map f xs))       => Data (TypedList (f :: (k -> Type)) (xs :: [k])) where     gfoldl _ z U         = z U-    gfoldl k z (x :* xs) = case inferTypeableCons @_ @xs of+    gfoldl k z (x :* xs) = case inferTypeableCons @xs of       Dict -> z (:*) `k` x `k` xs-    gunfold k z _ = case typeables @k @xs of+    gunfold k z _ = case typeables @xs of         U      -> z U-        _ :* _ -> case inferTypeableCons @_ @xs of Dict -> k (k (z (:*)))+        _ :* _ -> case inferTypeableCons @xs of Dict -> k (k (z (:*)))     toConstr U        = typedListConstrEmpty     toConstr (_ :* _) = typedListConstrCons     dataTypeOf _ = typedListDataType@@ -121,12 +124,16 @@     TypedListRepNil (_ ': _) = Rec0 Void  type family TypedListRepCons (f :: (k -> Type)) (xs :: [k]) :: (Type -> Type) where-    TypedListRepCons _ '[]       = Rec0 Void-    TypedListRepCons f (x ': xs) = C1 ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)-      ( S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)+    TypedListRepCons _ '[]+      = Rec0 Void+    TypedListRepCons f (x ': xs)+      = C1 ('MetaCons ":*" ('InfixI 'RightAssociative 5) 'False)+      ( S1 ('MetaSel 'Nothing 'NoSourceUnpackedness+                     'NoSourceStrictness 'DecidedLazy)            (Rec0 (f x))        :*:-        S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)+        S1 ('MetaSel 'Nothing 'NoSourceUnpackedness+                     'NoSourceStrictness 'DecidedLazy)            (Rec0 (TypedList f xs))       ) @@ -137,13 +144,13 @@     from U         = M1 (L1 (M1 U1))     from (x :* xs) = M1 (R1 (M1 (M1 (K1 x) :*: M1 (K1 xs))))     to (M1 (L1 _))-      | Dict <- unsafeEqTypes @[k] @xs @'[] = U+      | Dict <- unsafeEqTypes @xs @'[] = U     to (M1 (R1 xxs))-      | Dict <- unsafeEqTypes @[k] @xs @(Head xs ': Tail xs)+      | Dict <- unsafeEqTypes @xs @(Head xs ': Tail xs)       , M1 (M1 (K1 x) :*: M1 (K1 xs)) <- xxs = x :* xs  -- | A list of type proxies-type TypeList (xs :: [k]) = TypedList Proxy xs+type TypeList = (TypedList Proxy :: [k] -> Type)  -- | Same as `Dict`, but allows to separate constraint function from --   the type it is applied to.@@ -170,26 +177,25 @@   -- | A list of dicts for the same constraint over several types.-type DictList (c :: k -> Constraint) (xs :: [k])-  = TypedList (Dict1 c) xs+type DictList (c :: k -> Constraint)+  = (TypedList (Dict1 c) :: [k] -> Type)   -- | Pattern matching against this causes `RepresentableList` instance --   come into scope. --   Also it allows constructing a term-level list out of a constraint.-pattern TypeList :: forall (k :: Type) (xs :: [k])-                  . () => RepresentableList xs => TypeList xs+pattern TypeList :: forall xs . () => RepresentableList xs => TypeList xs pattern TypeList <- (mkRTL -> Dict)   where-    TypeList = tList @k @xs+    TypeList = tList @xs  -- | Pattern matching against this allows manipulating lists of constraints. --   Useful when creating functions that change the shape of dimensions.-pattern EvList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k])+pattern EvList :: forall c xs                 . () => (All c xs, RepresentableList xs) => DictList c xs pattern EvList <- (mkEVL -> Dict)   where-    EvList = _evList (tList @k @xs)+    EvList = _evList (tList @xs)  -- | Zero-length type list pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k])@@ -204,116 +210,142 @@ pattern Empty = U  -- | Constructing a type-indexed list-pattern (:*) :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+pattern (:*) :: forall f xs               . ()-             => forall (y :: k) (ys :: [k])+             => forall y ys               . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs pattern (:*) x xs = Cons x xs infixr 5 :*  -- | Constructing a type-indexed list in the canonical way-pattern Cons :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+pattern Cons :: forall f xs               . ()-             => forall (y :: k) (ys :: [k])+             => forall y ys               . (xs ~ (y ': ys)) => f y -> TypedList f ys -> TypedList f xs-pattern Cons x xs <- (patTL @k @f @xs -> PatCons x xs)+pattern Cons x xs <- (patTL @_ @f @xs -> PatCons x xs)   where     Cons = Numeric.TypedList.cons  -- | Constructing a type-indexed list from the other end-pattern Snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k])-              . ()-             => forall (sy :: [k]) (y :: k)-              . (xs ~ (sy +: y)) => TypedList f sy -> f y -> TypedList f xs-pattern Snoc sx x <- (unsnocTL @k @f @xs -> PatSnoc sx x)+pattern Snoc :: forall f xs . ()+             => forall sy y . SnocList sy y xs+             => TypedList f sy -> f y -> TypedList f xs+pattern Snoc sx x <- (unsnocTL @_ @f @xs -> PatSnoc sx x)   where     Snoc = Numeric.TypedList.snoc  -- | Reverse a typed list-pattern Reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k])-                 . ()-                => forall (sx :: [k])-                 . (xs ~ Reverse sx, sx ~ Reverse xs)+pattern Reverse :: forall f xs . ()+                => forall sx . ReverseList xs sx                 => TypedList f sx -> TypedList f xs-pattern Reverse sx <- (unreverseTL @k @f @xs -> PatReverse sx)+pattern Reverse sx <- (unreverseTL @_ @f @xs -> PatReverse sx)   where     Reverse = Numeric.TypedList.reverse -cons :: forall (k :: Type) (f :: k -> Type) (x :: k) (xs :: [k])+-- | /O(1)/ append an element in front of a @TypedList@ (same as `(:)` for lists).+cons :: forall f x xs       . f x -> TypedList f xs -> TypedList f (x :+ xs)-cons x xs = TypedList (unsafeCoerce# x : coerce xs)+cons x xs = TypedList (unsafeCoerce x : coerce xs) {-# INLINE cons #-} -snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (x :: k)+-- | /O(n)/ append an element to the end of a @TypedList@.+snoc :: forall f xs x       . TypedList f xs -> f x -> TypedList f (xs +: x)-snoc xs x = TypedList (coerce xs ++ [unsafeCoerce# x])+snoc xs x = TypedList (coerce xs ++ [unsafeCoerce x]) {-# INLINE snoc #-} -reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+-- | /O(n)/ return elements of a @TypedList@ in reverse order.+reverse :: forall f xs          . TypedList f xs -> TypedList f (Reverse xs) reverse = coerce (Prelude.reverse :: [Any] -> [Any]) {-# INLINE reverse #-} -head :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+-- | /O(1)/ Extract the first element of a @TypedList@, which must be non-empty.+head :: forall f xs       . TypedList f xs -> f (Head xs)-head (TypedList xs) = unsafeCoerce# (Prelude.head xs)+head (TypedList xs) = unsafeCoerce (Prelude.head xs) {-# INLINE head #-} -tail :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+-- | /O(1)/ Extract the elements after the head of a @TypedList@,+--   which must be non-empty.+tail :: forall f xs       . TypedList f xs -> TypedList f (Tail xs) tail = coerce (Prelude.tail :: [Any] -> [Any]) {-# INLINE tail #-} -init :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+-- | /O(n)/ Return all the elements of a @TypedList@ except the last one+--   (the list must be non-empty).+init :: forall f xs       . TypedList f xs -> TypedList f (Init xs) init = coerce (Prelude.init :: [Any] -> [Any]) {-# INLINE init #-} -last :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+-- | /O(n)/ Extract the last element of a @TypedList@, which must be non-empty.+last :: forall f xs       . TypedList f xs -> f (Last xs)-last (TypedList xs) = unsafeCoerce# (Prelude.last xs)+last (TypedList xs) = unsafeCoerce (Prelude.last xs) {-# INLINE last #-} -take :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k])+-- | /O(min(n,k))/ @take k xs@ returns a prefix of @xs@ of length @min(length xs, k)@.+--   It calls `Prelude.take` under the hood, so expect the same behavior.+take :: forall (n :: Nat) f xs       . Dim n -> TypedList f xs -> TypedList f (Take n xs) take = coerce (Prelude.take . dimValInt :: Dim n -> [Any] -> [Any]) {-# INLINE take #-} -drop :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k])+-- | /O(min(n,k))/ @drop k xs@ returns a suffix of @xs@ of length @max(0, length xs - k)@.+--   It calls `Prelude.drop` under the hood, so expect the same behavior.+drop :: forall (n :: Nat) f xs       . Dim n -> TypedList f xs -> TypedList f (Drop n xs) drop = coerce (Prelude.drop . dimValInt :: Dim n -> [Any] -> [Any]) {-# INLINE drop #-} -length :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+-- | Return the number of elements in a @TypedList@ (same as `order`).+length :: forall f xs        . TypedList f xs -> Dim (Length xs) length = order {-# INLINE length #-} -splitAt :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k])++-- | /O(min(n,k))/ @splitAt k xs@ has the same effect as @('take' k xs, 'drop' k xs)@.+--   It calls `Prelude.splitAt` under the hood, so expect the same behavior.+splitAt :: forall (n :: Nat) f xs          . Dim n         -> TypedList f xs         -> (TypedList f (Take n xs), TypedList f (Drop n xs)) splitAt = coerce (Prelude.splitAt . dimValInt :: Dim n -> [Any] -> ([Any], [Any])) {-# INLINE splitAt #-} -order' :: forall (k :: Type) (xs :: [k])-        . RepresentableList xs => Dim (Length xs)-order' = order (tList @_ @xs)++-- | Return the number of elements in a type list @xs@ bound by a constraint+--   @RepresentableList xs@ (same as `order`, but takes no value arguments).+order' :: forall xs . RepresentableList xs => Dim (Length xs)+order' = order (tList @xs) {-# INLINE order' #-} -order :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+-- | Return the number of elements in a @TypedList@ (same as `length`).+order :: forall f xs        . TypedList f xs -> Dim (Length xs)-order = unsafeCoerce# (fromIntegral . Prelude.length :: [Any] -> Word)+order = unsafeCoerce (fromIntegral . Prelude.length :: [Any] -> Word) {-# INLINE order #-} -concat :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k])+-- | Concat two @TypedList@s.+--   It calls `Prelude.(++)` under the hood, so expect the same behavior.+concat :: forall f xs ys         . TypedList f xs        -> TypedList f ys        -> TypedList f (xs ++ ys) concat = coerce ((++) :: [Any] -> [Any] -> [Any]) {-# INLINE concat #-} -stripPrefix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k])+-- | Drops the given prefix from a @TypedList@.+--   It returns 'Nothing' if the @TypedList@ does not start with the prefix+--   given, or 'Just' the @TypedList@ after the prefix, if it does.+--   It calls `Prelude.stripPrefix` under the hood, so expect the same behavior.+--+--   This function can be used to find the type-level evidence that one type-level+--   list is indeed a prefix of another.+stripPrefix :: forall f xs ys              . ( All Typeable xs, All Typeable ys, All Eq (Map f xs))             => TypedList f xs             -> TypedList f ys@@ -326,7 +358,13 @@   | otherwise    = Nothing {-# INLINE stripPrefix #-} -stripSuffix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k])+-- | Drops the given suffix from a @TypedList@.+--   It returns 'Nothing' if the @TypedList@ does not end with the suffix+--   given, or 'Just' the @TypedList@ before the suffix, if it does.+--+--   This function can be used to find the type-level evidence that one type-level+--   list is indeed a suffix of another.+stripSuffix :: forall f xs ys              . ( All Typeable xs, All Typeable ys, All Eq (Map f xs))             => TypedList f xs             -> TypedList f ys@@ -344,7 +382,7 @@  -- | Returns two things at once: --   (Evidence that types of lists match, value-level equality).-sameList :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k])+sameList :: forall f xs ys           . ( All Typeable xs, All Typeable ys, All Eq (Map f xs))          => TypedList f xs          -> TypedList f ys@@ -359,14 +397,14 @@ sameList _ _ = Nothing  -- | Map a function over contents of a typed list-map :: forall (k :: Type) (f :: k -> Type) (g :: k -> Type) (xs :: [k])-     . (forall (a :: k) . f a -> g a)+map :: forall f g xs+     . (forall a . f a -> g a)     -> TypedList f xs     -> TypedList g xs map k = coerce (Prelude.map k')   where     k' :: Any -> Any-    k' = unsafeCoerce# . k . unsafeCoerce#+    k' = unsafeCoerce k {-# INLINE map #-}  -- | Get a constructible `TypeList` from any other `TypedList`;@@ -375,9 +413,9 @@ -- --   > case types ts of TypeList -> ... ---types :: forall (k :: Type) (f :: k -> Type) (xs :: [k])+types :: forall f xs        . TypedList f xs -> TypeList xs-types (TypedList xs) = unsafeCoerce# (Prelude.map (const Proxy) xs)+types = Numeric.TypedList.map (const Proxy) {-# INLINE types #-}  -- | Construct a @TypeList xs@ if there is an instance of @Typeable xs@ around.@@ -385,30 +423,29 @@ --   This way, you can always bring `RepresentableList` instance into the scope --   if you have a `Typeable` instance. ---typeables :: forall (k :: Type) (xs :: [k]) . Typeable xs => TypeList xs+typeables :: forall xs . Typeable xs => TypeList xs typeables = case R.typeRep @xs of-    R.App (R.App _ (_ :: R.TypeRep (n :: k1))) (txs :: R.TypeRep (ns :: k2))-      -> case (unsafeCoerce# (Dict @(k1 ~ k1, k2 ~ k2))-                :: Dict (k ~ k1, [k] ~ k2)) of-          Dict -> case (unsafeCoerce# (Dict @(xs ~ xs))-                          :: Dict (xs ~ (n ': ns))) of-            Dict -> Proxy @n :* R.withTypeable txs (typeables @k @ns)+    R.App (R.App _ (_ :: R.TypeRep (n :: k))) (txs :: R.TypeRep (ns :: ks))+      | Dict <- unsafeCoerce (Dict @(k ~ k, ks ~ ks))+                  :: Dict (k ~ KindOfEl xs, ks ~ KindOf xs)+      , Dict <- unsafeEqTypes @xs @(n ': ns)+      -> Proxy @n :* R.withTypeable txs (typeables @ns)     R.Con _-      -> unsafeCoerce# U+      -> unsafeCoerce U     r -> error ("typeables -- impossible typeRep: " ++ show r) {-# INLINE typeables #-}  -- | If all elements of a @TypedList@ are @Typeable@, --   then the list of these elements is also @Typeable@.-inferTypeableList :: forall (k :: Type) (f :: k -> Type) (xs :: [k])-                   . (Typeable k, All Typeable xs)+inferTypeableList :: forall f xs+                   . (Typeable (KindOfEl xs), All Typeable xs)                   => TypedList f xs -> Dict (Typeable xs) inferTypeableList U         = Dict inferTypeableList (_ :* xs) = case inferTypeableList xs of Dict -> Dict  -- | Representable type lists. --   Allows getting type information about list structure at runtime.-class RepresentableList (xs :: [k]) where+class RepresentableList xs where   -- | Get type-level constructed list   tList :: TypeList xs @@ -416,39 +453,38 @@   tList = U  instance RepresentableList xs => RepresentableList (x ': xs :: [k]) where-  tList = Proxy @x :* tList @k @xs+  tList = Proxy @x :* tList @xs  -- | Generic show function for a @TypedList@.-typedListShowsPrecC :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k])+typedListShowsPrecC :: forall c f xs                      . All c xs                     => String                        -- ^ Override cons symbol-                    -> ( forall (x :: k) . c x => Int -> f x -> ShowS )+                    -> ( forall x . c x => Int -> f x -> ShowS )                        -- ^ How to show a single element                     -> Int -> TypedList f xs -> ShowS typedListShowsPrecC _ _ _ U = showChar 'U' typedListShowsPrecC consS elShowsPrec p (x :* xs) = showParen (p >= 6)     $ elShowsPrec 6 x     . showChar ' ' . showString consS . showChar ' '-    . typedListShowsPrecC @k @c @f consS elShowsPrec 5 xs+    . typedListShowsPrecC @c @f consS elShowsPrec 5 xs  -- | Generic show function for a @TypedList@.-typedListShowsPrec :: forall (k :: Type) (f :: k -> Type) (xs :: [k])-                    . ( forall (x :: k) . Int -> f x -> ShowS )+typedListShowsPrec :: forall f xs+                    . ( forall x . Int -> f x -> ShowS )                       -- ^ How to show a single element                    -> Int -> TypedList f xs -> ShowS typedListShowsPrec _ _ U = showChar 'U' typedListShowsPrec elShowsPrec p (x :* xs) = showParen (p >= 6) $-    elShowsPrec 6 x . showString " :* " . typedListShowsPrec @k @f elShowsPrec 5 xs+    elShowsPrec 6 x . showString " :* " . typedListShowsPrec @f elShowsPrec 5 xs  -- | Generic read function for a @TypedList@. --   Requires a "template" to enforce the structure of the type list.-typedListReadPrec :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type)-                            (xs :: [k]) (g :: k -> Type)+typedListReadPrec :: forall c f xs g                    . All c xs                   => String                      -- ^ Override cons symbol-                  -> ( forall (x :: k) . c x => Read.ReadPrec (f x) )+                  -> ( forall x . c x => Read.ReadPrec (f x) )                      -- ^ How to read a single element                   -> TypedList g xs                      -- ^ Enforce the type structure of the result@@ -457,15 +493,15 @@ typedListReadPrec consS elReadPrec (_ :* ts) = Read.parens . Read.prec 5 $ do     x <- Read.step elReadPrec     Read.lift . Read.expect $ Read.Symbol consS-    xs <- typedListReadPrec @k @c consS elReadPrec ts+    xs <- typedListReadPrec @c consS elReadPrec ts     return (x :* xs)  -- | Generic read function for a @TypedList@ of unknown length.-withTypedListReadPrec :: forall (k :: Type) (f :: k -> Type) (r :: Type)+withTypedListReadPrec :: forall f (r :: Type)                        . (forall (z :: Type) .-                            ( forall (x :: k) . f x -> z) -> Read.ReadPrec z )+                            ( forall x . f x -> z) -> Read.ReadPrec z )                          -- ^ How to read a single element-                      -> (forall (xs :: [k]) . TypedList f xs -> r )+                      -> (forall xs . TypedList f xs -> r )                          -- ^ Consume the result                       -> Read.ReadPrec r withTypedListReadPrec withElReadPrec use = Read.parens $@@ -474,7 +510,7 @@     Read.prec 5 (do       WithAnyTL withX <- Read.step $ withElReadPrec (\x -> WithAnyTL $ use . (x :*))       Read.lift . Read.expect $ Read.Symbol ":*"-      withTypedListReadPrec @k @f @r withElReadPrec withX+      withTypedListReadPrec @f @r withElReadPrec withX     )  -- Workaround impredicative polymorphism@@ -494,21 +530,18 @@               . TypeList xs              -> (RepresentableList xs => r)              -> r-reifyRepList tl k = unsafeCoerce# (MagicRepList k :: MagicRepList xs r) tl+reifyRepList tl k = unsafeCoerce (MagicRepList k :: MagicRepList xs r) tl {-# INLINE reifyRepList #-} newtype MagicRepList xs r = MagicRepList (RepresentableList xs => r)  data PatReverse (f :: k -> Type) (xs :: [k])-  = forall (sx :: [k]) . (xs ~ Reverse sx, sx ~ Reverse xs)-  => PatReverse (TypedList f sx)+  = forall (sx :: [k]) . ReverseList xs sx => PatReverse (TypedList f sx)  unreverseTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])              . TypedList f xs -> PatReverse f xs-unreverseTL (TypedList xs)-  = case (unsafeCoerce# (Dict @(xs ~ xs, xs ~ xs))-           :: Dict (xs ~ Reverse sx, sx ~ Reverse xs)-         ) of-      Dict -> PatReverse (unsafeCoerce# (Prelude.reverse xs))+unreverseTL xs+  = case unsafeEqTypes @xs @(Reverse (Reverse xs)) of+      Dict -> PatReverse @k @f @xs @(Reverse xs) (Numeric.TypedList.reverse xs) {-# INLINE unreverseTL #-}  @@ -521,16 +554,16 @@  data PatSnoc (f :: k -> Type) (xs :: [k]) where   PatSNil :: PatSnoc f '[]-  PatSnoc :: TypedList f ys -> f y -> PatSnoc f (ys +: y)+  PatSnoc :: SnocList xs s xss => TypedList f xs -> f s -> PatSnoc f xss  unsnocTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])           . TypedList f xs -> PatSnoc f xs unsnocTL (TypedList [])-  = case unsafeEqTypes @_ @xs @'[] of+  = case unsafeEqTypes @xs @'[] of       Dict -> PatSNil unsnocTL (TypedList (x:xs))-  = case unsafeEqTypes @_ @xs @(Init xs +: Last xs) of-      Dict -> PatSnoc (unsafeCoerce# sy) (unsafeCoerce# y)+  = case unsafeEqTypes @xs @(Init xs +: Last xs) of+      Dict -> PatSnoc (coerce sy) (unsafeCoerce y)   where     (sy, y) = unsnoc x xs     unsnoc :: Any -> [Any] -> ([Any], Any)@@ -546,11 +579,11 @@ patTL :: forall (k :: Type) (f :: k -> Type) (xs :: [k])        . TypedList f xs -> PatCons f xs patTL (TypedList [])-  = case unsafeEqTypes @_ @xs @'[] of+  = case unsafeEqTypes @xs @'[] of       Dict -> PatCNil patTL (TypedList (x : xs))-  = case unsafeEqTypes @_ @xs  @(Head xs ': Tail xs) of-      Dict -> PatCons (unsafeCoerce# x) (unsafeCoerce# xs)+  = case unsafeEqTypes @xs  @(Head xs ': Tail xs) of+      Dict -> PatCons (unsafeCoerce x) (coerce xs) {-# INLINE patTL #-}  mkEVL :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k])@@ -564,8 +597,6 @@ _evList U         = U _evList (_ :* xs) = case _evList xs of evs -> Dict1 :* evs -unsafeEqTypes :: forall (k :: Type) (a :: k) (b :: k) . Dict (a ~ b)-unsafeEqTypes = unsafeCoerce# (Dict :: Dict (a ~ a))  dimValInt :: forall (k :: Type) (x :: k) . Dim x -> Int dimValInt = fromIntegral . dimVal

@@ -0,0 +1,193 @@+{-# LANGUAGE ConstraintKinds           #-}+{-# LANGUAGE DataKinds                 #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE ExplicitNamespaces        #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE GADTs                     #-}+{-# LANGUAGE PolyKinds                 #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE StandaloneDeriving        #-}+{-# LANGUAGE TypeApplications          #-}+{-# LANGUAGE TypeFamilies              #-}+{-# LANGUAGE TypeInType                #-}+{-# LANGUAGE TypeOperators             #-}+{-# LANGUAGE UndecidableInstances      #-}++module Data.Type.ListTest where++import Data.Constraint+import Data.Kind          (Type)+import Data.Type.Equality+import Data.Type.List+import Data.Type.Lits+import Numeric.Natural+import Test.QuickCheck+import Unsafe.Coerce++data P (a :: k) = P Natural+  deriving (Eq, Show, Read)++p :: KnownNat n => P n+p = let x = P (natVal x) in x++cmpP :: P n -> P m -> SEq n m+cmpP (P a) (P b)+  | a == b = unsafeCoerce (SEq @() @())+  | otherwise = unsafeCoerce (SNe @1 @2)++data L :: [k] -> Type where+  N :: L '[]+  (:^) :: P n -> L ns -> L (n ': ns)+infixr 5 :^++data SEq :: k -> k -> Type where+  SEq :: (a ~ b, (a == b) ~ 'True) => SEq a b+  SNe :: ((a == b) ~ 'False) => SEq a b++cmpL :: L as -> L bs -> SEq as bs+cmpL N N = SEq+cmpL (a :^ as) (b :^ bs) = case (cmpP a b, cmpL as bs) of+    (SEq, SEq) -> SEq+    (SNe, _)   -> SNe+    (_, SNe)   -> SNe+cmpL N (_ :^ _) = SNe+cmpL (_ :^ _) N = SNe++instance Show (L as) where+  show N           = ""+  show (P n :^ N)  = show n+  show (P n :^ xs) = show n ++ "." ++ show xs+++data SomeL (k :: Type) = forall (as :: [k]) . SomeL (L as)++instance Show (SomeL k) where+  show (SomeL a) = show a++x00 :: P 0+x00 = p++x01 :: P 1+x01 = p++xs00 :: L ('[] :: [Nat])+xs00 = N++xs01 :: L '[3]+xs01 = p :^ N++xs02 :: L '[4,8]+xs02 = p :^ p :^ N++xs03 :: L '[5,7,9,2]+xs03 = p :^ p :^ p :^ p :^ N++snoc :: forall (k :: Type) (xs :: [k]) (s :: k) (xss :: [k])+      . SnocList xs s xss => L xs -> P s -> L xss+snoc N x         = x :^ N+snoc (x :^ xs) y = x :^ (snoc xs y)++someXs00 :: SomeL Nat+someXs00 = SomeL xs00+someXs01 :: SomeL Nat+someXs01 = SomeL xs01+someXs02 :: SomeL Nat+someXs02 = SomeL xs02+someXs03 :: SomeL Nat+someXs03 = SomeL xs03++initL :: forall (k :: Type) (xs :: [k]) (s :: k) (xss :: [k])+       . SnocList xs s xss => L xss -> L xs+initL (_ :^ N)         = N+initL (x :^ (y :^ ys)) = x :^ initL (y :^ ys)++revL1 :: forall (k :: Type) (xs :: [k]) (sx :: [k])+     . ReverseList xs sx => L xs -> L sx+revL1 N         = N+revL1 (m :^ ms) = snoc (revL1 ms) m++revL2 :: forall (k :: Type) (xs :: [k]) (sx :: [k])+      . ReverseList xs sx => L sx -> L xs+revL2 N         = N+revL2 (m :^ ms) = snoc (revL2 ms) m++revL3 :: forall (k :: Type) (xs :: [k])+      . L xs -> L (Reverse xs)+revL3 xs = go xs N+  where+    go :: forall (ys :: [k]) (sy :: [k]) (zs :: [k])+        . ReverseList ys sy => L ys -> L zs -> L (sy ++ zs)+    go N ms         = ms+    go ((n :: P n) :^ (ns :: L ns)) ms+      | Dict <- inferConcat @sy @zs+      = go ns (n :^ ms)+++stripPrefL :: ConcatList as bs asbs => L as -> L asbs -> L bs+stripPrefL N asbs                = asbs+stripPrefL (_ :^ as) (_ :^ asbs) = stripPrefL as asbs+++stripSufL :: ConcatList as bs asbs => L bs -> L asbs -> L as+stripSufL N asbs               = asbs+stripSufL bs aasbs@(a :^ asbs) = case cmpL bs aasbs of+  SEq -> N+  SNe -> a :^ stripSufL bs asbs++concatL :: ConcatList as bs asbs => L as -> L bs -> L asbs+concatL N bs         = bs+concatL (a :^ as) bs = a :^ concatL as bs++++goList :: forall as bs asbs+        . ConcatList as bs asbs => L as -> L bs -> L asbs -> Property+goList as bs asbs = conjoin+  [ conjoin $ map ((show as ===) . show)+    [as, stripSufL bs asbs, concatL N as, concatL as N, stripSufL bs (concatL N asbs)]+  , conjoin $ map ((show bs ===) . show)+    [bs, stripPrefL as asbs, concatL N bs, concatL bs N, stripPrefL as (concatL N asbs)]+  , conjoin $ map ((show asbs ===) . show)+    [asbs, concatL as bs, concatL N asbs, concatL asbs N, concatL as (concatL N bs)]+  , -- sadly, we have to use inferConcat here, because GHC cannot voluntarily+    -- try to infer ConcatList from the appearence of Concat TF alone.+    --   A plugin would solve this.+    case inferConcat @(Reverse bs) @(Reverse as) @_ of+      Dict -> show (revL1 asbs) === show (concatL (revL1 bs) (revL1 as))+  ]+++splitN :: Int -> SomeL k -> (SomeL k, SomeL k)+splitN 0 xs = (SomeL N, xs)+splitN _ (SomeL N) = (SomeL N, SomeL N)+splitN n (SomeL (x :^ xs))+  | (SomeL as, SomeL bs) <- splitN (n-1) (SomeL xs)+    = (SomeL (snoc as x), SomeL bs)+++dropEnd :: Int -> [a] -> [a]+dropEnd n = reverse . drop n . reverse++runTests :: IO Bool+runTests = isGood <$> quickCheckResult (conjoin tests)+  where+    isGood :: Result -> Bool+    isGood Success {} = True+    isGood _          = False+    tests :: [Property]+    tests =+      [ show xs00 === show (revL1 xs00)+      , dropEnd 2 (show xs03) === show (initL xs03)+      , show xs03 === reverse (show (revL1 xs03))+      , show as   === show (stripSufL bs xs03)+      , show (snd $ splitN 0 $ SomeL asbs) === drop 0 (show asbs)+      , show (snd $ splitN 1 $ SomeL asbs) === drop 2 (show asbs)+      , show (snd $ splitN 2 $ SomeL asbs) === drop 4 (show asbs)+      , show (snd $ splitN 3 $ SomeL asbs) === drop 6 (show asbs)+      , show (snd $ splitN 4 $ SomeL asbs) === drop 8 (show asbs)+      , show (snd $ splitN 5 $ SomeL asbs) === drop 10 (show asbs)+      , goList as bs asbs+      ]+    as = initL $ initL xs03+    bs = stripPrefL as xs03+    asbs = concatL as bs

@@ -64,8 +64,8 @@   | a <- max a' b'   , b <- min a' b'   , xda <- someDimVal a -- this is an unknown (Dim (XN 0))-  , Dx (db :: Dim b) <- someDimVal b-  , Just (Dx da) <- constrainDim @_ @(XN b) xda -- here da >= db+  , Dx (db@D :: Dim b) <- someDimVal b+  , Just (Dx da) <- constrainDim @(XN b) xda -- here da >= db   = a - b == dimVal (minusDim da db) prop_minusDim _ _ = False 

@@ -10,7 +10,7 @@ {-# LANGUAGE TypeApplications          #-} {-# LANGUAGE TypeOperators             #-} -module Numeric.Dimensions.IdxTest (runTests) where+module Numeric.Dimensions.IdxTest where  import Control.Arrow import Data.List@@ -45,7 +45,7 @@ prop_idxsFromWords1 ins   | (xs, ys) <- minMaxSeq ins   , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys-  , mIs <- idxsFromWords @Nat @ds xs+  , mIs <- idxsFromWords @ds xs     = or (zipWith (==) xs ys) || isJust mIs   | otherwise     = error "Impossible arguments"@@ -55,7 +55,7 @@ prop_idxsFromWords2 ins   | (xs, ys) <- minMaxSeq ins   , SomeDims (KnownDims :: Dims ds) <- someDimsVal xs-  , mIs <- idxsFromWords @Nat @ds ys+  , mIs <- idxsFromWords @ds ys     = null xs || isNothing mIs   | otherwise     = error "Impossible arguments"@@ -65,7 +65,7 @@ prop_idxsFromWords3 ins   | (xs, ys) <- minMaxSeq ins   , SomeDims (ds@KnownDims :: Dims ds) <- someDimsVal ys-  , mIs <- idxsFromWords @Nat @ds xs+  , mIs <- idxsFromWords @ds xs     = Just False /= (go xs ds <$> mIs)   | otherwise     = error "Impossible arguments"@@ -82,14 +82,14 @@ -- check for Word overflow wouldNotOverflow :: [Word] -> Bool wouldNotOverflow-  = and . snd . mapAccumR (\a e -> (a*e, a*e >= a && multLimit > a)) 1+  = and . snd . mapAccumR (\a e -> (a*e, a*e >= a && multLimit > a && multLimit > e)) 1  prop_idxsFromEnum :: [(Word, Word)] -> Bool prop_idxsFromEnum ins   | (xs, ys) <- minMaxSeq ins   , wouldNotOverflow ys   , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys-  , Just ids <- idxsFromWords @Nat @ds xs+  , Just ids <- idxsFromWords @ds xs     = ids == toEnum (fromEnum ids)   | otherwise = True @@ -98,7 +98,7 @@   | (xs, ys) <- minMaxSeq ins   , wouldNotOverflow ys   , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys-  , Just ids <- idxsFromWords @Nat @ds xs+  , Just ids <- idxsFromWords @ds xs     = ids == maxBound || fromEnum (succ ids) == succ (fromEnum ids)   | otherwise = True @@ -107,7 +107,7 @@   | (xs, ys) <- minMaxSeq ins   , wouldNotOverflow ys   , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys-  , Just ids <- idxsFromWords @Nat @ds xs+  , Just ids <- idxsFromWords @ds xs     = ids == minBound || fromEnum (pred ids) == pred (fromEnum ids)   | otherwise = True @@ -115,7 +115,7 @@ prop_idxsPredSucc ins   | (xs, ys) <- minMaxSeq ins   , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys-  , Just ids <- idxsFromWords @Nat @ds xs+  , Just ids <- idxsFromWords @ds xs     =  ids == minBound || ids == maxBound     || ( succ (pred ids) == ids && pred (succ ids) == ids )   | otherwise = True@@ -126,23 +126,23 @@   , wouldNotOverflow ys   , product ys < 100000   , SomeDims (KnownDims :: Dims ds) <- someDimsVal ys-  , Just ids <- idxsFromWords @Nat @ds xs+  , Just ids <- idxsFromWords @ds xs     = [ids..] == map toEnum [fromEnum ids .. fromEnum (maxBound @(Idxs ds))]   | otherwise = True  prop_idxsEnumFromTo :: [(Word, Word, Word)] -> Bool prop_idxsEnumFromTo ins   | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins-  , Just ids <- idxsFromWords @Nat @ds xs-  , Just jds <- idxsFromWords @Nat @ds ys+  , Just ids <- idxsFromWords @ds xs+  , Just jds <- idxsFromWords @ds ys     = [ids..jds] == map toEnum [fromEnum ids .. fromEnum jds]   | otherwise = True  prop_idxsEnumFromThen :: [(Word, Word, Word)] -> Bool prop_idxsEnumFromThen ins   | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins-  , Just ids <- idxsFromWords @Nat @ds xs-  , Just jds <- idxsFromWords @Nat @ds ys+  , Just ids <- idxsFromWords @ds xs+  , Just jds <- idxsFromWords @ds ys   , lim <- if jds >= ids then maxBound else minBound :: Idxs ds     = take 1000 [ids, jds ..]       ==@@ -152,8 +152,8 @@ prop_idxsEnumFromThenTo :: Bool -> [(Word, Word, Word)] -> Bool prop_idxsEnumFromThenTo up ins   | (xs, ys, SomeDims (KnownDims :: Dims ds)) <- twoIdxsSeq ins-  , Just ids <- idxsFromWords @Nat @ds xs-  , Just jds <- idxsFromWords @Nat @ds ys+  , Just ids <- idxsFromWords @ds xs+  , Just jds <- idxsFromWords @ds ys   , lim <- if up then maxBound else minBound :: Idxs ds     = take 1000 [ids, jds .. lim]       ==

@@ -3,6 +3,7 @@ import Distribution.TestSuite import System.Exit +import qualified Data.Type.ListTest import qualified Numeric.Dimensions.DimTest import qualified Numeric.Dimensions.IdxTest @@ -10,7 +11,8 @@ -- | Collection of tests in detailed-0.9 format tests :: IO [Test] tests = return-  [ test "Dim"   Numeric.Dimensions.DimTest.runTests+  [ test "List"  Data.Type.ListTest.runTests+  , test "Dim"   Numeric.Dimensions.DimTest.runTests   , test "Idx"   Numeric.Dimensions.IdxTest.runTests   ]