Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
General type utilities.
Synopsis
- class a ~ b => IsEq a b
- type family (a :: k) == (b :: k) :: Bool where ...
- type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
- type (++) as bs = as ++ bs
- type family IsElem (a :: k) (l :: [k]) :: Bool where ...
- type family (l :: [k]) / (a :: k) where ...
- type family (l1 :: [k]) // (l2 :: [k]) :: [k] where ...
- type FailUnlessEqual a b err = FailUnlessEqualElse a b err ()
- type FailUnlessEqualElse a b err els = (FailUnlessElsePoly (a `DefaultEq` b) err els, a ~ b)
- type FailWhen cond msg = FailWhenElse cond msg ()
- type FailWhenElse cond msg els = FailUnlessEqualElse cond 'False msg els
- type family FailWhenElsePoly cond msg els where ...
- type FailUnless cond msg = FailUnlessElse cond msg ()
- type FailUnlessElse cond msg els = FailUnlessEqualElse cond 'True msg els
- type FailUnlessElsePoly b e k = FailWhenElsePoly (Not b) e k
- failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True)
- failWhenEvi :: forall cond msg. FailWhen cond msg :- (cond ~ 'False)
- type family AllUnique (l :: [k]) :: Bool where ...
- type RequireAllUnique desc l = RequireAllUnique' desc l l
- class ReifyList (c :: k -> Constraint) (l :: [k]) where
- type family PatternMatch (a :: Type) :: Constraint where ...
- type family PatternMatchL (l :: [k]) :: Constraint where ...
- class KnownList l where
- data KList (l :: [k]) where
- 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)
- data Some1 (f :: k -> Type) = forall a. Some1 (f a)
- 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)
- class MockableConstraint (c :: Constraint) where
- onFirst :: Bifunctor p => p a c -> (a -> b) -> p b c
- knownListFromSingI :: forall xs. SingI xs => Dict (KnownList xs)
Documentation
class a ~ b => IsEq a b Source #
Equality constraint in form of a typeclass.
Instances
a ~ b => IsEq (a :: k) (b :: k) Source # | |
Defined in Morley.Util.Type |
type family (a :: k) == (b :: k) :: Bool where ... infix 4 #
A type family to compute Boolean equality.
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #
Type-level If. If True a b
==> a
; If False a b
==> b
type (++) as bs = as ++ bs infixr 5 Source #
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 FailUnlessEqual a b err = FailUnlessEqualElse a b err () Source #
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) Source #
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 () Source #
Fail with given error if the condition holds.
type FailWhenElse cond msg els = FailUnlessEqualElse cond 'False msg els Source #
A version of FailWhenElsePoly
that imposes an equality constraint on its
Bool
argument.
type family FailWhenElsePoly cond msg els where ... Source #
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 (DelayError 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 = () -- f2 :: ( IsZero n ~ 'True , FailWhenElsePolyAlternative (IsZero n) ('Text "Expected zero") (() :: Constraint)) => () f2 = () :}
>>>
f1 @'Z
... ... • Couldn't match type ‘IsZero 'Z’ with ‘'True’ ...
>>>
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.
FailWhenElsePoly 'True msg _els = TypeError msg | |
FailWhenElsePoly 'False _ els = els |
type FailUnless cond msg = FailUnlessElse cond msg () Source #
Fail with given error if the condition does not hold.
type FailUnlessElse cond msg els = FailUnlessEqualElse cond 'True msg els Source #
A version of FailUnlessElsePoly
that imposes an equality constraint on its
Bool
argument.
type FailUnlessElsePoly b e k = FailWhenElsePoly (Not b) e k Source #
Fail with given error if the condition does not hold. Otherwise, return the third argument.
failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True) Source #
Deprecated: FailUnless should carry the corresponding type equality already
A natural conclusion from the fact that an error has not occurred.
failWhenEvi :: forall cond msg. FailWhen cond msg :- (cond ~ 'False) Source #
Deprecated: FailWhen should carry the corresponding type equality already
type RequireAllUnique desc l = RequireAllUnique' desc l l Source #
class ReifyList (c :: k -> Constraint) (l :: [k]) where Source #
Bring type-level list at term-level using given function to demote its individual elements.
Instances
ReifyList (c :: k -> Constraint) ('[] :: [k]) Source # | |
Defined in Morley.Util.Type | |
(c x, ReifyList c xs) => ReifyList (c :: a -> Constraint) (x ': xs :: [a]) Source # | |
Defined in Morley.Util.Type |
type family PatternMatch (a :: Type) :: Constraint where ... Source #
Make sure given type is evaluated.
This type family fits only for types of Type
kind.
PatternMatch Int = ((), ()) | |
PatternMatch _ = () |
type family PatternMatchL (l :: [k]) :: Constraint where ... Source #
PatternMatchL '[] = ((), ()) | |
PatternMatchL _ = () |
class KnownList l where Source #
Similar to SingI []
, but does not require individual elements to be also
instance of SingI
.
rsplit :: forall k (l :: [k]) (r :: [k]) f. RSplit l r => Rec f (l ++ r) -> (Rec f l, Rec f r) Source #
Split a record into two pieces.
data Some1 (f :: k -> Type) Source #
A value of type parametrized with some type parameter.
forall a. Some1 (f a) |
recordToSomeList :: Rec f l -> [Some1 f] Source #
type ConcatListOfTypesAssociativity a b c = ((a ++ b) ++ c) ~ (a ++ (b ++ c)) Source #
Deprecated: Unused; use the definition instead
listOfTypesConcatAssociativityAxiom :: forall a b c. Dict (ConcatListOfTypesAssociativity a b c) Source #
Deprecated: Unused; a less ad-hoc version is available from Morley.Michelson.Typed.Instr.Internal.Proofs.assocThm
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 Source #
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.
unsafeProvideConstraint :: Dict c Source #
Deprecated: Apparently unused, and turns out to be very unsafe in practice.
Produce a constraint out of thin air.