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 (++) as bs = as ++ bs infixr 5

Append for type-level lists. We use this synonym instead of using the one from Data.Vinyl.TypeLevel directly because the latter is missing a fixity declaration. See the vinyl pull request.

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 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 ('Text "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 ('Text "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 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.

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 cond msg els = FailUnlessEqualElse cond 'True msg els

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

type family FailUnlessElsePoly b e k where ...

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

Equations

FailUnlessElsePoly 'False msg _els = TypeError msg

FailUnlessElsePoly 'True _ els = els

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]

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.