[commit: ghc] wip/T11067: Wibbles (60e4a58)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/T11067
Link       : http://ghc.haskell.org/trac/ghc/changeset/60e4a5860773ed0030131141a98aa3d30a6a894f/ghc

>---------------------------------------------------------------

commit 60e4a5860773ed0030131141a98aa3d30a6a894f
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri Nov 27 17:45:43 2015 +0000

    Wibbles


>---------------------------------------------------------------

60e4a5860773ed0030131141a98aa3d30a6a894f
 compiler/typecheck/TcTyDecls.hs                    | 64 ++++++++--------------
 .../tests/indexed-types/should_compile/T10318.hs   | 35 ++++++++++++
 testsuite/tests/indexed-types/should_compile/all.T |  1 +
 3 files changed, 59 insertions(+), 41 deletions(-)

diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 3813d5f..080808d 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -165,48 +165,30 @@ exmaple, is fine
 even though C's full definition uses C.
 
 Making the check static also makes it conservative.  Eg
+  type family F a
+  class F a => C a
+Here an instance of (F a) might mention C:
+  type instance F [a] = C a
+and now we'd have a loop.
+
+The static check works like this, starting with C
+  * Look at C's superclass predicates
+  * If any is a type-function application, fail
+  * If any has C at the head, fail
+  * If any has a type class D at the head,
+    make the same test with D
+
+A tricky point is: what if there is a type variable at the head:
   class f a => C f a
-  class C a => D a
-Here if we produced a constraint (C D a), then its
-superclass would be (D a)
-
-
-We want definitions such as:
-
-  class C cls a where cls a => a -> a
-  class C D a => D a where
-
-to be accepted, even though a naive acyclicity check would reject the
-program as having a cycle between D and its superclass.  Why? Because
-when we instantiate
-     D ty1
-we get the superclas
-     C D ty1
-and C has no superclasses, so we have terminated with a finite set.
-
-More precisely, the rule is this: the superclasses sup_C of a class C
-are rejected iff:
-
-  C \elem expand(sup_C)
-
-Where expand is defined as follows:
-
-(1)  expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
-
-(2)  expand(D ty1 ... tyN) = {D}
-                             \union sup_D[ty1/x1, ..., tyP/xP]
-                             \union expand(ty(P+1)) ... \union expand(tyN)
-           where (D x1 ... xM) is a class, P = min(M,N)
-
-(3)  expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
-        where T is not a class
-
-Eqn (1) is conservative; when there's a type variable at the head,
-look in all the argument types.  Eqn (2) expands superclasses; the
-third component of the union is like Eqn (1).  Eqn (3) happens mainly
-when the context is a (constraint) tuple, such as (Eq a, Show a).
-
-Furthermore, expand always looks through type synonyms.
+Can this loop with some instantation of C? Well, no. You might try
+  C C a
+to instantiate 'f' with 'C', but that's ill kinded.  So what about
+  C (C ?) a
+To make it loop you'd need an infinte thing
+  C (C (C ... )) a
+
+So I don't think we can make a loop through a type variable in
+the head.
 -}
 
 checkClassCycles :: Class -> Maybe SDoc
diff --git a/testsuite/tests/indexed-types/should_compile/T10318.hs b/testsuite/tests/indexed-types/should_compile/T10318.hs
new file mode 100644
index 0000000..04a2ca1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T10318.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE FlexibleContexts, TypeSynonymInstances,
+             FlexibleInstances, TypeFamilies,
+             UndecidableSuperClasses #-}
+
+module T10318 where
+
+-- | Product of non-zero elements always non-zero.
+-- Every integral domain has a field of fractions.
+-- The field of fractions of any field is itself.
+class (Frac (Frac a) ~ Frac a, Fractional (Frac a), IntegralDomain (Frac a))
+  => IntegralDomain a where
+  type Frac a :: *
+  embed :: a -> Frac a
+
+instance IntegralDomain Integer where
+  type Frac Integer = Rational
+  embed = fromInteger
+
+instance IntegralDomain Rational where
+  type Frac Rational = Rational
+  embed = id
+
+g :: IntegralDomain a => a -> a
+g x = g x
+
+h :: a -> Frac a
+h x = h x
+
+-- This is the test function
+
+f :: IntegralDomain a => a -> Frac a
+f x = g (h (h x))
+  -- Given: IntegralDomain (Frac a)
+  -- Wanted: IntegralDomain (Frac (Frac a))
+
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 39b8a3a..7eea00e 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -265,3 +265,4 @@ test('T10753', normal, compile, [''])
 test('T10806', normal, compile_fail, [''])
 test('T10815', normal, compile, [''])
 test('T10931', normal, compile, [''])
+test('T10318', normal, compile, [''])