Modulerefined-0.8.2Haskell2010

Refined.Unsafe

This module exposes unsafe refinements. An unsafe refinement is one which either does not make the guarantee of totality in construction of the Refined value or does not perform a check of the refinement predicate. It is recommended only to use this when you can manually prove that the refinement predicate holds.

1 type
5 values

Packagerefined-0.8.2
Exports6
LanguageHaskell2010
LicenceMIT
SourceUnsafe.hs

Refined

1 declaration

newtypenewtype Refined (p :: k) x

A refinement type, which wraps a value of type x.

Instances13Lift, Foldable, Eq, Ord, Read, Show, …

Lift x => Lift (Refined p x)Defined in refined-0.8.2 · Refined.Unsafe.Type
Foldable (Refined p)Defined in refined-0.8.2 · Refined.Unsafe.Type
Eq x => Eq (Refined p x)Defined in refined-0.8.2 · Refined.Unsafe.Type
Ord x => Ord (Refined p x)Defined in refined-0.8.2 · Refined.Unsafe.Type
(Read x, Predicate p x) => Read (Refined p x)Defined in refined-0.8.2 · Refined · orphan
This instance makes sure to check the refinement.
Show x => Show (Refined p x)Defined in refined-0.8.2 · Refined.Unsafe.Type
NFData x => NFData (Refined p x)Defined in refined-0.8.2 · Refined.Unsafe.Type
(Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a)Defined in refined-0.8.2 · Refined · orphan
Hashable x => Hashable (Refined p x)Defined in refined-0.8.2 · Refined.Unsafe.Type
(FromJSON a, Predicate p a) => FromJSON (Refined p a)Defined in refined-0.8.2 · Refined · orphan
(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a)Defined in refined-0.8.2 · Refined · orphan
(ToJSON a, Predicate p a) => ToJSON (Refined p a)Defined in refined-0.8.2 · Refined · orphan
(ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a)Defined in refined-0.8.2 · Refined · orphan

Creation

valuereallyUnsafeRefine :: x -> Refined p x

Constructs a Refined value, completely ignoring any refinements! Use this only when you can manually prove that the refinement holds.

valueunsafeRefine :: Predicate p x => x -> Refined p x

Constructs a Refined value at run-time, calling error if the value does not satisfy the predicate.

WARNING: this function is not total!

Coercion

valuereallyUnsafeUnderlyingRefined :: Coercion x (Refined p x)

A coercion between a type and any refinement of that type. See Data.Type.Coercion for functions manipulating coercions.

valuereallyUnsafeAllUnderlyingRefined

:: (forall x y (p :: k). Coercible x y => Coercible y (Refined p x)) => r
-> r

Reveal that x and Refined p x are Coercible for all x and p simultaneously.

Example

reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)
reallyUnsafePredEquiv = reallyUnsafeAllUnderlyingRefined Coercion

valuereallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)

A coercion between two Refined types, magicking up the claim that one predicate is entirely equivalent to another.