[#27] Introduce Terminating constraint for preventing hanging showMemory

membrain.cabal

@@ -50,6 +50,7 @@ common common-options
                        -fhide-source-paths
                        -Wmissing-export-lists
                        -Wpartial-fields
+                       -freduction-depth=250
   if impl(ghc >= 8.8.1)
     ghc-options:       -Wmissing-deriving-strategies
                        -Werror=missing-deriving-strategies

src/Membrain/Memory.hs

@@ -1,4 +1,6 @@
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 {-# LANGUAGE AllowAmbiguousTypes       #-}
+{-# LANGUAGE CPP                       #-}
 {-# LANGUAGE DataKinds                 #-}
 {-# LANGUAGE DerivingStrategies        #-}
 {-# LANGUAGE ExistentialQuantification #-}
@@ -56,6 +58,10 @@ import Numeric.Natural (Natural)
 
 import Membrain.Units (KnownUnitSymbol, unitSymbol)
 
+#if ( __GLASGOW_HASKELL__ >= 804 )
+import Membrain.Units (Terminating)
+#endif
+
 import qualified Prelude
 
 
@@ -104,6 +110,12 @@ instance Monoid (Memory (mem :: Nat)) where
     mconcat = foldl' (<>) mempty
     {-# INLINE mconcat #-}
 
+#if ( __GLASGOW_HASKELL__ >= 804 )
+type KnownMem mem = (KnownNat mem, KnownUnitSymbol mem, Terminating mem)
+#else
+type KnownMem mem = (KnownNat mem, KnownUnitSymbol mem)
+#endif
+
 {- |
 This 'showMemory' function shows a 'Memory' value as 'Double' along with the
 measure unit suffix. It shows 'Memory' losslessly while used with standardized
@@ -119,7 +131,7 @@ different forms of units then the 'show' function for 'Memory' hangs.
 >>> showMemory (Memory 22 :: Memory Byte)
 "2.75B"
 -}
-showMemory :: forall mem . (KnownNat mem, KnownUnitSymbol mem) => Memory mem -> String
+showMemory :: forall mem . (KnownMem mem) => Memory mem -> String
 showMemory (Memory m) = showFrac m (nat @mem) ++ unitSymbol @mem
   where
     showFrac :: Natural -> Natural -> String
@@ -308,7 +320,7 @@ collections, or when 'Memory' of non-specified unit can be returned.
 
 -- | Existential data type for 'Memory's.
 data AnyMemory
-    = forall (mem :: Nat) . (KnownNat mem, KnownUnitSymbol mem)
+    = forall (mem :: Nat) . (KnownMem mem)
     => MkAnyMemory (Memory mem)
 
 instance Show AnyMemory where

src/Membrain/Units.hs

@@ -5,6 +5,7 @@
 {-# LANGUAGE MagicHash              #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
 #if ( __GLASGOW_HASKELL__ >= 806 )
 {-# LANGUAGE NoStarIsType           #-}
 #endif
@@ -58,11 +59,20 @@ module Membrain.Units
        , UnitSymbol
        , KnownUnitSymbol
        , unitSymbol
+
+#if ( __GLASGOW_HASKELL__ >= 804 )
+         -- * Type family for unit safety
+       , Terminating
+#endif
        ) where
 
+import Data.Kind (Constraint)
 import GHC.Exts (Proxy#, proxy#)
-import GHC.TypeLits (KnownSymbol, Symbol, symbolVal')
+import GHC.TypeLits (ErrorMessage (..), KnownSymbol, Symbol, TypeError, symbolVal')
 import GHC.TypeNats (type (*), Nat)
+#if ( __GLASGOW_HASKELL__ >= 804 )
+import GHC.TypeNats (Div, Mod)
+#endif
 
 
 type Bit       = 1
@@ -140,3 +150,41 @@ only with @-XTypeApplications@.
 unitSymbol :: forall (mem :: Nat) . KnownUnitSymbol mem => String
 unitSymbol = symbolVal' (proxy# :: Proxy# (UnitSymbol mem))
 {-# INLINE unitSymbol #-}
+
+#if ( __GLASGOW_HASKELL__ >= 804 )
+
+-- | Decides whether given decimal is a terminating decimal or not.
+type family Terminating (val :: Nat) :: Constraint where
+  Terminating v = TerminatingOrig v v
+
+-- | Decides whether given decimal is a terminating decimal or not but preserves
+-- the original number. It's used for generating the error message in @Terminating2@.
+type family TerminatingOrig (original :: Nat) (val :: Nat) :: Constraint where
+  TerminatingOrig _ 1 = ()
+  TerminatingOrig original v = Terminating5 original (v `Mod` 5) v
+
+-- | Decides whether given decimal is divisible by 5 or not.
+-- If it is divisible, divides it and sends it back to @TerminatingOrig@ for further reduction.
+-- If it is not, sends it to @Terminating2@ to see if it's in the form of 2^x.
+type family Terminating5 (original :: Nat) (mod_result :: Nat) (val :: Nat) :: Constraint where
+  Terminating5 original 0 v = TerminatingOrig original (v `Div` 5)
+  Terminating5 original _ v = Terminating2 original (v `Mod` 2) v
+
+-- | Decides whether given decimal is divisible by 2 or not.
+-- If it is divisible, divides it and sends it back to @TerminatingOrig@ for further reduction.
+-- If it is not, this is an error since;
+--   The value is not 1
+--   The value is not divisible by 2 or 5.
+--
+-- Conditions above means that this is not a "terminating decimal":
+-- https://en.wikipedia.org/wiki/Repeating_decimal
+type family Terminating2 (original :: Nat) (mod_result :: Nat) (val :: Nat) :: Constraint where
+  Terminating2 original 0 v = TerminatingOrig original (v `Div` 2)
+  Terminating2 original _ mul =
+    TypeError ('Text "Value "
+         ':<>: 'ShowType original
+         ':<>: 'Text " should only multipliers of 2 and 5"
+         ':<>: 'Text " (ie. should be in form 2^x.5^y)"
+         ':$$: 'Text "but it has the multiplier " ':<>: 'ShowType mul
+         ':$$: 'Text "See showMemory function for why this is needed.")
+#endif

test/Doctest.hs

@@ -16,4 +16,5 @@ main = do
         : "-XDerivingStrategies"
         : "-XGeneralizedNewtypeDeriving"
         : "-XDeriveGeneric"
+        : "-freduction-depth=250"
         : sourceFiles