{-# LANGUAGE FunctionalDependencies #-}

module Strongweak.Strengthen.Unsafe where

import Numeric.Natural
import Data.Word
import Data.Int
import Refined ( Refined )
import Refined.Unsafe ( reallyUnsafeRefine )
import Data.Vector.Sized ( Vector )
import Data.Vector.Generic.Sized.Internal qualified
import Data.Vector qualified

{- | Any 'w' can be unsafely "strengthened" into an 's' by pretending that we've
     asserted some properties.

For example, you may unsafely strengthen some 'Natural' @n@ into a 'Word8' by
unsafely coercing the value, ignoring the possibility that @n >= 255@.

Currently, this class is more of a thought experiment than something to use.
That is to say, do not use this.

This typeclass should probably follow its big sis 'Strengthen'. Only provide
'UnsafeStrengthen' instances for types that have similar 'Strengthen' instances.
-}
class UnsafeStrengthen w s | s -> w where unsafeStrengthen :: w -> s

-- | 'unsafeStrengthen' with reordered type variables for more convenient
--   visible type application.
unsafeStrengthen' :: forall s w. UnsafeStrengthen w s => w -> s
unsafeStrengthen' :: forall s w. UnsafeStrengthen w s => w -> s
unsafeStrengthen' = w -> s
forall w s. UnsafeStrengthen w s => w -> s
unsafeStrengthen

-- | Unsafely strengthen each element of a list.
instance UnsafeStrengthen w s => UnsafeStrengthen [w] [s] where
    unsafeStrengthen :: [w] -> [s]
unsafeStrengthen = (w -> s) -> [w] -> [s]
forall a b. (a -> b) -> [a] -> [b]
map w -> s
forall w s. UnsafeStrengthen w s => w -> s
unsafeStrengthen

-- | Obtain a sized vector by unsafely assuming the size of a plain list.
--   Extremely unsafe.
instance UnsafeStrengthen [a] (Vector n a) where
    unsafeStrengthen :: [a] -> Vector n a
unsafeStrengthen = Vector a -> Vector n a
forall (v :: * -> *) (n :: Nat) a. v a -> Vector v n a
Data.Vector.Generic.Sized.Internal.Vector (Vector a -> Vector n a) -> ([a] -> Vector a) -> [a] -> Vector n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Vector a
forall a. [a] -> Vector a
Data.Vector.fromList

-- | Obtain a refined type by ignoring the predicate.
instance UnsafeStrengthen a (Refined p a) where
    unsafeStrengthen :: a -> Refined p a
unsafeStrengthen = a -> Refined p a
forall a p. a -> Refined p a
reallyUnsafeRefine

-- Coerce 'Natural's into Haskell's bounded unsigned numeric types. Poorly-sized
-- values will safely overflow according to the type's behaviour.
instance UnsafeStrengthen Natural Word8  where unsafeStrengthen :: Nat -> Word8
unsafeStrengthen = Nat -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Natural Word16 where unsafeStrengthen :: Nat -> Word16
unsafeStrengthen = Nat -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Natural Word32 where unsafeStrengthen :: Nat -> Word32
unsafeStrengthen = Nat -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Natural Word64 where unsafeStrengthen :: Nat -> Word64
unsafeStrengthen = Nat -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral

-- Coerce 'Integer's into Haskell's bounded signed numeric types. Poorly-sized
-- values will safely overflow according to the type's behaviour.
instance UnsafeStrengthen Integer Int8   where unsafeStrengthen :: Integer -> Int8
unsafeStrengthen = Integer -> Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Integer Int16  where unsafeStrengthen :: Integer -> Int16
unsafeStrengthen = Integer -> Int16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Integer Int32  where unsafeStrengthen :: Integer -> Int32
unsafeStrengthen = Integer -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Integer Int64  where unsafeStrengthen :: Integer -> Int64
unsafeStrengthen = Integer -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral