[Haskell-cafe] Existential type variables in constraints

[CASANOVA Juan]

Just for the record, the question still remains, but as usual, after I sent the question I realized the general ballpark in which the answer may end up being.

When doing:

instance (forall b. (Ord a, Ord b)) => Class1 a where
  fun1 = (<)

While in this case there are no functional dependencies, it is possible in principle that (Ord a, Ord b) produces a functional dependency between a and b, which would make the specific "a" a function of whatever "b" is, and since "b" is existentially quantified, then "a" would also be dependent on the specific type it ended up being instantiated to. Is this what's going on? In order to do this, undecidable things like exploring all the possible combinations of functional dependencies would need to be explored by the compiler?

Even if this was exactly the problem, I would still be very happy to hear ideas on how to deal with this without having to manually write down all of the constraints that do not include a specific type variable.

Thanks again.
________________________________
From: CASANOVA Juan
Sent: 02 April 2021 13:54
To: YueCompl via Haskell-Cafe <haskell-cafe at haskell.org>
Subject: Existential type variables in constraints

Hello again,

Here with more type class issues.

As usual, assume all extensions required. But here I am going to be explicit, because UndecidableInstances is definitely required for this and I know it's a problematic one. These may be excessive, but with these extensions this should work:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds #-}

My "problem" is I want (almost need) existentially quantified types in constraints. The reason is that I have lots, lots and lots of constraints over up to 10 type variables (multi-parameter type classes in most cases, with complex functional dependencies), which are trickled down over multiple layers of functions over multiple modules. So what I do is I define some global type synonyms that combine families of these constraints, usually the ones that are used in a specific module. Something like:

type ModuleAConstraints a b c d = (Ord a, Ord b , Ord c, Class1 a b, Class2 a [c], Class3 [(c,a)] (a -> d [b]))

(the specific constraints are made up, mine are much more and more complicated, but you get the idea of the liberality of the constraints)

Now, what happens is that in one of the highest-level modules, some of the type variables begin to disappear because they are only used internally in the lower-level modules. The functional dependencies ensure that, once I instantiate the remaining type variables, those type variables will have only one possible result, for which I will have an implemented instance.

But my type synonyms include them, and I need them to use the lower-level functions.

No problem, you can have existentially quantified variables in constraints. For example, this works:

class Class1 a where
   fun1 :: a -> a -> Bool

instance (Ord a, forall b. Ord b) => Class1 a where
  fun1 = (<)

You can also do this with type synonyms and group constraints into pairs. For example, the two following equivalent alternatives work (same definition of Class1):

1:
instance (Ord a, forall b c. (Ord b, Ord c)) => Class1 a where
  fun1 = (<)

2:
type CType b c = (Ord b, Ord c)
instance (Ord a, forall b c. CType b c) => Class1 a where
  fun1 = (<)

But, it seems, any constraints under the existentially quantifier that only utilize non-quantified variables seems to be completely overlooked by the compiler. As such, the following two equivalent alternatives both fail to type check, telling me that it cannot deduce (Ord a):

3:
instance (forall b. (Ord a, Ord b)) => Class1 a where
  fun1 = (<)

4:
type CType a b = (Ord a, Ord b)
instance (forall b. CType a b) => Class1 a where
  fun1 = (<)



Is there a good reason for this? It could be a good reason in the sense of: The deduction would be incorrect; or a good reason in the sense of: The compiler would need to do undecidable things to be able to deduce that in general. But right now I cannot see a reason. I honestly cannot see how it could be hard for the compiler to realize that

instance (Ord a, forall b. Ord b) => Class1 a where
  fun1 = (<)

and

instance (forall b. (Ord a, Ord b)) => Class1 a where
  fun1 = (<)

are equivalent. But it doesn't.

Also, is there any way I can make this work? Right now, the only option I can see is to manually re-enumerate all of the constraints that do not include the quantified variable and use that. I guess I can do that and it would only take around an hour... but what a boring and tedious hour, and to be fair I was going to stop for today anyway so I thought I'd throw the question on Haskell Cafe. I hope that's okay 🙂.

Thanks in advance as usual.
Juan Casanova.
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210402/38229af8/attachment.html>