On Wed, Jan 02, 2013 at 08:23:37PM +0000, Simon Peyton-Jones wrote:

| > The solution is to add (EuclideanRing k) to the type sig of cubicExt. | > Then it compiles all the way up to the top. | | But the DoCon declares | class (EuclideanRing a, FactorizationRing a) => Field a | | (EuclideanRing is a superclass for Field), | and the test declares | cubicExt :: (Field k, FactorizationRing (UPol k)) => | k -> k -> Domains1 k -> (Domains1 (E k), [E k], k -> E k) | | So, why the compiler does not `extract' EuclideanRing k from Field k

I made a mistake. I should have said "add (EuclideanRing (Pol k)) to the type sig of cubicExt".

GHC can't extract EuclideanRing (Pol k) from Field k except by using one of the two (overlapping) instances.

I don't know why 7.4 accepts it, but I'm not inclined to investigate... looks like a bug in 7.4.

ghc-7.4.1 may use a special trick, but is correct.

I should have said "add (EuclideanRing (Pol k)) to the type sig of cubicExt".

(1) UPol is for an Univariate Polynomial, and Pol is for an Multivariate Polynomial (more generic). (2) DoCon declares Field k => EuclideanRing (UPol k). (3) DoCon does not have the instance Field k => EuclideanRing (Pol k), because it is not correct in algebra. Haskell+Glasgow can not derive EuclideanRing (Pol k) from Field k in the DoCon code. (4) In cubicExt, Haskell+Glasgow derives a weaker instances: LinSolvRing (Pol k), LinSolvRing (Pol (UPol k)), LinSolvRing (UPol (Pol k)) -- and this is sufficient. This is the intension of DoCon + cubicExt, and ghc-7.4.1 supports this (may be, by some tricky designп, I do not know). (5) I can add EuclideanRing (UPol k) to the sig of cubicExt (even though Haskell+Glasgow must derive it), but I expect that this would not help. (6) I can not add EuclideanRing (Pol k) to the sig of cubicExt, because this is not correct by the algebraic design. cubicExt indeed uses rather a complicated set of instances. I do not know, may be I need to think of how to reorganize the design for porting it to ghc-7.6.2. ghc-7.4.1 did the job correctly, and it is difficult to change the coresponding part of the DoCon design. And if you happen to find how to meet (1) -- (6), then I would not need to re-design the thing. Regards, ------ Sergei

On Wed, Jan 02, 2013 at 11:27:15PM +0000, Simon Peyton-Jones wrote:

I made a second mistake. I meant (LinSolvRing (UPol k)). Apologies.

| > I don't know why 7.4 accepts it, but I'm not inclined to investigate... | > looks like a bug in 7.4. | | ghc-7.4.1 may use a special trick, but is correct.

I don't understand your explanation. What is wrong with this reasoning?

1. The call to upEucRing in cubicExt gives rise the constraint (LinSolvRing (UPol k)) Corect?

2. There are two overlapping instances for (LinSolvRing (UPol k)), defined in UPol2_ and UPol3_ Correct?

3. So GHC cannot solve the constraint using an instance declaration. Correct?

4. The type signature provides (Field k, FactorizationRing (UPol k)) but neither is enough to satisfy LinSolvRing (UPol k). Correct?

5. Therefore we must add LinSolvRing (UPol k) to the signature.

If you believe that the function should typecheck as-is, please explain how to deduce (LinSolvRing (UPol k)) from (Field k, FactorizationRing (UPol k)).

1. I try adding `, LinSolvRing (UPol k)' to the sig of cubeExt. Now, ghc-7.6.1.20121207 builds docon-2.12 but does not compile the demonstration of T_cubeext.hs (where cubicExt is) -- with {-# LANGUAGE ScopedTypeVariables, MonoLocalBinds #-} prepended to the module. Can you, please, reproduce this in ghc-7.6.1.20121207 ? Because a) the problem is in porting to a fresh stable GHC version, b) ghc-7.6.1.20121207 is announced to become a fresh ghc-7.6.2, and it asks for testing, c) if I use an older version, then, why, I could simply remain with ghc-7.4.1. 2. Now suppose that a fresh GHC is fixed, and the point (1) works. Adding `, LinSolvRing (UPol k)' is not an error. But is an awkward algebraic statement. For example, one can formulate "for all integer p > 2 such that p is prime and p is odd, it holds Foo(p)". Adding "and p is odd" is not an error, but looks awkward, because it is derived from (p > 2, p is prime) according to previous theory. This reduces redability of the text, because the reader starts to think that he is missing something subtle. Similarly, LinSolvRing (UPol k) is derived in cubicExt from cubicExt and from the proper DoCon. The matter is that the algorithm (instance) for this LinSolvRing (UPol k) is derived in multiple ways -- overlapping instances. 3. For this particular case, I agree to tell to GHC: "choose any derivation way you like". Because a) I know that the needed final result part does not depend on this choice (even though the algoritms differ), b) the cost difference will not be great. How can I tell this to GHC -- with respect to only this function signature, or maybe, only to this module ? 4. Probably, the rule of the substitutional instance specialization in Haskell+Glasgow is not enough to follow algebra. Why not give the user an additional way to choose the derivation? For example, let there be the instances I, II, III, IV, and the instance (Foo T) is derived from I, II, III, IV in multiple ways. The programmer writes the signature f :: (..., (Foo T, using {II, III}, notUsing {I, IV})) => ... which means to consider for (Foo T) only those derivations which use {II, III} and do not use {I, IV}. I do not know, may be I am missing something. 5. Now, I specify how LinSolvRing (UPol k) is derived in the existing Haskell+Glasgow language. DoCon = Proper-DoCon + demo; cubicExt is a part of demo. First, Proper-DoCon is installed -- this works. And cubicExt is not compiled. Proper-DoCon includes: GCDRing a and EuclideanRing a are superclasses for Field a, (I) class (GCDRing a, LinSolvRing a) => EuclideanRing a where ... (II) instance GCDRing a => GCDRing (UPol a) where ... (III) instance Field k => EuclideanRing (UPol k) where ... (IV) instance EuclideanRing a => LinSolvRing (UPol a) where ... (V) (in Pol2_.hs) Each of these has a very useful algebraic meaning. Now, GHC starts to compile cubicExt. And there Field k => LinSolvRing (UPol k) is derived from I -- V in at least two ways, and may be there are even more of them. Algebraically, these overlaps are all right, they are in the nature, these derivations give equivalent results. But one may insist: "choose the way, because the algorithms are different, and the computation cost may differ". For example, for Field k => LinSolvRing (UPol k), I would choose this way: "Field k is declared. Euclidean is a superclass for Field by (I). hence there is the instance Euclidean k. hence there is the instance LinSolvRing (UPol k) by V with a := k. " And Haskell+Glasgow sees this derivation surely. In the algebra textbooks it is expressed like this: "k is a Field, hence it is EuclideanRing, hence, by V, (UPol k) is LinSolvRing." Other ways I consider as algorithmically parasitic. They appear by GHC composing I -- V in various combinations. I am forced to write I -- V, because each of them is useful by itself in various situations; this is in the nature of algebra. On the other hand, I have not enough language constructs to cut out (for GHC) the combinations that are parasitic -- with respect to the computational cost choice. Here is another derivation for Field k => LinSolvRing (UPol k). Repeat the state: GCDRing a and EuclideanRing a are superclasses for Field a, (I) class (GCDRing a, LinSolvRing a) => EuclideanRing a where ... (II) instance GCDRing a => GCDRing (UPol a) (III) instance Field k => EuclideanRing (UPol k) (IV) instance EuclideanRing a => LinSolvRing (UPol a) (V) (in Pol2_.hs) The derivation is: Field k is given. EuclideanRing (UPol k) is by IV. LinSolvRing a is a superclass for EuclideanRing a by II. Hence, with a := UPol k, there must presense the instance LinSolvRing (UPol k), such an instance must precede IV in order IV to be compiled. And GHC finds the instance for LinSolvRing (UPol k). For example, it is by V with a := k. And it occurs that the first derivation is a part of the second one. I do not know how many derivations exist, and whether GHC ignores the second one. But at least I have answered to the question

If you believe that the function should typecheck as-is, please explain how to deduce (LinSolvRing (UPol k)) from (Field k, FactorizationRing (UPol k)).

I have presented the two derivations, the first one looks natural.

I don't understand your explanation. What is wrong with this reasoning?

1. The call to upEucRing in cubicExt gives rise the constraint (LinSolvRing (UPol k)) Corect?

Yes. It gives rise to EuclideanRing (UPol k). And LinSolvRing a is a superclass for EuclideanRing a. And the constraint of EuclideanRing (UPol k) follows from the call to upEucRing in cubicExt and from the declaration upEucRing :: EuclideanRing a => ADomDom a in Ring_0.hs. Because cubicExt applies upEucRing with a = (Field k, ...) => UPol k The condition of EuclideanRing (UPol k) is satisfied by the following declarations in DoCon (not in the demonstration program): GCDRing a and EuclideanRing a are superclasses for Field a, (I) class (GCDRing a, LinSolvRing a) => EuclideanRing a (II) instance GCDRing a => GCDRing (UPol a) (III) instance Field k => EuclideanRing (UPol k) (IV) instance EuclideanRing a => LinSolvRing (UPol a) (V) (in Pol2_.hs) So, Field k => EuclideanRing (UPol k) follows by IV and also by V & III & I (I find this way only now).

2. There are two overlapping instances for (LinSolvRing (UPol k)), defined in UPol2_ and UPol3_ Correct?

a) DoCon has not UPol2_.hs nor UPol3_.hs. It has Pol2_.hs and Pol3_.hs. (And for any occasion: as I wrote earlier, the data costructors Pol and UPol have different meaning and different instance sets ). b) I have shown the two derivations for Field k => LinSolvRing (UPol k) (the second one in strange, because it is included in the first). May be, there exists some more clear overlap. instance EuclideanRing a => LinSolvRing (UPol a) of Pol_2.hs is used in the first derivation. c) Pol3_ has instance (LinSolvRing (Pol a), CommutativeRing a) => LinSolvRing (UPol (Pol a)) But this does not overlap with I -- V, in particular, not with Field k => LinSolvRing (UPol k). Because Pol a is never of a Field nor of EuclideanRing. And Hashell+Glasgow sees this.

3. So GHC cannot solve the constraint using an instance declaration. Correct?

GHC finds multiple solutions for this constraint. Several instances overlap. Each of these derivations is algebraically correct. I do not know of whether this overlap is resolved by the rules of the Haskell+Glasgow language. Also ghc-7.4.1 says it resolves them (at least, the demo program works correct), and ghc-7.6.1.20121207 does not resolve.

4. The type signature provides (Field k, FactorizationRing (UPol k)) but neither is enough to satisfy LinSolvRing (UPol k). Correct?

No. LinSolvRing (UPol k) is derived by Haskell+Glasgow from Field k. See above my explanation. But it is derived in multiple ways.

5. Therefore we must add LinSolvRing (UPol k) to the signature.

This is not an error. But ghc-7.6.1.20121207 does not compile this. Also see the beginning of my part of this letter.

If you believe that the function should typecheck as-is, please explain how to deduce (LinSolvRing (UPol k)) from (Field k, FactorizationRing (UPol k)).

I have shown this above. The GHC problem is that most probably, it is deduced in multiple ways. At least, it is now desirable the following: to make ghc-7.6.1.20121207 to compile your variant with adding LinSolvRing (UPol k) to the signature. Do you agree with this single point? Regards, ------ Sergei

On Thu, Jan 3, 2013 at 4:57 AM, Simon Peyton-Jones wrote:

When matching instances, GHC does not take account of the context of the instance. Say you have

data T a = ... data S1 = ... data S2 = ... [a] instance Num a => Num (T a) where ... [b] instance Show a => Num (T a) where ... instance Num S1

and suppose you need an instance of (Num (T S1)). Then although [a] and [b] overlap, you might say we should use [a], since S1 is an instance of Num, but not an instance of Show. But GHC does not do this. It matches instances only based on the bit after the "=>".

It seems you're making GHC seem more capricious than it is here. Even were GHC to consider contexts in instance selection, the choice of [a] over [b] would still be incoherent: the compiler has no way to prove that there is no later instance adding S1 to class Show. Indeed, the S1's and S2's are in some sense not relevant: because Haskell provides no mechanism to exclude types from classes, there is no way to ever coherently use instance [a] or [b], regardless of the argument to T. /g -- Sent from my mail client.