Stack Overflow Asked by Asad Saeeduddin on November 20, 2021
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, TheFamily t y) => TheFamily t (t x y))
, TheFamily t a
, TheFamily t b
) => Dict (TheFamily t (t a b))
foo = Dict
-- NB: Only using `Dict` to assert that the relevant constraint is satisfied in the body of `foo`
produces the error:
• Could not deduce: TheFamily t (t a b)
arising from a use of ‘Dict’
from the context: (TheClass t,
forall x y. (TheFamily t x, TheFamily t y) => TheFamily t (t x y),
TheFamily t a, TheFamily t b)
bound by the type signature for:
foo :: forall (t :: * -> * -> *) a b.
(TheClass t,
forall x y. (TheFamily t x, TheFamily t y) => TheFamily t (t x y),
TheFamily t a, TheFamily t b) =>
Dict (TheFamily t (t a b))
but the following seemingly trivial modification to foo
:
foo' :: forall t a b temp.
( TheClass t
, TheFamily t ~ temp
, (forall x y. (temp x, temp y) => temp (t x y))
, TheFamily t a
, TheFamily t b
) => Dict (TheFamily t (t a b))
foo' = Dict
makes the compiler happy?
Shouldn’t the two snippets be equivalent? All I’m doing is aliasing TheFamily t
as some other temporary type variable using an equality constraint.
Get help from others!
Recent Answers
Recent Questions
© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP