9

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.

Asad Saeeduddin
  • 46,193
  • 6
  • 90
  • 139
  • does this answer your question https://stackoverflow.com/questions/56470600/quantified-constraints-vs-closed-type-families – Li-yao Xia Jul 20 '20 at 12:34
  • @Li-yaoXia If there's an answer to my question in there, I can't see it. As far as I can tell the setting of the two problems is different, because I have a constraint-valued type family applied to a naked type parameter (with no type-valued type families involved), whereas in the other question they are using a standard class applied to the result of a type-valued type family. Maybe this is a red herring though, i don't really know. – Asad Saeeduddin Jul 20 '20 at 13:16
  • I see, yes, that seems like a different situation, though the take away ends up the same: quantified constraints and type families don't mix; some indirection is necessary. I think your specific question (explaining this behavior) can only be answered by someone who understands the implementation, so you're better off asking on the mailing lists or on GHC's issue tracker. – Li-yao Xia Jul 20 '20 at 13:42
  • 1
    Please update your GHC: quantified constraints are a new feature and lots of fixes are being applied. The issue is actually just that `forall x y. (TheFamily t x, TheFamily t y) => TheFamily t (t x y)` isn't allowed in the first place, so it doesn't matter that it doesn't work properly. GHC 8.10.1 complains "Quantified predicate must have a class or type variable head". Your GHC seems to lack this check. I'm voting to close. – HTNW Jul 21 '20 at 01:14
  • Actually, it looks like 8.10.1 rejects `foo` with that error but accepts `foo'`. – K. A. Buhr Jul 21 '20 at 21:31

0 Answers0