[Haskell-cafe] Existential type variables in constraints

CASANOVA Juan Juan.Casanova at ed.ac.uk
Fri Apr 2 12:54:37 UTC 2021


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/ce40c190/attachment.html>


More information about the Haskell-Cafe mailing list