<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
Hello again,</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
Here with more type class issues.<br>
<br>
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:<br>
<br>
{-# LANGUAGE MultiParamTypeClasses #-}
<div>{-# LANGUAGE FunctionalDependencies #-}</div>
<div>{-# LANGUAGE FlexibleInstances #-}</div>
<div>{-# LANGUAGE UndecidableInstances #-}</div>
<div>{-# LANGUAGE TypeSynonymInstances #-}</div>
<div>{-# LANGUAGE RankNTypes #-}</div>
<div>{-# LANGUAGE KindSignatures #-}</div>
<div>{-# LANGUAGE ScopedTypeVariables #-}</div>
<div>{-# LANGUAGE QuantifiedConstraints #-}</div>
<div>{-# LANGUAGE FlexibleContexts #-}</div>
<div>{-# LANGUAGE LiberalTypeSynonyms #-}</div>
<div>{-# LANGUAGE ExistentialQuantification #-}</div>
{-# LANGUAGE ConstraintKinds #-}<br>
</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
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:<br>
<br>
type ModuleAConstraints a b c d = (Ord a, Ord b , Ord c, Class1 a b, Class2 a [c], Class3 [(c,a)] (a -> d [b]))<br>
<br>
(the specific constraints are made up, mine are much more and more complicated, but you get the idea of the liberality of the constraints)<br>
<br>
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.<br>
<br>
But my type synonyms include them, and I need them to use the lower-level functions.<br>
<br>
No problem, you can have existentially quantified variables in constraints. For example, this works:<br>
<br>
class Class1 a where
<div>   fun1 :: a -> a -> Bool</div>
<div><br>
</div>
<div></div>
instance (Ord a, forall b. Ord b) => Class1 a where<br>
  fun1 = (<)<br>
<br>
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):<br>
<br>
1:<br>
instance (Ord a, forall b c. (Ord b, Ord c)) => Class1 a where</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
  fun1 = (<)<br>
<br>
2:<br>
type CType b c = (Ord b, Ord c)
<div>instance (Ord a, forall b c. CType b c) => Class1 a where</div>
  fun1 = (<)<br>
<br>
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):<br>
<br>
3:<br>
instance (forall b. (Ord a, Ord b)) => Class1 a where</div>
<div style="font-family: Calibri, Arial, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
  fun1 = (<)<br>
<br>
4:<br>
type CType a b = (Ord a, Ord b)
<div>instance (forall b. CType a b) => Class1 a where</div>
  fun1 = (<)<br>
<br>
<br>
<br>
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<br>
<br>
instance (Ord a, forall b. Ord b) => Class1 a where<br>
  fun1 = (<)<br>
<br>
and<br>
<br>
<span style="font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">instance (forall b. (Ord a, Ord b)) => Class1 a where</span><br>
<span style="font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">  fun1 = (<)</span><br>
<br>
are equivalent. But it doesn't.<br>
<br>
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
<span id="🙂">🙂</span>.<br>
<br>
Thanks in advance as usual.<br>
Juan Casanova.<br>
</div>
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.
</body>
</html>