Check for type families in an instance context

This patch adds a check for type families to the instance-decl
termination check.  See Note [Type families in instance contexts]
and Trac #15172.

5 files changed, 32 insertions, 2 deletions

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index bdda6cd455..35e6a956f3 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1405,8 +1405,10 @@ checkInstTermination tys theta
 
    check2 pred pred_size
      | not (null bad_tvs)     = addErrTc (noMoreMsg bad_tvs what)
+     | not (isTyFamFree pred) = addErrTc (nestedMsg what)
      | pred_size >= head_size = addErrTc (smallerMsg what)
      | otherwise              = return ()
+     -- isTyFamFree: see Note [Type families in instance contexts]
      where
         what    = text "constraint" <+> quotes (ppr pred)
         bad_tvs = fvType pred \\ head_fvs
@@ -1432,7 +1434,18 @@ undecidableMsg, constraintKindsMsg :: SDoc
 undecidableMsg     = text "Use UndecidableInstances to permit this"
 constraintKindsMsg = text "Use ConstraintKinds to permit this"
 
-{-
+{- Note [Type families in instance contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Are these OK?
+  type family F a
+  instance F a    => C (Maybe [a]) where ...
+  intance C (F a) => C [[[a]]]     where ...
+
+No: the type family in the instance head might blow up to an
+arbitrarily large type, depending on how 'a' is instantiated.
+So we require UndecidableInstances if we have a type family
+in the instance head.  Trac #15172.
+
 Note [Associated type instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We allow this:
diff --git a/testsuite/tests/indexed-types/should_fail/T15172.hs b/testsuite/tests/indexed-types/should_fail/T15172.hs
new file mode 100644
index 0000000000..da7a8f80f2
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T15172.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies, ConstraintKinds, FlexibleInstances #-}
+module ShouldFail where
+
+import GHC.Exts( Constraint )
+
+type family F a :: Constraint
+
+class C a where
+
+-- Should be rejected because of the type family
+instance (F a) => C [[a]] where
diff --git a/testsuite/tests/indexed-types/should_fail/T15172.stderr b/testsuite/tests/indexed-types/should_fail/T15172.stderr
new file mode 100644
index 0000000000..8c28c5148c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T15172.stderr
@@ -0,0 +1,5 @@
+
+T15172.hs:11:10: error:
+    • Illegal nested constraint ‘F a’
+      (Use UndecidableInstances to permit this)
+    • In the instance declaration for ‘C [[a]]’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 4d25d970b9..61025d6c92 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -141,3 +141,4 @@ test('T14033', normal, compile_fail, [''])
 test('T14045a', normal, compile_fail, [''])
 test('T14175', normal, compile_fail, [''])
 test('T14369', normal, compile_fail, [''])
+test('T15172', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail214.stderr b/testsuite/tests/typecheck/should_fail/tcfail214.stderr
index c6a4387142..83fa344834 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail214.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail214.stderr
@@ -1,5 +1,5 @@
 
 tcfail214.hs:9:10: error:
-    • The constraint ‘F a’ is no smaller than the instance head
+    • Illegal nested constraint ‘F a’
       (Use UndecidableInstances to permit this)
     • In the instance declaration for ‘C [a]’