TransWikia.com

Interaction between associated type families and quantified constraints

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.

Add your own answers!

Ask a Question

Get help from others!

© 2024 TransWikia.com. All rights reserved. Sites we Love: PCI Database, UKBizDB, Menu Kuliner, Sharing RPP