Morley.Util.Type

General type utilities.

Documentation

class a ~ b => IsEq a b

Equality constraint in form of a typeclass.

Instances

a ~ b => IsEq (a :: k) (b :: k)

Defined in Morley.Util.Type

type family (a :: k) == (b :: k) :: Bool where ... infix 4

A type family to compute Boolean equality.

Equations

(f a :: k2) == (g b :: k2) = (f == g) && (a == b)

(a :: k) == (a :: k) = 'True

(_1 :: k) == (_2 :: k) = 'False

type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...

Type-level If. If True a b ==> a; If False a b ==> b

Equations

If 'True (tru :: k) (fls :: k) = tru

If 'False (tru :: k) (fls :: k) = fls

type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...

Append for type-level lists.

Equations

('[] :: [k]) ++ (bs :: [k]) = bs

(a ': as :: [k]) ++ (bs :: [k]) = a ': (as ++ bs)

type family IsElem (a :: k) (l :: [k]) :: Bool where ...

Equations

IsElem _ '[] = 'False

IsElem a (a ': _) = 'True

IsElem a (_ ': as) = IsElem a as

type family (l :: [k]) / (a :: k) where ...

Remove all occurences of the given element.

Equations

'[] / _ = '[]

(a ': xs) / a = xs / a

(b ': xs) / a = b ': (xs / a)

type family (l1 :: [k]) // (l2 :: [k]) :: [k] where ...

Difference between two lists.

Equations

l // '[] = l

l // (x ': xs) = (l / x) // xs

type AssertTypesEqual a b err = FailUnlessEqual a b err

An old name for FailUnlessEqual.

type FailUnlessEqual a b err = FailUnlessEqualElse a b err ()

Constrain two types to be equal, and produce an error message if they are found not to be.

>>> :k! FailUnlessEqual Int Int ('Text "This should not result in a failure")
FailUnlessEqual Int Int ('Text "This should not result in a failure") :: Constraint
= (() :: Constraint, Int ~ Int)

>>> :k! FailUnlessEqual Bool Int ('Text "This should result in a failure")
FailUnlessEqual Bool Int ('Text "This should result in a failure") :: Constraint
= ((TypeError ...), Bool ~ Int)

type FailUnlessEqualElse a b err els = (FailUnlessElsePoly (a `DefaultEq` b) err els, a ~ b)

Constrain two types to be equal. If they are found not to be, produce an error message. If they are shown to be equal, impose an additional given constraint.

>>> :k! FailUnlessEqualElse Int Int ('Text "This should not result in a failure") ()
FailUnlessEqualElse Int Int ('Text "This should not result in a failure") () :: Constraint
= (() :: Constraint, Int ~ Int)

>>> :k! FailUnlessEqualElse Bool Int ('Text "This should result in a failure") ()
FailUnlessEqualElse Bool Int ('Text "This should result in a failure") () :: Constraint
= ((TypeError ...), Bool ~ Int)

the ~ constraint might seem redundant, but, without it, GHC would reject

foo :: FailUnlessEqualElse a b MyError () => a -> b
foo = id

GHC needs to "see" the type equality ~ in order to actually "learn" something from a type family's result.

We use DefaultEq here, rather than ==, so this will work with type variables known to be equal, even if nothing is known about them concretely. For example, the following will compile:

foo :: FailUnlessEqualElse a b MyError () => a -> b
foo x = x

bar :: a -> a
bar = foo

If we used (==), then bar would be rejected.

(==) has its place (see the comments below it in Data.Type.Equality) but I don't think it has anything to offer us here. In particular, the equality constraint we bundle up seems to win us all the reasoning power that (==) would provide and more. The following adaptation of the example in the Data.Type.Equality comments compiles:

foo :: FailUnlessEqualElse (Maybe a) (Maybe b) ('Text "yo") ()
         :- FailUnlessEqualElse a b ('Text "heya") ()
foo = Sub Dict

In this example, the entire consequent follows from the equality constraint in the antecedent; the FailUnlessElsePoly part of it is irrelevant, so we don't need to be able to reason from it. If we were reasoning solely using (==), foo would be rejected because the error messages are different.

type family Guard (cond :: Bool) (a :: k) :: Maybe k where ...

Equations

Guard 'False _ = 'Nothing

Guard 'True a = 'Just a

type FailWhen cond msg = FailWhenElse cond msg ()

Fail with given error if the condition holds.

type FailWhenElse cond msg els = FailUnlessEqualElse cond 'False msg els

A version of FailWhenElsePoly that imposes an equality constraint on its Bool argument.

type family FailWhenElsePoly cond msg els where ...

Fail with given error if the condition does not hold. Otherwise, return the third argument.

There is a subtle difference between FailWhenElsePoly and the following type definition:

type FailWhenElsePolyAlternative cond msg els =
  If cond
     (TypeError msg)
     els

If cond cannot be fully reduced (e.g., it's a stuck type family application or an ambiguous type) then:

• FailWhenElsePoly will state that the constraint cannot be deduced (and this error message will be suppressed if there are also custom type errors).
• FailWhenElsePolyAlternative will fail with the given error message, err.

For example:

-- Partial function
type family IsZero (n :: Peano) :: Bool where
  IsZero ('S _) = 'False

f1 :: (IsZero n ~ 'True, FailWhenElsePoly (IsZero n) ('Text "Expected zero") (() :: Constraint)) => ()
f1 = ()

f1 :: (IsZero n ~ 'True, FailWhenElsePolyAlternative (IsZero n) ('Text "Expected zero") (() :: Constraint)) => ()
f1 = ()

f1res == f1 'Z
--  • Couldn't match type ‘IsZero 'Z’ with ‘'True’

f2res == f2 'Z
--  • Expected zero

As you can see, the error message in f2res is misleading (because the type argument actually _is_ zero), so it's preferable to fail with the standard GHC error message.

Equations

FailWhenElsePoly 'True msg _els = TypeError msg

FailWhenElsePoly 'False _ els = els

type FailUnless cond msg = FailUnlessElse cond msg ()

Fail with given error if the condition does not hold.

type FailUnlessElse b msg els = FailWhenElse (Not b) msg els

A version of FailUnlessElsePoly that imposes an equality constraint on its Bool argument.

type FailUnlessElsePoly b e k = FailWhenElsePoly (Not b) e k

Fail with given error if the condition does not hold. Otherwise, return the third argument.

failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True)

A natural conclusion from the fact that an error has not occurred.

failWhenEvi :: forall cond msg. FailWhen cond msg :- (cond ~ 'False)

type family AllUnique (l :: [k]) :: Bool where ...

Equations

AllUnique '[] = 'True

AllUnique (x ': xs) = Not (IsElem x xs) && AllUnique xs

type RequireAllUnique desc l = RequireAllUnique' desc l l

class ReifyList (c :: k -> Constraint) (l :: [k]) where

Bring type-level list at term-level using given function to demote its individual elements.

Methods

reifyList :: (forall a. c a => Proxy a -> r) -> [r]

Instances

ReifyList (c :: k -> Constraint) ('[] :: [k])

Defined in Morley.Util.Type

Methods

reifyList :: (forall (a :: k0). c a => Proxy a -> r) -> [r]

(c x, ReifyList c xs) => ReifyList (c :: a -> Constraint) (x ': xs :: [a])

Defined in Morley.Util.Type

Methods

reifyList :: (forall (a0 :: k). c a0 => Proxy a0 -> r) -> [r]

type family PatternMatch (a :: Type) :: Constraint where ...

Make sure given type is evaluated. This type family fits only for types of Type kind.

Equations

PatternMatch Int = ((), ())

PatternMatch _ = ()

type family PatternMatchL (l :: [k]) :: Constraint where ...

Equations

PatternMatchL '[] = ((), ())

PatternMatchL _ = ()

class KnownList l where

Similar to SingI [], but does not require individual elements to be also instance of SingI.

Methods

klist :: KList l

Instances

KnownList ('[] :: [k])

Defined in Morley.Util.Type

Methods

klist :: KList '[]

KnownList xs => KnownList (x ': xs :: [k])

Defined in Morley.Util.Type

Methods

klist :: KList (x ': xs)

data KList (l :: [k]) where

Data.List.Singletons.SList analogue for KnownList.

Constructors

KNil :: KList '[]

KCons :: KnownList xs => Proxy x -> Proxy xs -> KList (x ': xs)

type RSplit l r = KnownList l

rsplit :: forall k (l :: [k]) (r :: [k]) f. RSplit l r => Rec f (l ++ r) -> (Rec f l, Rec f r)

Split a record into two pieces.

data Some1 (f :: k -> Type)

A value of type parametrized with some type parameter.

Constructors

forall a. Some1 (f a)

Instances

(forall (a :: k). Show (f a)) => Show (Some1 f)

Defined in Morley.Util.Type

Methods

showsPrec :: Int -> Some1 f -> ShowS

show :: Some1 f -> String

showList :: [Some1 f] -> ShowS

recordToSomeList :: Rec f l -> [Some1 f]

type ConcatListOfTypesAssociativity a b c = ((a ++ b) ++ c) ~ (a ++ (b ++ c))

listOfTypesConcatAssociativityAxiom :: forall a b c. Dict (ConcatListOfTypesAssociativity a b c)

GHC can't deduce this itself because in general a type family might be not associative, what brings extra difficulties and redundant constraints, especially if you have complex types. But (++) type family is associative, so let's define this small hack.

class MockableConstraint (c :: Constraint) where

Constaints that can be provided on demand.

Needless to say, this is a pretty unsafe operation. This typeclass makes using it safer in a sense that getting a segfault becomes harder, but still it deceives the type system and should be used only if providing a proper proof would be too difficult.

Methods

unsafeProvideConstraint :: Dict c

Produce a constraint out of thin air.

Instances

c a => MockableConstraint (c a)

In majority of the cases we don't want to mock typeclass constraints since coercing instances of typeclasses with methods is utterly unsafe.

Defined in Morley.Util.Type

Methods

unsafeProvideConstraint :: Dict (c a)

(MockableConstraint c1, MockableConstraint c2) => MockableConstraint (c1, c2)

Defined in Morley.Util.Type

Methods

unsafeProvideConstraint :: Dict (c1, c2)

(MockableConstraint c1, MockableConstraint c2, MockableConstraint c3) => MockableConstraint (c1, c2, c3)

Defined in Morley.Util.Type

Methods

unsafeProvideConstraint :: Dict (c1, c2, c3)

MockableConstraint (RequireLongerOrSameLength l a)

Defined in Morley.Util.Peano

Methods

unsafeProvideConstraint :: Dict (RequireLongerOrSameLength l a)

MockableConstraint (RequireLongerThan l a)

Defined in Morley.Util.Peano

Methods

unsafeProvideConstraint :: Dict (RequireLongerThan l a)

MockableConstraint (a ~ b)

Defined in Morley.Util.Type

Methods

unsafeProvideConstraint :: Dict (a ~ b)

(MockableConstraint c1, MockableConstraint c2, MockableConstraint c3, MockableConstraint c4) => MockableConstraint (c1, c2, c3, c4)

Defined in Morley.Util.Type

Methods

unsafeProvideConstraint :: Dict (c1, c2, c3, c4)

(MockableConstraint c1, MockableConstraint c2, MockableConstraint c3, MockableConstraint c4, MockableConstraint c5) => MockableConstraint (c1, c2, c3, c4, c5)

Defined in Morley.Util.Type

Methods

unsafeProvideConstraint :: Dict (c1, c2, c3, c4, c5)

onFirst :: Bifunctor p => p a c -> (a -> b) -> p b c

Utility function to help transform the first argument of a binfunctor.

knownListFromSingI :: forall xs. SingI xs => Dict (KnownList xs)

Given a type-level list that is SingI, construct evidence that it is also a KnownList. Note that KnownList is weaker, hence this construction is always possible.