constraints 0.14.2 → 0.14.3
raw patch · 4 files changed
+14/−11 lines, 4 filesdep −ghc-primPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies removed: ghc-prim
API changes (from Hackage documentation)
- Data.Constraint: [Dict] :: a => Dict a
+ Data.Constraint: [Dict] :: forall a. a => Dict a
- Data.Constraint: class Any => Bottom
+ Data.Constraint: class Any :: Constraint => Bottom
- Data.Constraint: data Dict :: Constraint -> *
+ Data.Constraint: data Dict a
- Data.Constraint: implied :: forall a b. (a => b) => a :- b
+ Data.Constraint: implied :: (a => b) => a :- b
- Data.Constraint.Char: charToNat :: forall c. KnownChar c :- KnownNat (CharToNat c)
+ Data.Constraint.Char: charToNat :: forall (c :: Char). KnownChar c :- KnownNat (CharToNat c)
- Data.Constraint.Char: natToChar :: forall n. (n <= 0x10FFFF, KnownNat n) :- KnownChar (NatToChar n)
+ Data.Constraint.Char: natToChar :: forall (n :: Natural). (n <= 1114111, KnownNat n) :- KnownChar (NatToChar n)
- Data.Constraint.Deferrable: data () => (a :: k) :~: (b :: k)
+ Data.Constraint.Deferrable: data (a :: k) :~: (b :: k)
- Data.Constraint.Deferrable: defer :: forall p r. Deferrable p => (p => r) -> r
+ Data.Constraint.Deferrable: defer :: Deferrable p => (p => r) -> r
- Data.Constraint.Deferrable: deferred :: forall p. Deferrable p :- p
+ Data.Constraint.Deferrable: deferred :: Deferrable p :- p
- Data.Constraint.Forall: class (forall a. p a) => Forall (p :: k -> Constraint)
+ Data.Constraint.Forall: class forall (a :: k). () => p a => Forall (p :: k -> Constraint)
- Data.Constraint.Forall: class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)
+ Data.Constraint.Forall: class Forall ComposeC p f => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)
- Data.Constraint.Forall: class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4)
+ Data.Constraint.Forall: class Forall Q p t => ForallT (p :: k4 -> Constraint) (t :: k1 -> k2 -> k3 -> k4)
- Data.Constraint.Forall: forall_ :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)
+ Data.Constraint.Forall: forall_ :: (forall (a :: k). () => Dict (p a)) -> Dict (Forall p)
- Data.Constraint.Forall: inst :: forall p a. Forall p :- p a
+ Data.Constraint.Forall: inst :: forall {k} p (a :: k). Forall p :- p a
- Data.Constraint.Forall: inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f
+ Data.Constraint.Forall: inst1 :: forall p (f :: Type -> Type). Forall p :- p f
- Data.Constraint.Forall: instF :: forall p f a. ForallF p f :- p (f a)
+ Data.Constraint.Forall: instF :: forall {k2} {k1} p (f :: k1 -> k2) (a :: k1). ForallF p f :- p (f a)
- Data.Constraint.Forall: instT :: forall k1 k2 k3 k4 (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
+ Data.Constraint.Forall: instT :: forall k1 k2 k3 k4 p (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
- Data.Constraint.Forall: type Forall1 p = Forall p
+ Data.Constraint.Forall: type Forall1 (p :: k -> Constraint) = Forall p
- Data.Constraint.Lifting: class Lifting p f
+ Data.Constraint.Lifting: class Lifting (p :: k -> Constraint) (f :: k -> k)
- Data.Constraint.Lifting: class Lifting2 p f
+ Data.Constraint.Lifting: class Lifting2 (p :: k -> Constraint) (f :: k -> k -> k)
- Data.Constraint.Lifting: lifting :: Lifting p f => p a :- p (f a)
+ Data.Constraint.Lifting: lifting :: forall (a :: k). Lifting p f => p a :- p (f a)
- Data.Constraint.Lifting: lifting2 :: Lifting2 p f => p a :- Lifting p (f a)
+ Data.Constraint.Lifting: lifting2 :: forall (a :: k). Lifting2 p f => p a :- Lifting p (f a)
- Data.Constraint.Nat: divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c)
+ Data.Constraint.Nat: divMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- (Div a c <= Div b c)
- Data.Constraint.Nat: divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b)
+ Data.Constraint.Nat: divMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- (Div a c <= Div a b)
- Data.Constraint.Nat: divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
+ Data.Constraint.Nat: divNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)
- Data.Constraint.Nat: dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)
+ Data.Constraint.Nat: dividesDef :: forall (a :: Nat) (b :: Nat). Divides a b :- (Mod b a ~ 0)
- Data.Constraint.Nat: dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
+ Data.Constraint.Nat: dividesGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Gcd b c)
- Data.Constraint.Nat: dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c
+ Data.Constraint.Nat: dividesLcm :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a c, Divides b c) :- Divides (Lcm a b) c
- Data.Constraint.Nat: dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)
+ Data.Constraint.Nat: dividesMax :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Max b c)
- Data.Constraint.Nat: dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)
+ Data.Constraint.Nat: dividesMin :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (Min b c)
- Data.Constraint.Nat: dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)
+ Data.Constraint.Nat: dividesPlus :: forall (a :: Nat) (b :: Nat) (c :: Nat). (Divides a b, Divides a c) :- Divides a (b + c)
- Data.Constraint.Nat: dividesPow :: (1 <= n, Divides a b) :- Divides a (b ^ n)
+ Data.Constraint.Nat: dividesPow :: forall (n :: Natural) (a :: Nat) (b :: Nat). (1 <= n, Divides a b) :- Divides a (b ^ n)
- Data.Constraint.Nat: dividesTimes :: Divides a b :- Divides a (b * c)
+ Data.Constraint.Nat: dividesTimes :: forall (a :: Nat) (b :: Nat) (c :: Natural). Divides a b :- Divides a (b * c)
- Data.Constraint.Nat: euclideanNat :: (1 <= c) :- (a ~ ((c * Div a c) + Mod a c))
+ Data.Constraint.Nat: euclideanNat :: forall (c :: Natural) (a :: Natural). (1 <= c) :- (a ~ ((c * Div a c) + Mod a c))
- Data.Constraint.Nat: gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))
+ Data.Constraint.Nat: gcdAssociates :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))
- Data.Constraint.Nat: gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a)
+ Data.Constraint.Nat: gcdCommutes :: forall (a :: Nat) (b :: Nat). Dict (Gcd a b ~ Gcd b a)
- Data.Constraint.Nat: gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
+ Data.Constraint.Nat: gcdDistributesOverLcm :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))
- Data.Constraint.Nat: gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)
+ Data.Constraint.Nat: gcdIsIdempotent :: forall (n :: Nat). Dict (Gcd n n ~ n)
- Data.Constraint.Nat: gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
+ Data.Constraint.Nat: gcdNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)
- Data.Constraint.Nat: gcdOne :: forall a. Dict (Gcd 1 a ~ 1)
+ Data.Constraint.Nat: gcdOne :: forall (a :: Nat). Dict (Gcd 1 a ~ 1)
- Data.Constraint.Nat: gcdZero :: forall a. Dict (Gcd 0 a ~ a)
+ Data.Constraint.Nat: gcdZero :: forall (a :: Nat). Dict (Gcd 0 a ~ a)
- Data.Constraint.Nat: lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
+ Data.Constraint.Nat: lcmAssociates :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))
- Data.Constraint.Nat: lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a)
+ Data.Constraint.Nat: lcmCommutes :: forall (a :: Nat) (b :: Nat). Dict (Lcm a b ~ Lcm b a)
- Data.Constraint.Nat: lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
+ Data.Constraint.Nat: lcmDistributesOverGcd :: forall (a :: Nat) (b :: Nat) (c :: Nat). Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))
- Data.Constraint.Nat: lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)
+ Data.Constraint.Nat: lcmIsIdempotent :: forall (n :: Nat). Dict (Lcm n n ~ n)
- Data.Constraint.Nat: lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
+ Data.Constraint.Nat: lcmNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
- Data.Constraint.Nat: lcmOne :: forall a. Dict (Lcm 1 a ~ a)
+ Data.Constraint.Nat: lcmOne :: forall (a :: Nat). Dict (Lcm 1 a ~ a)
- Data.Constraint.Nat: lcmZero :: forall a. Dict (Lcm 0 a ~ 0)
+ Data.Constraint.Nat: lcmZero :: forall (a :: Nat). Dict (Lcm 0 a ~ 0)
- Data.Constraint.Nat: leZero :: forall a. (a <= 0) :- (a ~ 0)
+ Data.Constraint.Nat: leZero :: forall (a :: Natural). (a <= 0) :- (a ~ 0)
- Data.Constraint.Nat: log2Nat :: forall n. (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
+ Data.Constraint.Nat: log2Nat :: forall (n :: Nat). (KnownNat n, 1 <= n) :- KnownNat (Log2 n)
- Data.Constraint.Nat: log2Pow :: forall n. Dict (Log2 (2 ^ n) ~ n)
+ Data.Constraint.Nat: log2Pow :: forall (n :: Natural). Dict (Log2 (2 ^ n) ~ n)
- Data.Constraint.Nat: maxAssociates :: forall m n o. Dict (Max (Max m n) o ~ Max m (Max n o))
+ Data.Constraint.Nat: maxAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat). Dict (Max (Max m n) o ~ Max m (Max n o))
- Data.Constraint.Nat: maxCommutes :: forall n m. Dict (Max m n ~ Max n m)
+ Data.Constraint.Nat: maxCommutes :: forall (n :: Nat) (m :: Nat). Dict (Max m n ~ Max n m)
- Data.Constraint.Nat: maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
+ Data.Constraint.Nat: maxDistributesOverMin :: forall (n :: Nat) (m :: Nat) (o :: Nat). Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))
- Data.Constraint.Nat: maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))
+ Data.Constraint.Nat: maxDistributesOverPlus :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n + Max m o) ~ Max (n + m) (n + o))
- Data.Constraint.Nat: maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
+ Data.Constraint.Nat: maxDistributesOverPow1 :: forall (n :: Nat) (m :: Nat) (o :: Natural). Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))
- Data.Constraint.Nat: maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
+ Data.Constraint.Nat: maxDistributesOverPow2 :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))
- Data.Constraint.Nat: maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))
+ Data.Constraint.Nat: maxDistributesOverTimes :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Max m o) ~ Max (n * m) (n * o))
- Data.Constraint.Nat: maxIsIdempotent :: forall n. Dict (Max n n ~ n)
+ Data.Constraint.Nat: maxIsIdempotent :: forall (n :: Nat). Dict (Max n n ~ n)
- Data.Constraint.Nat: maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c)
+ Data.Constraint.Nat: maxMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b) :- (Max a c <= Max b c)
- Data.Constraint.Nat: maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c)
+ Data.Constraint.Nat: maxMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c) :- (Max a b <= Max a c)
- Data.Constraint.Nat: maxNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)
+ Data.Constraint.Nat: maxNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Max n m)
- Data.Constraint.Nat: maxZero :: forall n. Dict (Max n 0 ~ n)
+ Data.Constraint.Nat: maxZero :: forall (n :: Nat). Dict (Max n 0 ~ n)
- Data.Constraint.Nat: minAssociates :: forall m n o. Dict (Min (Min m n) o ~ Min m (Min n o))
+ Data.Constraint.Nat: minAssociates :: forall (m :: Nat) (n :: Nat) (o :: Nat). Dict (Min (Min m n) o ~ Min m (Min n o))
- Data.Constraint.Nat: minCommutes :: forall n m. Dict (Min m n ~ Min n m)
+ Data.Constraint.Nat: minCommutes :: forall (n :: Nat) (m :: Nat). Dict (Min m n ~ Min n m)
- Data.Constraint.Nat: minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
+ Data.Constraint.Nat: minDistributesOverMax :: forall (n :: Nat) (m :: Nat) (o :: Nat). Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))
- Data.Constraint.Nat: minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))
+ Data.Constraint.Nat: minDistributesOverPlus :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n + Min m o) ~ Min (n + m) (n + o))
- Data.Constraint.Nat: minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
+ Data.Constraint.Nat: minDistributesOverPow1 :: forall (n :: Nat) (m :: Nat) (o :: Natural). Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))
- Data.Constraint.Nat: minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
+ Data.Constraint.Nat: minDistributesOverPow2 :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))
- Data.Constraint.Nat: minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))
+ Data.Constraint.Nat: minDistributesOverTimes :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Min m o) ~ Min (n * m) (n * o))
- Data.Constraint.Nat: minIsIdempotent :: forall n. Dict (Min n n ~ n)
+ Data.Constraint.Nat: minIsIdempotent :: forall (n :: Nat). Dict (Min n n ~ n)
- Data.Constraint.Nat: minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c)
+ Data.Constraint.Nat: minMonotone1 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b) :- (Min a c <= Min b c)
- Data.Constraint.Nat: minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c)
+ Data.Constraint.Nat: minMonotone2 :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c) :- (Min a b <= Min a c)
- Data.Constraint.Nat: minNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)
+ Data.Constraint.Nat: minNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (Min n m)
- Data.Constraint.Nat: minZero :: forall n. Dict (Min n 0 ~ 0)
+ Data.Constraint.Nat: minZero :: forall (n :: Nat). Dict (Min n 0 ~ 0)
- Data.Constraint.Nat: minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
+ Data.Constraint.Nat: minusNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)
- Data.Constraint.Nat: minusZero :: forall n. Dict ((n - 0) ~ n)
+ Data.Constraint.Nat: minusZero :: forall (n :: Natural). Dict ((n - 0) ~ n)
- Data.Constraint.Nat: modBound :: forall m n. (1 <= n) :- (Mod m n <= n)
+ Data.Constraint.Nat: modBound :: forall (m :: Natural) (n :: Natural). (1 <= n) :- (Mod m n <= n)
- Data.Constraint.Nat: modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
+ Data.Constraint.Nat: modNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)
- Data.Constraint.Nat: plusAssociates :: forall m n o. Dict (((m + n) + o) ~ (m + (n + o)))
+ Data.Constraint.Nat: plusAssociates :: forall (m :: Natural) (n :: Natural) (o :: Natural). Dict (((m + n) + o) ~ (m + (n + o)))
- Data.Constraint.Nat: plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))
+ Data.Constraint.Nat: plusCommutes :: forall (n :: Natural) (m :: Natural). Dict ((m + n) ~ (n + m))
- Data.Constraint.Nat: plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ ((n * m) + (n * o)))
+ Data.Constraint.Nat: plusDistributesOverTimes :: forall (n :: Natural) (m :: Natural) (o :: Natural). Dict ((n * (m + o)) ~ ((n * m) + (n * o)))
- Data.Constraint.Nat: plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)
+ Data.Constraint.Nat: plusIsCancellative :: forall (n :: Natural) (m :: Natural) (o :: Natural). ((n + m) ~ (n + o)) :- (m ~ o)
- Data.Constraint.Nat: plusMinusInverse1 :: forall n m. Dict (((m + n) - n) ~ m)
+ Data.Constraint.Nat: plusMinusInverse1 :: forall (n :: Natural) (m :: Natural). Dict (((m + n) - n) ~ m)
- Data.Constraint.Nat: plusMinusInverse2 :: forall n m. (m <= n) :- (((m + n) - m) ~ n)
+ Data.Constraint.Nat: plusMinusInverse2 :: forall (n :: Natural) (m :: Natural). (m <= n) :- (((m + n) - m) ~ n)
- Data.Constraint.Nat: plusMinusInverse3 :: forall n m. (n <= m) :- (((m - n) + n) ~ m)
+ Data.Constraint.Nat: plusMinusInverse3 :: forall (n :: Natural) (m :: Natural). (n <= m) :- (((m - n) + n) ~ m)
- Data.Constraint.Nat: plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
+ Data.Constraint.Nat: plusMod :: forall (a :: Natural) (b :: Natural) (c :: Natural). (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)
- Data.Constraint.Nat: plusMonotone1 :: forall a b c. (a <= b) :- ((a + c) <= (b + c))
+ Data.Constraint.Nat: plusMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a + c) <= (b + c))
- Data.Constraint.Nat: plusMonotone2 :: forall a b c. (b <= c) :- ((a + b) <= (a + c))
+ Data.Constraint.Nat: plusMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a + b) <= (a + c))
- Data.Constraint.Nat: plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)
+ Data.Constraint.Nat: plusNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n + m)
- Data.Constraint.Nat: plusZero :: forall n. Dict ((n + 0) ~ n)
+ Data.Constraint.Nat: plusZero :: forall (n :: Natural). Dict ((n + 0) ~ n)
- Data.Constraint.Nat: powMonotone1 :: forall a b c. (a <= b) :- ((a ^ c) <= (b ^ c))
+ Data.Constraint.Nat: powMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a ^ c) <= (b ^ c))
- Data.Constraint.Nat: powMonotone2 :: forall a b c. (b <= c) :- ((a ^ b) <= (a ^ c))
+ Data.Constraint.Nat: powMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a ^ b) <= (a ^ c))
- Data.Constraint.Nat: powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
+ Data.Constraint.Nat: powNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n ^ m)
- Data.Constraint.Nat: powOne :: forall n. Dict ((n ^ 1) ~ n)
+ Data.Constraint.Nat: powOne :: forall (n :: Natural). Dict ((n ^ 1) ~ n)
- Data.Constraint.Nat: powZero :: forall n. Dict ((n ^ 0) ~ 1)
+ Data.Constraint.Nat: powZero :: forall (n :: Natural). Dict ((n ^ 0) ~ 1)
- Data.Constraint.Nat: timesAssociates :: forall m n o. Dict (((m * n) * o) ~ (m * (n * o)))
+ Data.Constraint.Nat: timesAssociates :: forall (m :: Natural) (n :: Natural) (o :: Natural). Dict (((m * n) * o) ~ (m * (n * o)))
- Data.Constraint.Nat: timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))
+ Data.Constraint.Nat: timesCommutes :: forall (n :: Natural) (m :: Natural). Dict ((m * n) ~ (n * m))
- Data.Constraint.Nat: timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
+ Data.Constraint.Nat: timesDistributesOverGcd :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))
- Data.Constraint.Nat: timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
+ Data.Constraint.Nat: timesDistributesOverLcm :: forall (n :: Natural) (m :: Nat) (o :: Nat). Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))
- Data.Constraint.Nat: timesDistributesOverPow :: forall n m o. Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))
+ Data.Constraint.Nat: timesDistributesOverPow :: forall (n :: Natural) (m :: Natural) (o :: Natural). Dict ((n ^ (m + o)) ~ ((n ^ m) * (n ^ o)))
- Data.Constraint.Nat: timesDiv :: forall a b. Dict ((a * Div b a) <= b)
+ Data.Constraint.Nat: timesDiv :: forall (a :: Natural) (b :: Natural). Dict ((a * Div b a) <= b)
- Data.Constraint.Nat: timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
+ Data.Constraint.Nat: timesIsCancellative :: forall (n :: Natural) (m :: Natural) (o :: Natural). (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)
- Data.Constraint.Nat: timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
+ Data.Constraint.Nat: timesMod :: forall (a :: Natural) (b :: Natural) (c :: Natural). (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)
- Data.Constraint.Nat: timesMonotone1 :: forall a b c. (a <= b) :- ((a * c) <= (b * c))
+ Data.Constraint.Nat: timesMonotone1 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (a <= b) :- ((a * c) <= (b * c))
- Data.Constraint.Nat: timesMonotone2 :: forall a b c. (b <= c) :- ((a * b) <= (a * c))
+ Data.Constraint.Nat: timesMonotone2 :: forall (a :: Natural) (b :: Natural) (c :: Natural). (b <= c) :- ((a * b) <= (a * c))
- Data.Constraint.Nat: timesNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)
+ Data.Constraint.Nat: timesNat :: forall (n :: Nat) (m :: Nat). (KnownNat n, KnownNat m) :- KnownNat (n * m)
- Data.Constraint.Nat: timesOne :: forall n. Dict ((n * 1) ~ n)
+ Data.Constraint.Nat: timesOne :: forall (n :: Natural). Dict ((n * 1) ~ n)
- Data.Constraint.Nat: timesZero :: forall n. Dict ((n * 0) ~ 0)
+ Data.Constraint.Nat: timesZero :: forall (n :: Natural). Dict ((n * 0) ~ 0)
- Data.Constraint.Nat: type Divides n m = n ~ Gcd n m
+ Data.Constraint.Nat: type Divides (n :: Nat) (m :: Nat) = n ~ Gcd n m
- Data.Constraint.Symbol: appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))
+ Data.Constraint.Symbol: appendAssociates :: forall (a :: Symbol) (b :: Symbol) (c :: Symbol). Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))
- Data.Constraint.Symbol: appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
+ Data.Constraint.Symbol: appendSymbol :: forall (a :: Symbol) (b :: Symbol). (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)
- Data.Constraint.Symbol: appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a)
+ Data.Constraint.Symbol: appendUnit1 :: forall (a :: Symbol). Dict (AppendSymbol "" a ~ a)
- Data.Constraint.Symbol: appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a)
+ Data.Constraint.Symbol: appendUnit2 :: forall (a :: Symbol). Dict (AppendSymbol a "" ~ a)
- Data.Constraint.Symbol: drop0 :: forall a. Dict (Drop 0 a ~ a)
+ Data.Constraint.Symbol: drop0 :: forall (a :: Symbol). Dict (Drop 0 a ~ a)
- Data.Constraint.Symbol: dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a)
+ Data.Constraint.Symbol: dropDrop :: forall (n :: Nat) (m :: Nat) (a :: Symbol). Dict (Drop n (Drop m a) ~ Drop (n + m) a)
- Data.Constraint.Symbol: dropEmpty :: forall n. Dict (Drop n "" ~ "")
+ Data.Constraint.Symbol: dropEmpty :: forall (n :: Nat). Dict (Drop n "" ~ "")
- Data.Constraint.Symbol: dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "")
+ Data.Constraint.Symbol: dropLength :: forall (n :: Nat) (a :: Symbol). (Length a <= n) :- (Drop n a ~ "")
- Data.Constraint.Symbol: dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
+ Data.Constraint.Symbol: dropSymbol :: forall (n :: Nat) (a :: Symbol). (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)
- Data.Constraint.Symbol: lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n))
+ Data.Constraint.Symbol: lengthDrop :: forall (n :: Nat) (a :: Symbol). Dict (Length a <= (Length (Drop n a) + n))
- Data.Constraint.Symbol: lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a)
+ Data.Constraint.Symbol: lengthSymbol :: forall (a :: Symbol). KnownSymbol a :- KnownNat (Length a)
- Data.Constraint.Symbol: lengthTake :: forall n a. Dict (Length (Take n a) <= n)
+ Data.Constraint.Symbol: lengthTake :: forall (n :: Nat) (a :: Symbol). Dict (Length (Take n a) <= n)
- Data.Constraint.Symbol: take0 :: forall a. Dict (Take 0 a ~ "")
+ Data.Constraint.Symbol: take0 :: forall (a :: Symbol). Dict (Take 0 a ~ "")
- Data.Constraint.Symbol: takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
+ Data.Constraint.Symbol: takeAppendDrop :: forall (n :: Nat) (a :: Symbol). Dict (AppendSymbol (Take n a) (Drop n a) ~ a)
- Data.Constraint.Symbol: takeEmpty :: forall n. Dict (Take n "" ~ "")
+ Data.Constraint.Symbol: takeEmpty :: forall (n :: Nat). Dict (Take n "" ~ "")
- Data.Constraint.Symbol: takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a)
+ Data.Constraint.Symbol: takeLength :: forall (n :: Nat) (a :: Symbol). (Length a <= n) :- (Take n a ~ a)
- Data.Constraint.Symbol: takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
+ Data.Constraint.Symbol: takeSymbol :: forall (n :: Nat) (a :: Symbol). (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)
- Data.Constraint.Symbol: takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a)
+ Data.Constraint.Symbol: takeTake :: forall (n :: Nat) (m :: Nat) (a :: Symbol). Dict (Take n (Take m a) ~ Take (Min n m) a)
- Data.Constraint.Unsafe: unsafeSChar :: Char -> SChar c
+ Data.Constraint.Unsafe: unsafeSChar :: forall (c :: Char). Char -> SChar c
- Data.Constraint.Unsafe: unsafeSNat :: Natural -> SNat n
+ Data.Constraint.Unsafe: unsafeSNat :: forall (n :: Nat). Natural -> SNat n
- Data.Constraint.Unsafe: unsafeSSymbol :: String -> SSymbol s
+ Data.Constraint.Unsafe: unsafeSSymbol :: forall (s :: Symbol). String -> SSymbol s
Files
- CHANGELOG.markdown +4/−0
- constraints.cabal +8/−6
- src/Data/Constraint.hs +0/−1
- src/Data/Constraint/Deferrable.hs +2/−4
CHANGELOG.markdown view
@@ -1,3 +1,7 @@+0.14.3 [2026.01.10]+-------------------+* Remove unused `ghc-prim` dependency.+ 0.14.2 [2024.05.12] ------------------- * Re-export `Log2` from `Data.Constraint.Nat`.
constraints.cabal view
@@ -1,7 +1,7 @@ cabal-version: 2.4 name: constraints category: Constraints-version: 0.14.2+version: 0.14.3 license: BSD-2-Clause license-file: LICENSE author: Edward A. Kmett@@ -19,9 +19,12 @@ build-type: Simple tested-with:- GHC == 9.8.1- GHC == 9.6.3- GHC == 9.4.7+ GHC == 9.14.1+ GHC == 9.12.2+ GHC == 9.10.3+ GHC == 9.8.4+ GHC == 9.6.7+ GHC == 9.4.8 GHC == 9.2.8 GHC == 9.0.2 GHC == 8.10.7@@ -56,8 +59,7 @@ , binary >= 0.7.1 && < 0.9 , boring >= 0.2 && < 0.3 , deepseq >= 1.3 && < 1.6- , ghc-prim- , hashable >= 1.2 && < 1.5+ , hashable >= 1.2 && < 1.6 , mtl >= 2.2 && < 2.4 , transformers >= 0.5 && < 0.7 if !impl(ghc >= 9.0)
src/Data/Constraint.hs view
@@ -110,7 +110,6 @@ -- data Dict :: Constraint -> * where Dict :: a => Dict a- deriving Typeable deriving stock instance (Typeable p, p) => Data (Dict p) deriving stock instance Eq (Dict a)
src/Data/Constraint/Deferrable.hs view
@@ -1,6 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-}@@ -33,11 +32,10 @@ import Data.Typeable (Typeable, cast, typeRep) import Data.Type.Equality ((:~:)(Refl)) -import GHC.Types (type (~~))-import Data.Type.Equality ((:~~:)(HRefl))+import Data.Type.Equality (type (~~), (:~~:)(HRefl)) newtype UnsatisfiedConstraint = UnsatisfiedConstraint String- deriving (Typeable, Show)+ deriving Show instance Exception UnsatisfiedConstraint