Questions tagged [quantified-constraints]
16 questions
11
votes
2 answers
Quantified constraints vs. (closed) type families
I am trying to use this blogpost's approach to higher-kinded data without dangling Identity functors for the trival case together with quantified-constraint deriving:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints,…
Cactus
- 27,075
- 9
- 69
- 149
9
votes
0 answers
Interaction between associated type families and quantified constraints
Why is it that the following code:
class TheClass (t :: * -> * -> *)
where
type TheFamily t :: * -> Constraint
data Dict (c :: Constraint)
where
Dict :: c => Dict c
foo :: forall t a b.
( TheClass t
, (forall x y. (TheFamily t x,…
Asad Saeeduddin
- 46,193
- 6
- 90
- 139
9
votes
1 answer
Derive Ord with Quantified Constraints (forall a. Ord a => Ord (f a))
With quantified constraints I can derive Eq (A f) just fine? However, when I try to derive Ord (A f) it fails. I do not understand how to use quantified constraints when the constraint class has a superclass. How do I derive Ord (A f) and other…
William Rusnack
- 908
- 8
- 15
7
votes
3 answers
haskell -- rank n constraints? (or, monad transformers and Data.Suitable)
I'm trying to write something that appears to be analagous to "rank 2 types", but for constraints instead. (Or, maybe it's not correct to assume changing -> in the definition of "rank 2 types" to => is meaningful; please edit the question if you…
gatoatigrado
- 16,580
- 18
- 81
- 143
7
votes
3 answers
Can adding a constraint cause other constraints to go out of scope?
Consider the following code, which typechecks:
module Scratch where
import GHC.Exts
ensure :: forall c x. c => x -> x
ensure = id
type Eq2 t = (forall x y. (Eq x, Eq y) => Eq (t x y) :: Constraint)
foo :: forall t a.
( Eq2 t
, Eq a
) =>…
Asad Saeeduddin
- 46,193
- 6
- 90
- 139
6
votes
1 answer
Change in Behaviour of Quantified Constraints in GHC 9
Previously, in order to use quantified constraints on typeclasses like Ord, you had to include the superclass in the instance like so:
newtype A f = A (f Int)
deriving instance (forall a. Eq a => Eq (f a)) => Eq (A f)
deriving instance (forall a. Eq…
oisdk
- 9,763
- 4
- 18
- 36
5
votes
1 answer
Instance inductivity as constraint
I'm trying to express an idea that given
instance (MonadTrans t, MonadX m) => MonadX (t m)
it should follow, that any t1 (t2 ... (tn m)) is also MonadX as long as all tx have MonadTrans instance. However when i try to write it down it doesn't…
Ryba
- 681
- 4
- 13
5
votes
2 answers
How can I derive typeclass instances from constraint families that are in scope?
edit: I have followed up with a more specific question. Thank you answerers here, and I think the followup question does a better job of explaining some confusion I introduced here.
TL;DR I'm struggling to get proofs of constraints into…
Josh.F
- 3,666
- 2
- 27
- 37
5
votes
1 answer
Why is using QuantifiedConstraints to specify a subclass of a typeclass also demanding an instance of the subclass?
I'm playing around with a multikinded tagless encoding of Free
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds…
rampion
- 87,131
- 49
- 199
- 315
4
votes
3 answers
Quantified Constraints for Higher-kinded Typeclasses
Suppose I would like to write two Typeclasses.
Header:
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Complex
The first typeclass ExClass was defined as such:
class (forall a. (Monoid (t a))) => ExClass t…
w41g87
- 79
- 4
3
votes
1 answer
How can I use a Constraint Family that's in scope to prove instances within the body of an expression?
This is a follow up to my previous question. I recieved some good answers there, but, because of the way I simplified my actual problem, I think I misled the answerers, and I hope to remedy that here.
TL;DR I have a typeclass Category from…
Josh.F
- 3,666
- 2
- 27
- 37
3
votes
1 answer
How to give GHC a hint for constructing QuantifiedConstraints?
If I have the method:
proveBar :: forall x . SingI x => Dict (Barable (Foo x))
proveBar = ...
Then how do I pass this as the context to:
useBar :: forall foo . (forall x. SingI x => Barable (foo x)) => ...
useBar = ...
binding foo to Foo
?
Dict…
dspyz
- 5,280
- 2
- 25
- 63
2
votes
1 answer
Why does this usage of quantified constraints fail to compile:
Consider the following:
{-# LANGUAGE QuantifiedConstraints #-}
data SomeMaybe c t where
SomeNothing :: SomeMaybe c t
SomeJust :: c t => t -> SomeMaybe c t
instance (forall b. c b => Semigroup b) => Semigroup (SomeMaybe c u) where
x <> y =…
Clinton
- 22,361
- 15
- 67
- 163
1
vote
1 answer
Quantified type equality of associated type families
I have an associated type family Bar in a type class Foo. Foo' requires that Bar f ~ Bar (f a) for all a, but in another function test I get an error Couldn't match type 'Bar f' with 'Bar (f a)', even though it depends on Foo' f. The code:
{-#…
Greg C
- 75
- 1
- 4
1
vote
2 answers
Letting a distributed DSL implementation choose its serialization format (via constraint family)
I'm writing a distributed programming DSL and I'd like to allow implementations to choose their serialization method (if any, as it might not even be needed for a simulated execution).
Trying to solve this by adding a type family led to the problem…
æons
- 53
- 4